[SwayamInSync]

A spec's checks did not look inside the body of a cppverify::choose it applies, which cost two things.

A reads clause over a choice failed, although it holds:

cv::spec int index_of(const int *a, int n, int x)
  cv::reads(a, n)
{
  return cv::choose(k, 0, n, a[k] == x);
}

error: spec reads failed: index_of (calls choose, which reads the heap without a reads clause)

and every proof that used the frame was Unresolved with reason spec.reads. The reads check treated the lifted choice as a heap-reading callee without a reads clause.

A postcondition proved by induction could not use the hypothesis at a call inside a choose:

cv::spec int bit_unblocked(int n)
  cv::decreases(n)
  cv::post(n < 0 || cv::result == cv::choose(k, 0, 2, k == n % 2))
{
  return n <= 1 ? n : cv::choose(j, 0, 2, j == bit_unblocked(n - 2));
}

This stayed Unresolved (spec.fuel) after 35 s. SpecBodyCollector, which gathers the loads and applications of a spec body for its reads, postcondition, and termination checks, stopped at the choice's application.

The change: at the application of a choice, SpecBodyCollector walks the choice's witness body (choiceWitness, as the recursion check already does since the choose recursion fix), at the application's arguments and with its binder as an enclosing quantifier. The collector owns the witness, since its sites point into it. The reads check then checks every load of the body against the declared cells at every binder value, as Dafny checks the reads of a let-such-that, and skips the choice callee itself, whose loads are now sites of their own. A choice whose witness cannot be built makes the check unsupported rather than skipping it. The postcondition checks get the induction hypothesis and the other specs' postconditions at the applications inside the body.

Docs: the reads section of the language reference shows a choose inside a frame and one that reads past it (index_past, with its counterexample). ch13 shows bit and why the hypothesis proves it. The release notes get an entry under "Failures that were not real".

Testing: Verify/suite/choose_reads.cpp covers the reads of index_of (verified) and index_past (fails at n = 0); a frame kept across a write elsewhere, for a hidden spec and for a recursive one; and a write inside the frame, which fails with a counterexample. In choose_axioms.cpp, bit_unblocked is now verified, in 0.4 s. Both fail on main. Two mutations each fail choose_reads.cpp:

• Walking nothing but still skipping the choice makes index_past's reads check verify. That is the unsound one.
• Walking without skipping fails index_of.

Checked: Verify suite 424 passed, 1 unsupported; VerifyTests 60 passed, 1 skipped (encoding parity, which needs archives). Together with #44, in a build with assertions, the Verify suite passes (425, 1 unsupported). A verdict differential against main over 431 Verify sources (the ULEB128 exhaustive decoder left out: it has no choose, and the change runs only at a choice's application) changes only the two test files above.

With #44 as well, a write elsewhere also keeps a non-recursive spec over a choice, which is inlined and so has no application left for its frame to apply to.