WARNING: Compiler instructed to emit for Algorand, but the conservative analysis found these potential problems

[Fraccas]

We recently added the option to update a specified price of assets within a smart contract, while upgrading to Reach 0.1.13 from 0.1.12. One contract was not changed at all but started giving these messages after the upgrade.

Since these changes, we have been getting warnings when compiling our contracts, our BE server logs, and FE console logs.

WARNING: Compiler instructed to emit for Algorand, but the conservative analysis found these potential problems:
 * API Buyer_buy may use up to 10 transaction references, but the limit is 8. API Buyer_buy starts at /app/index.rsh:112:21:application.
 * API Buyer_buy may use up to 5 accounts, but the limit is 4. API Buyer_buy starts at /app/index.rsh:112:21:application.
 * API Updater_delist may use up to 10 transaction references, but the limit is 8. API Updater_delist starts at /app/index.rsh:112:21:application.
 * API Updater_delist may use up to 5 accounts, but the limit is 4. API Updater_delist starts at /app/index.rsh:112:21:application.
 * API Updater_updatePrice may use up to 10 transaction references, but the limit is 8. API Updater_updatePrice starts at /app/index.rsh:112:21:application.
 * API Updater_updatePrice may use up to 5 accounts, but the limit is 4. API Updater_updatePrice starts at /app/index.rsh:112:21:application.
 * Step 1 may use up to 10 transaction references, but the limit is 8. Step 1 starts at /app/index.rsh:86:11:dot.
 * Step 1 may use up to 5 accounts, but the limit is 4. Step 1 starts at /app/index.rsh:86:11:dot.
 * Step 3 may use up to 10 transaction references, but the limit is 8. Step 3 starts at /app/index.rsh:112:21:dot.
 * Step 3 may use up to 5 accounts, but the limit is 4. Step 3 starts at /app/index.rsh:112:21:dot.

How concerned should we be with these warnings? Is it possible that our contracts can go into a broken state which will cause a loss of assets?

We have 3 contracts total, with all giving similar warnings. Here's an example of a contract that allows users to swap ASAs for ASAs.

https://gist.github.com/Fraccas/bac07ca00f8ae64da471061a36cf68d1

If we should not be concerned, is there a way to disable these messages from logging on to our site/backend?

[jeapostrophe]

You should be concerned. If you want to not print stuff out, you can use an environment variable: https://docs.reach.sh/frontend/#p_135

Here are some things to try:

• Remove line 113 and strengthen the invariant to be balance() == flatFee
• Add a commit on line 97 and then another API call. --- This makes it so that the parallelReduce body and continuation are guaranteed to get different transactions

[Fraccas]

So we are testing out the API call option, and it is dividing the Buyer.pay step from the asset transfer step.

In this case, it would be possible for a Buyer to pay the contract, who could then fail to sign the delete contract txn, and fail to receive the assets that they paid for.

  commit();
  Anybody.publish();

became

  commit();
  // Call API
  try {
    const [ _, k3 ] =
      call(Buyer.end)
        .assume(() => assume(true));
    k3(null);
  } catch (_) {
    Anybody.publish();
  }

In practice, this works, but we'd rather not have the user sign two different txns to complete the purchase. Are there any ways that we can restructure to ensure the payment and asset transfer are in the same step? We are experimenting with adding the transfers to the API calls within the parallel reduce but having some trouble with formal verification.

[jeapostrophe]

I find the change you made really strange.

First, the .assume does nothing, you should remove it.
Second, the try can't be violated, because there's no throw, so it also does nothing.

Basically, what you wrote is equivalent to:

commit()
const [ _, k3 ] = call(Buyer.end);
k3(null);

Now, even though you're calling it Buyer, there's nothing in this that restricts the caller to actually be the buyer. It could be anyone.

On to your question... you can have them in the same transaction if you move lines 98-111 to be inside the Buyer.buy call.

