Description

Fields are keyed in the context by name only (this#<name>), whatever class owns them and whatever the target expression is. Two fields with the same name in different classes (e.g. an outer class and a nested class) are treated as the same variable, so one is checked against the other's refinement.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Collision {
    @Refinement("_ < 0") int port = -1;
    private final Job job = new Job();

    public void send() { job.port = 5; }

    static class Job { @Refinement("_ >= 0") int port; }
}

Expected

Correct! Passed Verification. (Job.port is _ >= 0.)

Actual

Refinement Error: this#port⁴ == 5 is not a subtype of this#port⁴ < 0
5 |     public void send() { job.port = 5; }
  |                          ^^^^^^^^^^^^^

The write to job.port is checked against Collision.port's refinement.

Cause

Field reads and writes use String.format(Formats.THIS, fieldName) (e.g. OperationsChecker, RefinementTypeChecker.visitCtFieldRead), with no owning class or target object. A fix would need to key fields by their declaring type, and ideally separate instances (this.port vs job.port).

Reproduced on main at fbfb4e2 (liquidjava-verifier 0.0.35).