Ensure assets are not stuck in DC

[Sword-Smith]

• [x] Ensure explicit party numbers are sequential, starting at 1
• [x] Get number of parties for IntermediateContract (as function)
• [x] Add a boolean to IntermediateContract indicating if DC needs a tokenID = 0
• [ ] Calculate this boolean based on the contract
• [x] Store and use evaluated party token values in storage. First time pay() is called for a specific tokenID, this value is set
• [x] Implement tokenID = 0 handling in pay()
• [ ] Test that no assets are stuck in DC through extensive unit testing with multiple settlement assets

[Sword-Smith]

First task solved in 89d9662a3f8e94e116dff08571ec9cc743491969. Branch ensure-assets-not-stuck created for this issue.

[Sword-Smith]

Simon has convinced me that this problem in the general case cannot be solved in the type checker alone. It involves symbolic manipulation to e.g. determine that x - 10 + x are equivalent. For simple equations, this should be doable, but the algebra of our expressions contain min(a, b), max(a,b) if-then-else etc. which makes this generic approach hard to impossible.

So we need to implement the approach where tokenID=0 represents the position that that gets the funds that are not paid out to other parties. To achieve this, we need to at least complete the five tasks presented above.

I propose a function returning a bool in intermediateCompiler. This function attempts to determine if tokenId=0 is required for this contract. If it is needed, then its value can first be derived after all other positions are evaluated and their results stored in storage.

[Sword-Smith]

So for a contracts like these, no tokenID = 0 are needed.

Will always pay 1 DAI to party 1

transfer(DAI, 1)

Will always pay 1 DAI to party 1 and 1 GOLEM to party 2

both(
   transfer(DAI, 1),
   transfer(GOLEM, 2)

Will always pay a combined value of 10 DAI to party 1 and party 2

both(
    scale(10, obs(int, <addr>, 0 ), transfer(DAI, 1)),
     scale(10, 10 - obs(int, <addr>, 0 ), transfer(DAI, 2)))

where the rule to verify that no tokenID=0 is needed is that expr1 + expr2 = maxFactor1 = maxFactor2 = activationMap, or more generally: sum{expr_i, i = 1..N}=maxFactor_j, for all j (transfer calls). This will equal the activate map for all assets (I think).

In this latter example, we need symbolic manipulation/evaluation to calculate evaluate that x - 10 + x = 10. That is hard.

I suggest we write a function that returns a boolean holding our conclusion whether a tokenID = 0 is needed or not. If we cannot come to a conclusion, we of course need a tokenID = 0.