Theorem failures in dispenser contract

[NWBY]

'reach 0.1';

export const main = Reach.App(() => {
    const Seller = Participant('Seller', {
        asaToken: Token,
        pricePerAlgo: UInt,
        amount: UInt
    });
    const Buyer = Participant('Buyer', {
        algoPurchaseAmount: UInt
    });

    init();

    Seller.only(() => {
        const asa = declassify(interact.asaToken);
        const pricePerAlgo = declassify(interact.pricePerAlgo);
        const amount = declassify(interact.amount);
    });
    Seller.publish(asa, pricePerAlgo, amount);
    commit();

    Seller.pay([[amount, asa]]);
    commit();

    Buyer.only(() => {
        const algoPurchaseAmount = declassify(interact.algoPurchaseAmount);
    });
    Buyer.publish(algoPurchaseAmount).pay(algoPurchaseAmount);
    require(amount > (algoPurchaseAmount * pricePerAlgo));
    require(algoPurchaseAmount > 0);

    const tokenReturnAmount = algoPurchaseAmount * pricePerAlgo;
    
    assert(amount > tokenReturnAmount);
    transfer(algoPurchaseAmount).to(Seller);
    transfer([[tokenReturnAmount, asa]]).to(Buyer);
    commit();
});

I'm attempting to build a simple dispenser contract for ASAs.

• ASA owner sets exchange rate and amount they want to sell
• Buyer pays X amount of Algo and receives X amount of ASA in return

However, I'm getting a number of theorem failures:

• Balance zero at exit - I know Reach prevents the contract from having funds at the end but for a dispenser contract we would need the seller to be able to provide the sale amount in one go and then multiple buyers can purchase the tokens until the sale amount is 0
• Failures on the two require statements saying that the result would be false

Anyone able to help?

[jeapostrophe]

For your first issue, you have to get the balance to be zero at the end. You have not yet made it so multiple buyers can do anything, so it is a bit misleading to try and fix this until you've completed what you hope the program will do. At the moment, you could return the unspent amounts to the seller.

For the second issue, the Buyer is not assumeing that those computations are correct. You could fix this by adding them as assumes, but you will probably rewrite this program to use a loop (via parallelReduce) and then you'll probably want to have an API call (with .api_) and then it will be more natural to use check