trait spec functions and overriding

[tjhance]

Issue #1781 has prompted me to think more about the current design for spec functions and traits. Currently, the design is that all trait functions are overridable, including spec functions. However, this leads to confusions like the one in the issue.

It's worth noting that the requires and ensures of exec and proof functions cannot be overriden. I would argue that the bodies of specification functions are conceptually in the same bucket as requires and ensures clauses.

Now, there are some use-cases for overridable default spec functions. However, I think these use-cases are the minority.

I propose that we both:

• Add an option to make trait spec functions not-overridable
• Make not-overridable the default.

Thus, there would be a way to mark a trait spec function as 'overridable', which can be applied whenever it has a body. (Being marked uninterp would count for this purpose.)

If the trait spec function has no body, the implementation would be required to provide a body, as it is now.