[Verif] Generalize Formal Contracts

[dobios]

This PR redesigns the recent formal contract ops to allow for them to be used within an arbitrary scope and not just at the level of an entire module. This also removes the need for the verif.instance op.

[fabianschuiki]

This looks reasonable!

One thing that isn't totally clear to me yet is what the basic block arguments do. Are they replaced by symbolic values when the contract is applied? In that case, can you pick any arbitrary number of block arguments since you may need any number of symbolic values to express your contract? Might this be easier to read with a verif.symbolic_value op that you've proposed before?

[dobios]

This looks reasonable!

One thing that isn't totally clear to me yet is what the basic block arguments do. Are they replaced by symbolic values when the contract is applied? In that case, can you pick any arbitrary number of block arguments since you may need any number of symbolic values to express your contract? Might this be easier to read with a verif.symbolic_value op that you've proposed before?

Thanks for the review! The reason I opted for block arguments was because I receive some push-back as to the usefulness of a dedicated symbolic value op, so I chose to use block arguments to generate the ssa values instead. Do you think that restoring the symbolic op is a better idea? I don't think that it will particularly make it easier to convert to btor2 later.

[fabianschuiki]

👍 Sounds good. I guess the two are pretty much equivalent, either an arbitrary list of block arguments that are understood to become symbolic values, or a dedicated op and no block args. Whichever works best -- we can always change things later.