Remove module overriding

[Cameron-Low]

As a fix for #380, disallow all ways of overriding a module when cloning a theory.
Note: this will most likely break some existing proofs.

[fdupress]

No issue with SHA3 (as expected). Kyber, Dilithium, XMSS remain to be checked—I expect XMSS to be edgy.

Coming up with generic fixes to proofs that did (hopefully soundly) rely on module merging is going to take a bit, so we might not want to wait. Anyone worried about this can stay on release 2023.09 until we have a recipe, IMO.

[mbbarbosa]

I have just fixed Kyber. I found that the code changes would be minimal, if we maintained the syntax for overriding modules with the different interpretation that you override types and operators and keep all copies of the things you can't override lying around. Could this be a less intrusive fix?

[fdupress]

@Cameron-Low what are your thoughts on Manuel's proposal from the point of view of "how hard is this going to be to implement correctly?" (Or its dual "how easy is this going to be to mess up?")

[Cameron-Low]

@mbbarbosa can you check the most recent commit and see if this is the behaviour you were after. (sorry for the delay)

[Cameron-Low]

@mbbarbosa, revisiting this topic. After taking another look at how the implementation of your desired behaviour would go, there are quite a few areas that would need careful thought and overhaul. As a result of this, and some discussions with @fdupress and @strub, sticking with the original plan and outright removing module cloning seems to be the simplest/safest option at present.

[fdupress]

As a supportive side note, we (@MM45, Charlotte and I) now have some evidence that (some of) the valid but edgy behaviours of module overriding can be recovered using the variant of Hoare conseq that transfers invariants through an equiv. (That is, you have an invariant on module M, but you would really like to have it on module M' which is a clone of M. conseq equiv_M_M' (: inv ==> inv) allows you to do that if safe, and in particular if M and M' are truly equivalent.)

I will attempt to document a transition recipe ahead of release.