I think your program is overly complex and you could make it a lot simpler. You have a parallelReduce, but in reality, the only thing that can happen multiple times is the updatePrice call. But, the updatePrice is the same as delist + relist, so my advice is to change your program to be:

Creator: publish the the stuff
race between the Creator and Buyer
Creator can delist
Buyer can buy

That's going to remove the parallelReduce and the verification will be trivial.

[Fraccas]

Are you suggesting that we remove the option to update the price to improve security?

We recently rewrote the contract with the parallel reduce to add support for updating the price.

The previous contract did not have any warnings/issues, but it's extra steps for the end user to delist/relist. If security is a tradeoff we'll revert the changes.

Previous Contract

// Swap NFT for NFT Smart Contract
// includes delisting, seller flat fee of 1A, and x amount of NFT for x amount of NFT

'reach 0.1';
'use strict';

const flatFee = 1000000;

// NFT for NFT swap listing
export const main = Reach.App(() => {
  const Seller =  Participant('Seller', {
    setSell: Fun([], Tuple(Token, UInt, Token, UInt, Address)),
    showSell: Fun([Contract], Null), 
  });

  const Viewer = Participant('Viewer', {
    getBuy: Fun([Token, UInt, Token, UInt], Null),
  });

  const Buyer =  API('Buyer', {
    showBuy: Fun([], Null), //Tuple(Token, UInt, Token, UInt)),
    delist: Fun([], Bool)
  });

  init();

  // get NFT token id, nft amount, and price from Seller
  Seller.only(() => {
    // asset to purchase, # of said asset, asset needed to purchase, # of said asset
    const [ sellerNFT, sellerNftAmt, buyerNFT, buyerNftAmt, platformAddress ] = declassify(interact.setSell());
    assume(sellerNFT != buyerNFT);
  });
  Seller.publish(sellerNFT, sellerNftAmt, buyerNFT, buyerNftAmt, platformAddress); // publish to blockchain
  commit();
  
  Seller.pay([ flatFee, [sellerNftAmt, sellerNFT ]]); // Seller transfer NFTs to smart contract and pays 1A flat fee

  require(balance(sellerNFT) == sellerNftAmt); // require the amount of NFT equal to amount
  commit();

  Seller.only(() => {
    interact.showSell(getContract());
  });

  Viewer.only(() => {
    // asset to purchase, # of said asset, asset needed to purchase, # of said asset
    interact.getBuy(sellerNFT, sellerNftAmt, buyerNFT, buyerNftAmt);
  });

  fork()
  .paySpec([buyerNFT]) // specify token as payment
  .api(Buyer.delist,
      (() => { assume(this == Seller); }),
      // pay 0 Algo, pay zero NFT
      (() => [0, [0, buyerNFT]]),
      (k => {
          k(this == Seller);
          require(this == Seller);
          transfer(balance()).to(Seller);
          transfer(balance(sellerNFT), sellerNFT).to(this);
          transfer(balance(buyerNFT), buyerNFT).to(Seller);
          commit();
          exit();
      }))
  .api(Buyer.showBuy,
      // pay 0 Algo, pay set amt of buyer NFT
      () => [0, [buyerNftAmt, buyerNFT]],
      (k => {
          //k([sellerNFT, sellerNftAmt, buyerNFT, buyerNftAmt]);
          k(null);
      }))
  .timeout(false);

  transfer(flatFee).to(platformAddress);
  transfer(balance()).to(Seller);
  transfer(balance(sellerNFT), sellerNFT).to(this);
  transfer(balance(buyerNFT), buyerNFT).to(Seller);

  commit();
  exit();
});

[Fraccas]

So we actually tried this suggestion
On to your question... you can have them in the same transaction if you move lines 98-111 to be inside the Buyer.buy call.

With some adjustments, we no longer have errors/warnings and can ensure that the swapping of assets occurs within a single step. Thanks for all the help!

[jeapostrophe]

Boom