A for loop over indices forgets the list's ghost, so i < l.size() does not prove l.get(i) #479

Summary

In for (int i = 0; i < l.size(); i++) l.get(i); the loop condition does not prove the index. Inside the body the list is a new version whose ghost is unconstrained, although the body does not change the list. The condition is kept as i < 2 (the size before the loop), but get needs i < size(l').

Minimal reproducer

ArrayListRefinements.java:

import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.Ghost;
import liquidjava.specification.Refinement;
import liquidjava.specification.StateRefinement;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int size")
public interface ArrayListRefinements<E> {
    @StateRefinement(to = "size(this) == 0")
    void ArrayList();

    @StateRefinement(to = "size(this) == size(old(this)) + 1")
    boolean add(E e);

    E get(@Refinement("_ >= 0 && _ < size(this)") int index);

    @Refinement("_ == size(this) && _ >= 0")
    int size();
}

Client.java:

import java.util.ArrayList;

public class Client {
    public static void main(String[] args) {
        ArrayList<String> l = new ArrayList<>();
        l.add("a");
        l.add("b");
        for (int i = 0; i < l.size(); i++) {
            String s = l.get(i);   // Refinement Error
        }
    }
}

Output on main at 19991d3:

Refinement Error: #fresh == 2 && #fresh >= 0 && i < #fresh is not a subtype of i >= 0 && i < size(l)

Expected: Correct! Passed Verification. Two things seem to combine: i >= 0 is not carried into the body (no loop invariant), and the list's ghost is forgotten at the loop head even though nothing in the loop modifies l. I understand the forgetting comes from the soundness fixes for loops (#338, #427); keeping the ghost of objects the body never calls a state-changing method on would keep those fixes and accept this.

Seen on 1a506fe and main at 19991d3.

Why it matters: real code

This is the commonest way to walk a list. A spec that tracks a list's size (so that get(0) on an empty list is caught) rejects every such loop. Mined example: agileuml Ocl.min, for (int i = 1; i < slist.size(); i++) { T val = slist.get(i); ... }.

Found while writing an ArrayList spec (liquid-java/co-specification, verifier probe V37).