minimal TLA+ spec of the xycloans monitor

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

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 <<shares, total_shares>>
+
+\* @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 <<shares, total_shares, fee_per_share_universal>>
+
+=============================================================================

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