[Bug] [kprove] - Michelson Multisig Test Regression

[sskeirik]

Test Regression Information

The Michelson semantics has not been updated for a long time because some kprove tests would fail on newer versions of K.
In order to update the K submodule of K-Michelson, a few tests were disabled on CI.
We want to fix and re-enable these tests.
This issue contains information about how to run the tests (both the K versions and Michelson versions).

Here is the version information:

Prev K Submodule Commit/Version: bf17ff1 (v5.1.64)
Prev Michelson Commit (HEAD^): runtimeverification/michelson-semantics@ea0a99c

Curr K Submodule Commit/Version: b725ebd (v5.2.4)
Curr Michelson master Commit (HEAD): runtimeverification/michelson-semantics@d4b9cc89d

The test in question can be run on either Michelson commit by doing the following:

git clone https://github.com/runtimeverification/michelson-semantics/
cd michelson-semantics
git checkout <version-number>
git submodule update --init --recursive -- ext/k
make deps-k build-prove
make tests/proofs/multisig-spec.md.prove

In order to more easily test K-Michelson against both versions of K, I recommend checking out the michelson-semantics repo into two separate git worktrees.

Additional Info

This test made use of smt-lemma in a way that is no longer supported.
Either the usage of smt-lemma needs to be replaced or the semantics needs to be updated to properly support the modern smt-lemma restrictions.

[ehildenb]

Related: #2327 #2328 #2329 #2330 #2331 #2332