Optimal satisfaction algorithm is not modelled

[dgpv]

Early version of the spec had malleable_sat/malleable_dsat and has_sig properties on nodes, but they were specified without full understanding of the satisfaction algorithm, were not correct, and were removed.

It still might be useful to have a specification for the non-malleable satisfaction algorithm. The spec already models instances for valid/empty sigs, correct/wrong preimages, and zero/one witnesses, and models sat/dsat. Would the non-malleable satisfaction algorithm be modelled, an implementations would be able to check against the spec for correctness of their algorithm.

It might make sense to model the algorithm as a separate spec that would import the main spec via open miniscript. Modelling satisfaction algorithm will make the overall model more complex, and therefore it will take more time to check. Having the basic model small will be cheaper. On the other hand, if we have a spec that would correctly detect malleability and has_sig run-time properties, we could check them against s,e,f type modifiers and increase confidence in the consistency of the spec

[dgpv]

The problem with modelling the satisfaction algorithm is that it should chose the optimal satisfaction, and this means choosing between different instances. This means that 'optimal satisfaction' is a hyperproperty, that can't be directly modelled in Alloy. One would have to model all possible non-malleable satisfactions first, and then chose the optimal between them.