Reject case class fields that reference mutable object-level vals

[Copilot]

Case class val fields whose bodies reference mutable object-level vals (globals in Scala objects) were silently accepted as pure, producing unsound verification results. The root cause: val c = Counter(0) in an object is extracted as def c(): Counter = Counter(0) — a zero-argument pure function — so effects(fd.fullBody) for val y = c.next() returns empty, bypassing the existing purity check.

object Test:
  case class Counter(var x: BigInt):
    def next(): BigInt = { val old = x; x = x + 1; old }
  val c = Counter(0)
  case class A(x: BigInt):
    val y = c.next()   // used to be silently accepted — now rejected
  def main() =
    val obj = A(10); val obj2 = A(10)
    assert(obj == obj2)   // TRUE
    assert(obj.y == obj2.y)  // SHOULD BE FALSE, but Stainless said TRUE

Changes

• ast/Definitions.scala — New IsModuleVal flag ("moduleVal") to mark object-level val definitions, plus its extractFlag entry.
• ast/Deconstructors.scala — Deconstruct/reconstruct case for IsModuleVal so the flag survives all pipeline transformations.
• CodeExtraction.scala (extractStatic) — Appends IsModuleVal to the flags of both ExNonCtorFieldDef and ExLazyFieldDef extracted from objects.
• EffectsChecker.scala (checkMutableField) — Added a preTraversal pass over the field body: any FunctionInvocation to a function carrying IsModuleVal whose return type is mutable now throws ImperativeEliminationException, rejecting the program with a clear error message.
• frontends/benchmarks/extraction/invalid/MutableModuleValField.{scala,check} — Negative test reproducing the issue.

[CLAassistant]

Thank you for your submission! We really appreciate it. Like many open source projects, we ask that you sign our Contributor License Agreement before we can accept your contribution.
_{You have signed the CLA already but the status is still pending? Let us recheck it.}