Treat the erased soft keyword as Stainless @ghost

[vkuncak]

Scala 3 has erased definitions: https://dotty.epfl.ch/docs/reference/experimental/erased-defs.html

We can presumably extract erased parameter keyword and map it to Stainless @ghost.

First, introduce ErasedChecks that has require, ensuring, assert, etc. all expecting erased parameters.
We need to keep StaticChecks for legacy reasons.

We should start by writing some code that uses erased instead of ghost and compiles with Scala 3 (even without Stainless).

There are differences between erased, including the fact that var-s are possibly not marked by erased. Still, being able to remove immutable parameters of defs and case classes is already useful, as it allows to not rely on our own ghost code elimination.

[vkuncak]

This example is accepted by Scala 3.5.0, so those erased locals are what we would like to accept as ghost.

import scala.language.experimental.erasedDefinitions

@scala.annotation.experimental
object ErasedTerms1 {

  def takeErased(x: BigInt)(erased y: BigInt): BigInt = {
    x + 1
  }

  def valid1(y: BigInt) = {
    erased val z: BigInt = y + 1
    takeErased(y)(z)
 }.ensuring { _ > y }

  def valid2(y: BigInt) = {
    val z: BigInt = y + 1
    takeErased(y)(z)
 }.ensuring { _ > y }
}