There seems to be a bug in the Playground at https://prod.meadow.marlowe.iohkdev.io/

I enter the following Haskell program into the "Haskell Editor" tab:

{-# LANGUAGE OverloadedStrings #-}
module Swap where

import           Language.Marlowe

main :: IO ()
main = print . pretty $ contract

contract :: Contract
contract =
    Let stakeId (Constant 100) $
    When 
        [ Case (Deposit "Alice" "Alice" stake) $
            When 
                [ Case (Deposit "Bob" "Bob" stake) $
                    When
                        [ Case (Notify TrueObs) $ Pay "Bob" (Party "Alice") stake Refund
                        , Case (Notify FalseObs) $ Pay "Alice" (Party "Bob") stake Refund
                        ] 20 Refund
                ] 10 Refund
         ] 5 Refund
  where
    stakeId = ValueId 1
    stake = UseValue stakeId

This program compiles just fine, but when I send it to "Simulation", I get a weird error in line 2, saying "expected '-'".

Currently, symbolic execution only takes a contract as input, and it assumes the initial state is empty. This can be counter-intuitive from the point of view of the playground since the contract may be half-way execution when the analysis button is pressed, and the analysis will typically find warnings that are impossible to reproduce because the state prevents them from happening.

To solve this we propose to pass the state together with the contract and run the analysis from there.

Semantics 3.0 do not implement contract-Let or value-Bind. Implementing Merkle trees instead of contract-Let would be very elegant, specially since we do not have While anymore and we can get replication.

But we definitely want to implement value-Bind, even though it should be quite straightforward.

Do we want to have multiplication and division?

We have skipped it from the first draft of semantics for simplicity.

See feedback:

Observation ValueGE
  - why isn't there also ValueLE and ValueEQ?

we'll add those. I've implemented it the same way as it was in Marlowe semantics, where it was only ValueGE and Not, which was sufficient to prove things, I think.

Documentation should note that these are missing and will be added later. 

Multiplication by a constant.

See feedback:

Blockly contains a lot of self-explanatory text, which is great. But this is in tension with the desire for blocks not to be too large, so that I can see a reasonable chunk of program at one time. Even small Blockly programs occupy a huge amount of screen. Some attention to making the blocks more compact would help.

Try to find out if there is a way of fixing the length of the lists that represent maps in symbolic execution, so that it is not necessary to use the symbolic versions of tail and head.

See feedback:

In some windows, attempting to move the mouse out of the window causes automatic scroll. Good! This is both intuitive and convenient. But in the window for composing a Blockly program, one needs to explicitly move the scroll bars to scroll the window, which is inconvenient. The automatic scroll behaviour would make it much easier to compose programs, since even the simplest program is likely to exceed the window size.

See #20

This is the long-term version of #9. See #9 for more detail.
See feedback:

And again, for the long term I am not convinced this is the best design. It would be simpler if once money was given to the contract it just belongs to the contract. In the 'both' example, each would just pay out 100 of the money (one hopes greater than 200) committed to the contract. 

The Simulation tab on the playground could be integrated into VSCode. This would enable development of contracts offline and also symbolic analysis offline. It could also open up a new format for structured editing and integration with Haskell editing.

See feedback:

  - what is the purpose of the second timeout?

second timeout is a timeout after which the committed money can be redeemed if there anything left to redeem. 
For example if one committed 100 Ada before start timeout and payed 80 Ada during the contract continuation, he/she can redeem remaining 20 Ada after `end (second) timeout`. 

  - what happens if it is exceeded?

same thing happens when CommitCash is evaluated either after first or after second timeout – the contract continues with the second "timeout" continuation of CommitCash.
For example, say, we have a contract: CommitCash (IdentCC 1) (1024 Ada) (startTimeout = 50) (endTimeout = 200) contract1 contract2
If the current slot is, say, 20, then the commit is successful and the evaluation is continued with `contract1`. Committer can redeem money left after `endTimeout` slot 200.
If the current slot is, say, 70, or 270 – the commit is `timed out` and the evaluation continues with `contract2`.

This is definitely not clear in the existing tutorial. It must be clarified.```

Subj

See feedback:

  - what is the identifier (IdentCC) used for?

 the identifier is used to identify the commit in RedeemCC construct or in Both construct.
like in CommitCC (IdentCC 1) (1024 Ada)  (startTimeout = 50) (endTimeout = 200) (contract1 = RedeemCC (IdentCC1) Null) (contract2 = Null) – this allows to redeem committed money immediately after commit, not waiting for `endTimeout`. So if one committed at slot 40, he'll be able to redeem at slot 51.
or in Both (CommitCC (IdentCC 1) (100 Ada) con1 con2) 
(CommitCC (IdentCC 2) (100 Ada) con3 con4) – here we need to specify commit from which branch we perform.
We require CommitCC identifiers to be unique within a contract.

Again, this needs clarification in the tutorial.

The plutus tutorial is deployed on the same server that plutus playground is running, this means it is always up to date, see the “Tutorial” link here https://prod.playground.plutus.iohkdev.io/.

Aim is to do the same for Marlowe, once revision process terminated. Would also require re-formatting to Ascii doc.

Add a construct for Marlowe debugging that allows the user to specify parts of the code that should not be reachable and extend symbolic analysis to check whether that is the case.

Semantics 3.0 work with slot intervals instead of block numbers. Currently the Values available are SlotIntervalStart and SlotIntervalEnd. Is this desirable? Do we want a way to reason about intervals that uses SlotNumber instead?

See feedback:

Most important: when I pressed the button "-> Blockly to Code" nothing happened! The result was that I lost all my work!

New semantics are currently using the order of elements in a map indexed by (AccountId) as automatically derived by Haskell "deriving".

The order in which the payments of refundAll happen should be irrelevant as long as the information of the state matches the amount of money available. But we may want to define the ordering better so that all the implementations are consistent even if the amount of money available is insufficient.

The Close contract should only refund the money that is available in the accounts, so it should be unable to issue any warnings. If this is indeed the case, we would not need to symbolically analyse the refund procedure (#47).

We might want to include a Marlowe version into a contract.
Also we might want to be able to identify a Marlowe validator from its address (via address attributes?).
The idea is to allow a node to implement Marlowe interpreter natively and speedup contracts execution.

See feedback:

An uninformative error message from the Fay part of Meadow [...] My guess is if this error message exists, there are probably many more like it.

The error:

Error while executing Fay code:

unhandled case in listCurryType,[object Object]

code is attached as contract.hs

See feedback:

  - what is the identifier (IdentPay) used for?

same as for CommitCC: to identify which payment we refer to in Both construct.

Again, this needs to be clarified in the documentation.

We should define a concept of trace for Semantics 3.0, and implement a function that applies the process function to a series of transactions (trace). This is useful for testing and formal verification.

Measure the cost of simulating the final refunds in symbolic analysis and potentially optimise it out.

Plutus has a full nix setup with a VM that provides an off the shelf development environment, this should be expanded with Marlowe stuff.

Use custom tokens to represent Marlowe contract participants.
Implement standard strategies for distributing payments according to token distribution.
Implement "M of N" strategy for providing inputs.

Long-term version of #7. See #7 for more detail.

But, as noted above, I think for the long term the best choice is to get rid of the second timeout. In particular, it strikes me as difficult to ensure that a contract behaves as intended if in the middle of execution it can be terminated and the alternative contract invoked instead. I'm happy to discuss and perhaps be convinced otherwise.

See feedback:

Participants are identified by small positive integers. Shouldn't they be identified by public keys instead?

In the Plutus implementation participants are identified by public keys.

But in Meadow they aren't. Users may find that confusing.

In the short term, the documentation needs to explain that they are small numbers even though one might expect public keys. In the long term, I would argue that Meadow should use public keys.

Semantics 3.0 do not currently implement oracles.

There needs to be a discussion about how oracles should be implemented in Cardano.

In the Haskell code for the Marlowe escrow contract, I have noticed the line:
chose :: Integer -> ConcreteChoice -> Observation

I assume it works, but surely it should be:
chose :: Person -> ConcreteChoice -> Observation

since the contract uses a type of Person throughout. There are several versions of the escrow contract, and they all seem to do this. Maybe I am wrong. Here is an example:
https://github.com/input-output-hk/marlowe/blob/master/src/EscrowV2.hs

The current implementation of Marlowe semantics written in purescript is not performant enough for large contracts. We need to assess how we can make large contracts work nicely on the playground, possibly sending things to the backend instead of executing in the browser.

We should be able to calculate this fast enough to provide warnings in real time, in the Marlowe editor.

We can simplify expressions that do not contain variables.

See feedback:

In the short term, the documentation should be modified to make clear that the contract *waits* until the payout is made before proceeding, and to give an example like the one Alexander gave to explain why a timeout is necessary.

Long term version is #6

See feedback regarding Meadow:

The buttons apple-C, apple-V, apple-+, apple-- all work as expected. Excellent! The tutorial should draw attention to this.

One of Phil's suggestion was to simplify Pay semantics by removing timeout and continuation from it.
We can do this by Eval input and tracking evaluated payments in contract's state.

So, for example, if we have a contract:

Pay id1 alice bob (Value 100) (timeout 1000) (RedeemCC id2)

We could instead have this:

Both (Pay id1 alice bob (Value 100)) (RedeemCC id2)

we could allow any party to do an Eval input transaction to execute payment and save it in state to allow claiming payed money at any point later in time.

One of the issues is was to do in this case:

CommitCash id1 alice (Value 50) 
    (Both (Pay id2 alice bob (Value 100))  (Pay id3 alice charlie (Value 200)))
    Null

There are insufficient funds in Alice's account, and the question is how to handle it.
One way is to split available amount between receivers proportional to payed amount.
Say, Bob gets 16, Charlie gets 32, and left 2 go into contract deposit.

Explore the feasibility of a structured editor for Marlowe that is half-way between plan text and blockly, and that supports function definitions and automated refactorings.