diff --git a/doc/case-studies/xycloans/MCxycloans_monitor.tla b/doc/case-studies/xycloans/MCxycloans_monitor.tla new file mode 100644 index 00000000..71dce5b6 --- /dev/null +++ b/doc/case-studies/xycloans/MCxycloans_monitor.tla @@ -0,0 +1,104 @@ +------------------------------- MODULE MCxycloans_monitor ------------------------------- +(* + * An instance of xycloans monitor for model checking and input generation. + * + * Igor Konnov, 2024 + *) +EXTENDS Integers, xycloans_types + +\* the set of all possible token amounts +AMOUNTS == Nat +\* the contract address for the xycLoans contract +XYCLOANS == "xycloans" +\* the token address +XLM_TOKEN_SAC_TESTNET == "xlm-sac" + +\* the pool of addresses to draw the values from +ADDR == { "alice", "bob", "eve", XLM_TOKEN_SAC_TESTNET, XYCLOANS } + +VARIABLES + \* @type: $tx; + last_tx, + \* @type: Str -> Int; + shares, + \* @type: Int; + total_shares, + \* @type: Int; + fee_per_share_universal, + \* Keep track of the current storage, + \* which can be only changed by a successful transaction. + \* @type: $storage; + storage + +INSTANCE xycloans_monitor + +Init == + LET init_stor == [ + self_instance |-> [ + FeePerShareUniversal |-> 0, + TokenId |-> "" + ], + self_persistent |-> [ + Balance |-> [ addr \in ADDR |-> 0 ], + MaturedFeesParticular |-> [ addr \in ADDR |-> 0 ], + FeePerShareParticular |-> [ addr \in ADDR |-> 0 ] + ], + token_persistent |-> [ Balance |-> [ addr \in ADDR |-> 0 ] ] + ] + IN + \* initialize the monitor + /\ shares = [ addr \in {} |-> 0 ] + /\ total_shares = 0 + /\ fee_per_share_universal = 0 + \* 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 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 + /\ storage' = IF success THEN new_stor ELSE storage + +\* restrict the executions to the successful transactions +NextOk == + Next /\ last_tx'.status + +\* use this falsy invariant to generate examples of successful transactions +NoSuccessInv == + ~IsConstructor(last_tx.call) => ~last_tx.status + +\* 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/xycloans_monitor.tla b/doc/case-studies/xycloans/xycloans_monitor.tla new file mode 100644 index 00000000..0e049af7 --- /dev/null +++ b/doc/case-studies/xycloans/xycloans_monitor.tla @@ -0,0 +1,145 @@ +-------------------------- MODULE xycloans_monitor -------------------------- +(* + * A monitor for the xycLoans contract to detect the known issue. + * + * This is a manual translation of the Typescript monitor from + * verify_js_examples_xycloans.ts. Our goal is to produce a simple and readable + * TLA+ specification that is used to monitor existing transactions and + * generate new transactions, e.g., from the current state. + * + * After receiving feedback from the users, we would think about automation. + * + * Igor Konnov, 2024 + *) + +EXTENDS Integers, xycloans_types + +STROOP == 10000000 + +CONSTANT + \* The token address for the xycLoans contract. + \* @type: Str; + XLM_TOKEN_SAC_TESTNET + +(* The internal state of our monitor (not of the contract) *) +VARIABLES + \* Shares per address. + \* @type: Str -> Int; + shares, + \* The sum over all shares. + \* @type: Int; + total_shares, + \* Fee per share for the entire pool, in stroops. + \* @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 + /\ 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) + \* these conditions are not required by a monitor, but needed to avoid spurious generated values + /\ succeeds_with(tx, + tx.env.storage.self_instance.FeePerShareUniversal = tx.env.old_storage.self_instance.FeePerShareUniversal) + \* these conditions are not required by a monitor, but needed to avoid spurious generated values + /\ succeeds_with(tx, + tx.env.storage.self_persistent = tx.env.old_storage.self_persistent) + /\ shares' = [ addr \in {} |-> 0 ] + /\ total_shares' = 0 + /\ fee_per_share_universal' = 0 + +\* @type: $tx => Bool; +deposit(tx) == + LET call == AsDeposit(tx.call) + token == tx.env.storage.self_instance.TokenId + new_shares == [ shares EXCEPT ![call.from] = @ + call.amount ] + 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) + \* `from` received `amount` shares + /\ LET from_amt == get_or_else(tx.env.storage.self_persistent.Balance, call.from, 0) + old_from_amt == get_or_else(tx.env.old_storage.self_persistent.Balance, call.from, 0) + IN + /\ succeeds_with(tx, new_shares[call.from] = from_amt) + /\ succeeds_with(tx, from_amt = old_from_amt + call.amount) + \* these conditions are not required by a monitor, but needed to avoid spurious generated values + /\ succeeds_with(tx, + \A other \in DOMAIN tx.env.storage.self_persistent.Balance \ {call.from}: + /\ other \in DOMAIN tx.env.old_storage.self_persistent.Balance + /\ tx.env.storage.self_persistent.Balance[other] = tx.env.old_storage.self_persistent.Balance[other]) + /\ succeeds_with(tx, call.amount > 0) + \* update the monitor state + /\ shares' = new_shares + /\ total_shares' = total_shares + call.amount + /\ UNCHANGED fee_per_share_universal + +\* @type: $tx => Bool; +borrow(tx) == + LET call == AsBorrow(tx.call) + expected_fee == div_ceil(call.amount * STROOP, 12500000000) + expected_fee_per_share_universal == + tx.env.old_storage.self_instance.FeePerShareUniversal + + div_floor(expected_fee * STROOP, total_shares) + IN + /\ IsBorrow(tx.call) + \* `FeePerShareUniversal` has been updated correctly + /\ succeeds_with(tx, + expected_fee_per_share_universal = tx.env.storage.self_instance.FeePerShareUniversal) + \* 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) + \* these conditions are not required by a monitor, but needed to avoid spurious generated values + /\ succeeds_with(tx, tx.env.storage.self_persistent = tx.env.old_storage.self_persistent) + /\ succeeds_with(tx, call.amount > 0) + \* update the monitor state + \* we update the fee per share to compute rewards later + /\ fee_per_share_universal' = expected_fee_per_share_universal + /\ UNCHANGED <> + +\* @type: $tx => Bool; +update_fee_rewards(tx) == + LET call == AsUpdateFeeRewards(tx.call) + fees_not_yet_considered == + fee_per_share_universal - get_or_else(tx.env.old_storage.self_persistent.FeePerShareParticular, call.addr, 0) + expected_reward == div_floor(get_or_else(shares, call.addr, 0) * fees_not_yet_considered, STROOP) + mf == get_or_else(tx.env.storage.self_persistent.MaturedFeesParticular, call.addr, 0) + old_mf == get_or_else(tx.env.old_storage.self_persistent.MaturedFeesParticular, call.addr, 0) + actual_reward == mf - old_mf + IN + /\ IsUpdateFeeRewards(tx.call) + \* fee per share for `addr` is bumped to the universal fee per share + /\ LET fee == get_or_else(tx.env.storage.self_persistent.FeePerShareParticular, call.addr, 0) IN + succeeds_with(tx, fee = fee_per_share_universal) + \* delta of matured rewards for `addr` have been added + /\ expected_reward = actual_reward + \* these conditions are not required by a monitor, but needed to avoid spurious generated values + /\ succeeds_with(tx, + tx.env.storage.self_persistent.Balance = tx.env.old_storage.self_persistent.Balance) + \* update the monitor state + /\ UNCHANGED <> + +============================================================================= \ No newline at end of file diff --git a/doc/case-studies/xycloans/xycloans_types.tla b/doc/case-studies/xycloans/xycloans_types.tla new file mode 100644 index 00000000..3d279b2a --- /dev/null +++ b/doc/case-studies/xycloans/xycloans_types.tla @@ -0,0 +1,87 @@ +--------------------------------- MODULE xycloans_types ----------------------- +EXTENDS Variants + +(* + The relevant parts of the storage that is accessed by the contract. + Note that our view of the storage is partial: at any point in time, we only have + access to the parts of the storage that are touched by the contract. + + @typeAlias: storage = { + self_instance: { + FeePerShareUniversal: Int, + TokenId: Str + }, + self_persistent: { + Balance: Str -> Int, + MaturedFeesParticular: Str -> Int, + FeePerShareParticular: Str -> Int + }, + token_persistent: { + Balance: Str -> Int + } + }; + + The environment of the xycLoans contract that should be + produced by Solarkraft from the transaction metadata: + + @typeAlias: env = { + current_contract_address: Str, + storage: $storage, + old_storage: $storage + }; + + An external contract call: + + @typeAlias: call = + Constructor({ addr: Str }) + | Initialize({ token: Str }) + | Deposit({ from: Str, amount: Int }) + | Borrow({ receiver_id: Str, amount: Int }) + | UpdateFeeRewards({ addr: Str}) + ; + + Finally, a transaction is: + + @typeAlias: tx = { + env: $env, + call: $call, + status: Bool + }; + *) +xycloans_typedefs == TRUE + +(* Boilerplate definitions for the method types (mostly generated with copilot) *) + +\* @type: Str => $call; +Constructor(addr) == Variant("Constructor", [ addr |-> addr ]) +\* @type: $call => Bool; +IsConstructor(call) == VariantTag(call) = "Constructor" +\* @type: Str => $call; +Initialize(token) == Variant("Initialize", [ token |-> token ]) +\* @type: $call => Bool; +IsInitialize(call) == VariantTag(call) = "Initialize" +\* @type: $call => { token: Str }; +AsInitialize(call) == VariantGetUnsafe("Initialize", call) + +\* @type: (Str, Int) => $call; +Deposit(from, amount) == Variant("Deposit", [ from |-> from, amount |-> amount ]) +\* @type: $call => Bool; +IsDeposit(call) == VariantTag(call) = "Deposit" +\* @type: $call => { from: Str, amount: Int }; +AsDeposit(call) == VariantGetUnsafe("Deposit", call) + +\* @type: (Str, Int) => $call; +Borrow(receiver_id, amount) == Variant("Borrow", [ receiver_id |-> receiver_id, amount |-> amount ]) +\* @type: $call => Bool; +IsBorrow(call) == VariantTag(call) = "Borrow" +\* @type: $call => { receiver_id: Str, amount: Int }; +AsBorrow(call) == VariantGetUnsafe("Borrow", call) + +\* @type: Str => $call; +UpdateFeeRewards(addr) == Variant("UpdateFeeRewards", [ addr |-> addr ]) +\* @type: $call => Bool; +IsUpdateFeeRewards(call) == VariantTag(call) = "UpdateFeeRewards" +\* @type: $call => { addr: Str }; +AsUpdateFeeRewards(call) == VariantGetUnsafe("UpdateFeeRewards", call) + +=============================================================================== \ No newline at end of file