experiment with a simpler monitor

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 == <<last_tx.status, VariantTag(last_tx.call)>>
+=========================================================================================

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)
+
+===============================================================================

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)

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

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)
+
+=============================================================================

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)
+
 ===============================================================================