ghost fields can lead to different runtime behaviour when using equality

[samuelchassot]

Equality on classes with ghost fields does not ignore ghost fields, which can lead to different behaviour at runtime than verification.
For example:

import stainless.collection.*
import stainless.annotation.*
import stainless.lang.{ghost => ghostExpr, *}

object GhostEqTest:
  case class C(x: Int, y: Int, @ghost z: Int)

  def f(c1: C, c2: C): Unit = {
    require(c1.x == c2.x)
    require(c1.y == c2.y)

    if(c1 == c2){ // Here you in fact use z in a non-ghost context!!!!
      assert(c1.x == c2.x)
    } else{
      // it is possible: c1.x == c2.x && c1.y == c2.y
      // /!\
      assert(false) // Counterexample: C(0, 0, 0) and C(0, 0, 1)
    }
    // ghostExpr(assert(c1.z == c2.z))
  }

end GhostEqTest

This issue has been discovered based on the discussion I had with Jean-Christophe Filiâtre.

It seems related to #460

[samuelchassot]

The best solution is not clear to me for now.
We can consider equality on ghost to be ghost. This would however limit the use of ghost fields significantly.
Another option might be to ignore the ghost fields for structural equality, but it might lead to non-intuitive reasoning.