An example specification of the Cosmos SDK bank module

examples/.scripts/run-example.sh

@@ -34,7 +34,8 @@ result () {
             "$file" =~ ^cryptography/ ||
             "$file" =~ ^spells/ ||
             "$file" == "solidity/SimpleAuction/SimpleAuction.qnt" ||
-            "$file" == "cosmos/ics20/base.qnt" ) ]] ; then
+            "$file" == "cosmos/ics20/base.qnt" ||
+            "$file" == "cosmos/bank/bank.qnt" ) ]] ; then
       printf "N/A[^nostatemachine]"; return
     fi
 

examples/README.md

@@ -57,6 +57,8 @@ listed without any additional command line arguments.
 | [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> |
 | [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmos/bank/bank.qnt](./cosmos/bank/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
+| [cosmos/bank/bankTest.qnt](./cosmos/bank/bankTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/cosmos/bank/bank.qnt

@@ -0,0 +1,202 @@
+// -*- mode: Bluespec; -*-
+// An executable specification of the bank module
+module bank {
+  //----------------------- type declarations -------------------------
+  // Addresses are simply strings
+  type Addr = str
+  // Denominations are simply strings too
+  type Denom = str
+  // 64-bit and 256-bit integers are a special case of big integers.
+  // We have to take care of the bit width where it matters.
+  type Int64 = int
+  type Int256 = int
+
+  // the maximum value for Int256 in Golang
+  pure val MAX_INT256 = 2^256 - 1
+
+  // the range of 256-bit integers in the SDK
+  pure def isInt256(i: int): bool = -2^256 < i and i < 2^256
+
+  // A coin is a record that contains a denomination and an amount
+  type Coin = { denom: Denom, amount: Int256 }
+  // Coins is a map from denominations to amounts
+  type Coins = Denom -> Int256
+  // Account balances
+  type Balance = { address: Addr, coins: Coins }
+
+  // A result that is produced by the functions that update the context
+  type BankResult =
+    | BankErr(str)
+    | BankOk(BankCtx)
+
+  // A result that is produced by the functions that return a coin or panic
+  type CoinResult =
+    | CoinErr(str)
+    | CoinOk(Coin)
+
+  // A result that is produced by the functions that return a Boolean or panic
+  type BoolResult =
+    | BoolErr(str)
+    | BoolOk(bool)
+
+  // An input of a multiparty transfer
+  type Input = {
+    address: str,
+    coins: Coins,
+  }
+  // An output of a multiparty transfer
+  type Output = {
+    address: str,
+    coins: Coins,
+  }
+  // the portion of the context that is accessed by the bank module
+  type BankCtx = {
+    // block time (needed by vesting accounts)
+    blockTime: Int64,
+    // accessed via AccountKeeper
+    accounts: Set[Addr],
+    // the balances are the essential part of the bank module
+    balances: Addr -> Coins,
+    // module parameters
+    params: Params,
+  }
+
+  // Parameters of the bank module
+  type Params = {
+    // whether coin send is enabled for specific denominations
+    sendEnabled: Set[{ denom: str, enabled: bool }],
+    // whether coin send is enabled by default
+    defaultSendEnabled: bool,
+  }
+
+  //------- the module logic, that is, the logic of keepers -----------
+
+  /// `GetAllBalances` returns all the account balances for the given account address.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L61
+  pure def ViewKeeper::GetAllBalances(ctx: BankCtx, addr: Addr): Coins = {
+    if (ctx.balances.keys().contains(addr)) {
+      ctx.balances.get(addr)
+    } else {
+      Map()
+    }
+  }
+
+  /// `ValidateBalance` should only be called upon genesis state.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L202
+  pure def ViewKeeper::ValidateBalance(ctx: BankCtx, addr: Addr): bool = and {
+    ctx.accounts.contains(addr),
+    val coins = ViewKeeper::GetAllBalances(ctx, addr)
+    // Implementation: Coins.IsValid also validates denominations
+    coins.keys().forall(denom => coins.get(denom) > 0),
+    // TODO: add validation logic for the vesting accounts
+  }
+
+  /// GetBalance returns the balance of a specific denomination for a given account by address.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L98
+  pure def ViewKeeper::GetBalance(ctx: BankCtx, addr: Addr, denom: str): CoinResult = {
+    if (ctx.balances.keys().contains(addr)) {
+      val accountBal = ctx.balances.get(addr)
+      if (accountBal.keys().contains(denom)) {
+        CoinOk({ denom: denom, amount: accountBal.get(denom) })
+      } else {
+        CoinErr("Unmarshal error")
+      }
+    } else {
+      CoinErr("Unmarshal error")
+    }
+  }
+
+  /// HasBalance returns whether or not an account has at least amt balance.\
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L56
+  pure def ViewKeeper::HasBalance(ctx: BankCtx, addr: Addr, coin: Coin): BoolResult = {
+    // Implementation: panic if the address or denomination are not stored?
+    match ViewKeeper::GetBalance(ctx, addr, coin.denom) {
+    | CoinOk(c) => BoolOk(c.amount >= coin.amount)
+    | CoinErr(msg) => BoolErr(msg)
+    } 
+  }
+
+  /// GetAccountsBalances returns all the accounts balances from the store.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/view.go#L72
+  pure def ViewKeeper::GetAccountsBalances(ctx: BankCtx): Set[Balance] = {
+    // The implementation may panic due to unmarshalling errors.
+    // Since these errors are not related to the parameters, we do not propagate them.
+    ctx.balances.keys().map(a => { address: a, coins: ctx.balances.get(a) })
+  }
+
+  /// SendCoins transfers amt coins from a sending account to a receiving account.
+  /// An error is returned upon failure.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L135
+  pure def SendKeeper::SendCoins(ctx: BankCtx,
+      fromAddr: Addr, toAddr: Addr, amt: Coins): BankResult = {
+    // Implementation: if Coins are constructed with NewCoins, they must be positive.
+    // However, if they are constructed another way, there is no precondition.
+    // TODO: checking LockedCoins that deal with vested coins.
+    // Safely subtract the coins from fromAddr and add them to toAddr.
+    val fromCoins = ViewKeeper::GetAllBalances(ctx, fromAddr)
+    if (amt.keys().exists(d =>
+        not(d.in(fromCoins.keys())) or fromCoins.get(d) < amt.get(d))) {
+      // some denominations do not exist on fromAddr, or there is not enough funds
+      BankErr("invalid coins or insufficient funds")
+    } else {
+      // x/bank invariants prohibit persistence of zero balances
+      // clean zero balances
+      def getOr0(coins: Coins, d: str): int = if (d.in(coins.keys())) coins.get(d) else 0
+      val positiveDenoms = fromCoins.keys().filter(d => fromCoins.get(d) > getOr0(amt, d))
+      val subCoins = positiveDenoms.mapBy(d => fromCoins.get(d) - getOr0(amt, d))
+      // add coins to toAddr: the tricky part is that the denominations may differ
+      val toCoins = ViewKeeper::GetAllBalances(ctx, toAddr)
+      // extend the toCoins and amt with zeroes over the joint denominations
+      val jointDenoms = toCoins.keys().union(amt.keys())
+      // since toCoins and amt held positive values, their sums must be positive too
+      val addCoins = jointDenoms.mapBy(d => getOr0(toCoins, d) + getOr0(amt, d))
+      if (addCoins.keys().exists(d => addCoins.get(d) > MAX_INT256)) {
+        BankErr("overflow")
+      } else {
+        // add toAddr to the accounts, if it did not exist
+        val newAccounts = ctx.accounts.union(Set(toAddr))
+        val newBalances =
+          if (fromAddr == toAddr) {
+            ctx.balances
+          } else {
+            // Update the balance of fromAddr with subCoins.
+            val newBalancesSub = ctx.balances.set(fromAddr, subCoins)
+            // Since toAddr may be a new account, extend the map, if needed
+            newBalancesSub.put(toAddr, addCoins)
+          }
+        // succeed with a new balance
+        BankOk({ ...ctx, balances: newBalances, accounts: newAccounts })
+      }
+    }
+  }
+
+  /// GetParams returns the total set of bank parameters.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L61
+  pure def SendKeeper::GetParams(ctx: BankCtx): Params = ctx.params
+
+  /// SetParams sets the total set of bank parameters.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L67
+  pure def SendKeeper::SetParams(ctx: BankCtx, params: Params): BankCtx = {
+    { ...ctx, params: params }
+  }
+
+  /// IsSendEnabledCoin returns the current SendEnabled status of the provided coin's denom.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L315
+  pure def SendKeeper::IsSendEnabledCoin(ctx: BankCtx, coin: Coin): bool = {
+    val found = ctx.params.sendEnabled.filter(p => coin.denom == p.denom)
+    if (found != Set()) {
+      found.exists(p => p.enabled)
+    } else {
+      ctx.params.defaultSendEnabled
+    }
+  }
+
+  /// IsSendEnabledCoins checks the coins provide and returns an ErrSendDisabled if
+  /// any of the coins are not configured for sending.  Returns nil if sending is enabled
+  /// for all provided coin.
+  /// https://github.com/cosmos/cosmos-sdk/blob/06406f6a70f228bbb6d09b45a4e343477f1ef7e9/x/bank/keeper/send.go#L306C28-L306C28
+  pure def SendKeeper::IsSendEnabledCoins(ctx: BankCtx, coins: Set[Coin]): bool = {
+    // Implementation: return the error ErrSendDisabled on false
+    coins.forall(c => SendKeeper::IsSendEnabledCoin(ctx, c))
+  }
+}

examples/cosmos/bank/bankTest.qnt

@@ -0,0 +1,118 @@
+// -*- mode: Bluespec; -*-
+
+module bankTest {
+  import bank.* from "./bank"
+
+  // the state of the machine that tests the logic
+  // Total supply of coins per denomination
+  var supply: Denom -> Int256
+  // Balances for each address
+  var balances: Addr -> Coins
+  // if non-empty, then it stores the last error message
+  var _lastError: str
+  // all addresses we would like to work with
+  pure val ADDR = Set("king", "donkeykong", "peaches", "mario")
+  // all denominations
+  pure val DENOM = Set("banana", "burger")
+
+  // state transitions of the machine
+  // initialize the state machine
+  action init = all {
+    // limit the total supply of burgers and bananas to 10_000
+    supply' = Set("banana", "burger").mapBy(d => 10_000),
+    // the king has it all
+    balances' = Map("king" -> Set("banana", "burger").mapBy(d => 10_000)),
+    _lastError' = "",
+  }
+
+  action send(fromAddr: Addr, toAddr: Addr, coins: Coins): bool = all {
+    val ctx = stateToCtx(0)
+    val result = SendKeeper::SendCoins(ctx, fromAddr, toAddr, coins)
+    match result {
+      | BankOk(newCtx) => all {
+        balances' = newCtx.balances,
+        supply' = supply,
+        _lastError' = "",
+      }
+      | BankErr(msg) => all {
+        // We could simply return 'false' here.
+        // But we prefer to store the error message instead.
+        _lastError' = msg,
+        balances' = balances,
+        supply' = supply,
+      }
+    }
+  }
+
+  action step = any {
+    nondet fromAddr = oneOf(ADDR)
+    nondet toAddr = oneOf(ADDR)
+    nondet denom = oneOf(DENOM)
+    nondet amt = (-10).to(supply.get(denom)).oneOf()
+    send(fromAddr, toAddr, Set(denom).mapBy(d => amt))
+  }
+
+  // protocol invariants
+  // sum up amounts over all balances for a given denomination
+  def sumForDenom(denom: Denom): Int256 = {
+    balances.keys().fold(0, (sum, addr) => {
+      val coins = balances.get(addr)
+      if (denom.in(coins.keys())) {
+        sum + coins.get(denom)
+      } else {
+        sum
+      }
+    })
+  }
+
+  // The total Supply of the network is equal to the sum of all coins from the account
+  val totalSupplyInv = {
+    supply.keys().forall(denom => (sumForDenom(denom) == supply.get(denom)))
+  }
+
+  // tests
+  run getAllBalancesTest = {
+    init
+      .expect(
+        val ctx = stateToCtx(0)
+        val kings = ViewKeeper::GetAllBalances(ctx, "king")
+        val donkeys = ViewKeeper::GetAllBalances(ctx, "donkeykong")
+        and {
+          assert(kings.keys() == Set("banana", "burger")),
+          assert(kings.get("banana") == 10_000),
+          assert(kings.get("burger") == 10_000),
+          assert(donkeys.keys() == Set()),
+        }
+      )
+  }
+
+  // a helper operator that produces a context from a state
+  def stateToCtx(time: int): BankCtx = {
+    {
+      blockTime: time,
+      accounts: balances.keys(),
+      balances: balances,
+      params: {
+        sendEnabled: Set(),
+        defaultSendEnabled: true
+      }
+    }
+  }
+
+  run sendTest = {
+    init
+      // the King has bananas and he can send it
+      .then(send("king",
+                 "donkeykong",
+                 Map("banana" -> 2_000)))
+      .expect(and {
+        balances.get("king").get("banana") == 8_000,
+        balances.get("donkeykong").get("banana") == 2_000,
+        balances.get("king").get("burger") == 10_000,
+        balances.get("donkeykong").keys() == Set("banana"),
+      })
+      // Donkeykong does not have any burgers, so this action must fail
+      .then(send("donkeykong", "peaches", Set("burger").mapBy(d => 1_000)))
+      .expect(_lastError == "invalid coins or insufficient funds")
+  }
+}