Loop scope rule doesn't include implicit conditions on local variables

[FliegendeWurst]

As discussed in a meeting, the loop scope rule needs to be adjusted to include the implicit conditions on local variables, e.g. inInt(iter) and list = null | list.<created> = TRUE

Discussed in #3727

^{Originally posted by FliegendeWurst January 27, 2026}
I'm having trouble proving a method that is similar to the below.

import java.util.List;
import java.util.ArrayList;

public class LoopList {
    /*@ public normal_behavior
      @ ensures \result >= 0;
      @*/
    static int reassignList() {
        int iter = 0;
        List list = new ArrayList();
        list.add(new Object());
        /*@ loop_invariant
          @  list != null
          @  && \invariant_for(list)
          @  && iter >= 0
          @  && iter <= 20
          @ ;
          @ decreases 20 - iter;
          @ assignable list, iter;
          @*/
        while (!list.isEmpty() && iter < 20) {
            list = new ArrayList();
            iter++;
        }
        return iter;
    }
}

The problem is that I want to use list in the loop condition, but I can't close the Pre (isEmpty) branch. I get stuck on ==> list_0.<created>@heapAfter_add[anon({}, anon_heap_LOOP_0)]. I've tried adding list.<created> to the loop invariant, but that is a syntax error. How can I track the createdness of list in the invariant?

[WolframPfeifer]

A bit more information from the meeting(s): In contrast to the loop scope rule, the loop transformation rule correctly produces the necessary update list = null | list.<created> = TRUE. Note that also inInt(iter) is added there, which is also missing for the loop scope rule.

This is probably also related to #3720, where the anonymization of local ghost variables does not occur as needed. However, #3720 affects both loop rules.

Note that since both iter and list are local variables, it is not necessary to list them in the assignable clause. Instead, they are (or should be, at least) inferred by a static check (something like "occurs on the left-hand side of an assignment"). Apparently, this does not work correctly with the loop scope rule in general, and not correctly for set statements in the transformation loop rule.

[WolframPfeifer]

@unp1 Certainly, you have more knowledge than I for the loop scope rules. Can you take a look here?