Make Stainless specs no-op executable with scalac on JVM

[vkuncak]

Make sure that, when we import StaticChecks, all specification constructs:

• result in a no-op, without crashes or side effects
• have only constant overhead (e.g. due to closure creation), but no asymptotic overhead

This should also apply to all specification constructs that we have. In some cases it may require adding by name parameters.

Consider setting up an execution test suite on our valid benchmarks to check that they are executable.

[vkuncak]

This is partly related to GenC in that some of the constructs were introduced with GenC in mind. But I argue they should still work whenever reasonable on JVM, and otherwise just log an error without crashing.

This would work well with

• https://github.com/epfl-lara/stainless/issues/1276
• https://github.com/epfl-lara/stainless/issues/982

but the broader thing is to make nothing crash.

[vkuncak]

This will probably solved by relying on Scala 3 inline methods: https://docs.scala-lang.org/scala3/guides/macros/inline.html