Predicate call in an ISC breaks the 'already-processed complement' postcondition under return-value-threaded recursion (every while loop with this shape)

[wies]

Summary

A while loop whose invariant is an iterated-separating-conjunction (ISC) over a shrinking/growing set, where the ISC's body includes a predicate/invariant call (not just a plain own(...)), fails to verify on one specific postcondition clause -- even when that clause is trivially true and even when the identical logic verifies fine as a hand-written recursive lemma that has no return value.

This isn't specific to while loops as such: it reproduces with a hand-written recursive lemma too, as soon as it has the same shape rewrite_loops always produces for a loop that mutates a loop-carried variable: a return value threading the "remaining" set across the recursive call, combined with a postcondition describing the complement of that returned set. Since rewrite_loops (lib/frontend/rewrites/rewrites.ml) always needs a return value for any loop-carried variable that's mutated in the loop body, every while loop of this shape hits it as soon as its invariant contains a predicate call.

Minimal failing repro (hand-written, no while loop involved)

module M {
  ghost field snap: Int

  inv hps(hcell: Ref) {
    true
  }

  lemma bump_all_manual(n: Int, regs: FinSet[Ref], ghost todo: FinSet[Ref]) returns (ghost todo2: FinSet[Ref])
    requires todo subseteq regs
    requires forall r0: Ref :: r0 in todo ==> own(r0.snap, n, 1.0) && hps(r0)
    requires forall r0: Ref :: r0 in regs && r0 !in todo ==> own(r0.snap, n + 1, 1.0) && hps(r0)
    ensures todo2 subseteq regs
    ensures forall r0: Ref :: r0 in todo2 ==> own(r0.snap, n, 1.0) && hps(r0)
    ensures forall r0: Ref :: r0 in regs && r0 !in todo2 ==> own(r0.snap, n + 1, 1.0) && hps(r0)
    ensures todo2 == {||}
    decreases todo
  {
    todo2 := todo
    if (todo != {||}) {
      ghost val r := choose(todo)
      r.snap := n + 1
      todo := todo -- {|r|}
      todo2 := bump_all_manual(n, regs, todo)
    }
  }
}

Fails with:

Verification Error: A postcondition may not hold at this return point.
  ensures forall r0: Ref :: r0 in regs && r0 !in todo2 ==> own(r0.snap, n + 1, 1.0) && hps(r0)
                                                            ^^^^^^^^^^^^^^^^^^^^^^^^
Related Location: This own predicate may not hold.

Note this clause is the "already-processed" half of the invariant -- it's the one saying every element not still in the leftover set has already been bumped. It's the only clause that fails; todo2 subseteq regs, the "not-yet-processed" clause, and todo2 == {||} all verify fine. Manually asserting this exact fact immediately before/after each mutation inside the loop body also succeeds -- the logic itself is sound, something specific to how this clause gets checked against the returned todo2 (as opposed to the local todo at the point of the assert) is off.

Same shape, but without the return value: verifies fine

Drop the "leftover set" tracking (recurse first, then process the current element only -- the standard trick for this exact pattern, since tail-call efficiency doesn't matter in ghost code) and the whole thing needs only one requires/ensures pair and verifies immediately:

module M {
  ghost field snap: Int

  inv hps(hcell: Ref) {
    true
  }

  lemma bump_all(n: Int, regs: FinSet[Ref])
    requires forall r0: Ref :: r0 in regs ==> own(r0.snap, n, 1.0) && hps(r0)
    ensures forall r0: Ref :: r0 in regs ==> own(r0.snap, n + 1, 1.0) && hps(r0)
    decreases regs
  {
    if (regs != {||}) {
      ghost val r := choose(regs)
      bump_all(n, regs -- {|r|})
      r.snap := n + 1
    }
  }
}

This is a reasonable workaround for hand-written proofs, but a while loop can't be rewritten this way by hand -- rewrite_loops always produces the return-value-threaded shape for a loop-carried variable, so a while loop hits the bug unconditionally whenever its invariant mentions a predicate call.

Original while-loop trigger, for context

module M {
  ghost field snap: Int

  inv hps(hcell: Ref) {
    true
  }

  lemma bump_all_loop(n: Int, regs: FinSet[Ref])
    requires forall r0: Ref :: r0 in regs ==> own(r0.snap, n, 1.0) && hps(r0)
    ensures forall r0: Ref :: r0 in regs ==> own(r0.snap, n + 1, 1.0) && hps(r0)
  {
    ghost var todo: FinSet[Ref] := regs
    while (todo != {||})
      invariant todo subseteq regs
      invariant forall r0: Ref :: r0 in todo ==> own(r0.snap, n, 1.0) && hps(r0)
      invariant forall r0: Ref :: r0 in regs && r0 !in todo ==> own(r0.snap, n + 1, 1.0) && hps(r0)
    {
      ghost val r := choose(todo)
      r.snap := n + 1
      todo := todo -- {|r|}
    }
  }
}

Fails the same way, at the same clause (reported at the while statement's own location, since rewrite_loops synthesizes bump_all_loop_loop from it with exactly the shape of the first repro above).

What's been ruled out

• Not about while loops specifically -- reproduces with a hand-written recursive lemma.
• Not about the predicate call needing unfold/fold in the loop body -- hps's body is the constant true, no explicit unfold/fold needed anywhere in these repros.
• Not about fractional permissions or helping_prot_state-style existentials in the predicate body -- reproduces with own(_, _, 1.0) (full permission) and a trivial { true } predicate body.
• Replacing the predicate call with an unrelated pure conjunct (e.g. n >= 0) instead of hps(r0) verifies fine -- so it's specifically about a predicate/invariant call being part of the ISC's conjunct, not about having an extra conjunct in general.
• The fact itself is provable: explicit asserts of the exact same formula, placed right where the mutation happens, succeed.

Context

Found while filling in a TODO in test/ext/prophecy/dist_counter.rav on the bugfixes branch (an "iterate over a registered set with choose, bumping a per-element ghost field guarded by a per-element invariant" pattern) -- worked around there via the return-value-free recursive-lemma shape above.

Reaching this bug at all required a separate, prerequisite fix, made in the same session (lib/frontend/rewrites/rewrites.ml's rewrite_loops): a while loop inside a ghost block ({! ... !}) previously failed to type-check at all, because the synthesized recursive callable was always a Proc, and Rewriter.enter (lib/ast/rewriter.ml) computes a newly-entered callable's ghost-scope purely from Callable.is_ghost_kind on its own kind, with no way to inherit ghost-ness from the context it was introduced in (unlike enter_block, which does). rewrite_loops now synthesizes a Lemma instead of a Proc whenever the loop itself is in a ghost scope, which is what lets such a loop type-check at all -- this issue is the next, separate problem that surfaces once type-checking succeeds. That fix is not yet on main/pushed as of filing this issue.