Template constraint extension design

[palas]

This discussion studies the best way to extend Extended Marlowe so that it supports constraints for templates. That is, ways of specifying which ways of filling templates are valid, and which are not. E.g: timeouts in the outer Whens should be before those in inner Whens.

Potential solutions for TimeParam

When we say attached we mean that this approach can be done as an "attachment" to the contract, without modifying the Contract type or any of the dependencies. embedded means it requires changing the Contract type.

1. Attached partial ordering version

• List of tuples of pairs of time parameters: timeout1 ≤ timeout2
  1.2. Variant, also support constants: c ≤ timeout2
  • This will prevent unreachable contract because of epoch timeout

2. Attached partial ordering plus margins

• List of tuples of pairs of time parameters: timeout1 + c ≤ timeout2
• c would be a positive constant time difference in milliseconds, variants:
  2.1. Support multipliers like “days”
  2.2. Support advanced primitives like “next weekend”

1.3. and 2.3. Supporting cycles in the ordering (and negative values in c in the second approach) would allow effectively to express equality: timeout1 ≤ timeout2 && timeout2 ≤ timeout1 ⇒ timeout1 = timeout1

3. Attached generative version

• Two types of parameters, derivedParameter and providedParameter
• Constraints specified as in approaches 1 or 2
• Additionally, list of derived parameters as tuples:
  • derivedParameter := TimeExpression
• TimeExpression could be defined something like this:

TimeExpression = TimeAfter TimeExpression DiffTimeExpression
               | ProvidedParameter

DiffTimeExpression = Days Integer
                   | Months Integer
                   | Years Integer
                   | TimeAdd DiffTimeExpression DiffTimeExpression
                   | TimeMul Integer DiffTimeExpression
                   | TimeDiff TimeExpression TimeExpression

4. Embedded generative version

• Same as 4 but we replace Timeout with TimeExpression

5. Attached generic declarative version

• Degree 1 polynomial equations and inequations
  • Single solution means parameter is generated
• Detached from contract
• Disadvantage: requires SMT solver for filling template

6. Attached boolean expressions (potentially on top of equations)

Potential solutions for ConstantParam

When we say attached we mean that this approach can be done as an "attachment" to the contract, without modifying the Contract type or any of the dependencies. embedded means it requires changing the Contract type.

1. Attached optional min and max: [(String, Maybe Integer, Maybe Integer)], String would be the name of the ConstantParam

2. Attached Choice-like mechanism: [(String, [(Maybe Integer, Maybe Integer)])], String would be the name of the ConstantParam

3. Attached enum plus Choice-like mechanism

Choice = Simple (Maybe Integer) (Maybe Integer)
       | Complex [ComplexChoice]

ComplexChoice = SingleValue String Integer
              | Range String (Maybe Integer) (Maybe Integer) (Maybe Precision)

Precision = Integer

4. Attached boolean expressions

data ParamVal = ConstantParam String
              | Constant Integer
              | AddValue ParamVal ParamVal
              | SubValue ParamVal ParamVal
              | MulValue ParamVal ParamVal

data Constraint = AndConstraint Constraint Constraint
                | OrConstraint Constraint Constraint
                | NotConstraint Constraint
                | ParamValGE ParamVal ParamVal
                | ParamValGT ParamVal ParamVal
                | ParamValLT ParamVal ParamVal
                | ParamValLE ParamVal ParamVal
                | ParamValEQ ParamVal ParamVal
                | TrueConstraint
                | FalseConstraint

5. Add embedded offline computation operators to extended Marlowe (in addition to previous constraint mechanisms)
These would be analogous to Value and Observation but they would only use values that can be determined before execution (like constants and constant parameters), and they would be simplified before deployment, thus reducing contract size.

[bwbush]

In the long term, I think we'll need to change Core Marlowe so that is supports relative events and time arithmetic. The approach "3. Attached generative expression" would probably be most compatible with that future change. I'm unsure about using units like days, months, and years since these might be problematic due the the quirks of calendars, leap seconds, etc.

[bwbush]

There might be another alternative for ConstantParam: the normal Value, Observation, and Let constructions could be used, but we could change the implementation of toCore so that is evaluates all Value, Observation, and Let that can be done statically, and then outputs the Core contract with those computations eliminated.

[palas]

Nice, I like this idea. Yves is currently doing the simplification as part of ACTUS generation, and probably shouldn't have to worry about it.

[palas]

And we still could use a way of implementing the constraints in addition to that