Perform reads checks on ensures of bodiless functions

[samuelchassot]

What was changed?

• Add reads checks on ensures body for functions without a body. Closes issue Feature/Bug: Ensures clauses of bodiless functions should have reads checks #5822
• Fix the test comp/replaceables/complex/user.dfy: this new feature showed that the specification for these external functions was wrong. For one of the function, a missing reads clause (flagged by this new feature) allowed to derive false. The other function's spec was implying that a function was allocating a new instance (namely of Option<Int32> where Int32 is an extern class), which is forbidden. So we fix these specs by changing them to be methods instead.

How has this been tested?

Add a test to show this new check, update an existing test that includes such a bodiless function with reading ensures and without reads clause.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[samuelchassot]

The failing test comp/replaceables/complex/user.dfy passes locally.
However, the output log here https://github.com/dafny-lang/dafny/actions/runs/15475233860/job/43570694472?pr=6264 brings a good question:

Should this check be performed for {:extern}?

My first answer would be no, especially given that function {:extern} ... are used for API of C#/Java/... external code. For those, the reads clause makes little sense to me.

WDYT?

[robin-aws]

This reads check, and the accuracy of {:extern} specifications in general, is still very important to keep Dafny's reasoning consistent. In this case the reads check is very helpfully pointing out that the existing spec in that test was wrong, and I can actually the old spec to prove false:

  class {:extern "Int32" } Int32 {
    ghost var value: int
  }

  // Current incorrect spec:
  function {:axiom} {:extern} Int32ToInt(value: Int32): int
    ensures Int32ToInt(value) == value.value

  method UhOh(box: Int32) 
    requires box.value < 10  // Just to avoid complaints about overflow
    modifies box
  {
    ghost var before := Int32ToInt(box);
    assert box.value == before;

    box.value := box.value + 1;

    ghost var after := Int32ToInt(box);
    assert before == after;

    assert false;
  }

Because Int32ToInt claims to return the boxed value, but also somehow not to depend on reading the object, Dafny gets confused.

[samuelchassot]

Oh nice one!
So indeed, the reads checks are important here, and this proves this PR useful :)
I'll fix the test

[samuelchassot]

@robin-aws The test is fixed, and I updated the PR's text to mention it.

[robin-aws]

Awesome, love that it pointed out unsoundness in existing specs :)