Decide on in (initial?) TxOut constraint design

[uhbif19]

There are various reasons affecting their design:

• L1 scripts might need different constraints and amount of flexibility allowed. Most important is amount of non-determinism of TxOut needed. Coin-selection does imply it. But is this the only case? Is it only related to ADA inputs, or other tokens might need it as well?
• Another flexibility concern are double-satisfaction, and other attacks related to on-chain checking of some kind of constraints by default.
• Various backends might support only some subset of constraints, especially L1 indexing
• L1 code, while supporting probably anything, might have performance considerations
• Constraint translation/optimization and model-checking might be simpler to do

Options to decide:

• Constraints might have some "normal form" or might not. It depends on if there is representation, which is "best" for all purposes.
• Various features or might not be needed. While more powerful features might subsume others, so it might be better to have them.
• Amount of non-determinism allowed, and if it should be handled generically or in some specific cornercase.

Sources to take a look for:

• Another constrain languages and their issues with them: plutus-apps, CTL. Same with on-chain languages like plutarch.
• Usecases: on-chain scripts and specs
• BMC and constraint languages projects

[uhbif19]

My current idea of constraint primitives is:

• Atomic TxOut filtering predicates: by address, Datum, etc.
• Their combinations by any logical operators, including imply.
• exists_n, forall quantifiers over that