Allow adding postconditions by mixing in multiple traits

[romac]

@vkuncak Do you have an idea already how that would look like? I am not sure I see how to mix in a trait into an existing class such as List.

[vkuncak]

I don't know. Could we create a new class that mixes a trait into List? Maybe we can just create multiple lists that extend each other, starting from one without postconditions and then adding different kinds of postconditions? Would it help if we separated the interface of List into something like Seq? One can also maybe parameterize a collection with a joinable interface that has ++ that we use to describe effects of operations. But all these things may have costs in terms of efficiency of reasoning; making things more higher order needs to be done with care.

[vkuncak]

Here is a more specific proposal for the feature.

Traits require serialization when we have multiple versions of code. This proposal, however, is primarily concerned with methods that, from stainless point of view are abstract: they only have pre/postconditions, which is our way of encoding Pi types i.e. more precise signatures.

For such traits, if I introduce a class C that mixes in T1 and T2, what I want to say is that a concrete method C.m needs to satisfy the specification of T1.m and of T2.m. Moreover, we should make this work with @law annotations. The effect in all cases is that a class C that mixes in T1 and T2 satisfies all the specifications in T1 and all the specifications in T2.

(As we further improve on these features, we should consider whether lift+verify is the right approach. There has been substantial work on modular verification technology, which should avoid the need for postponing the verification to after lifting phase.)