Refinements on fields of nested classes depend on declaration order and on field names. Real code often puts helper classes (runnables, DTOs) at the bottom of the file, so this comes up when verifying real-world examples (see #308, fixed by #314 for field writes).

The root cause is that fields are registered only in the second pass, in source order. They are stored under a name-only key (this#<name>), and the variable context is reset whenever any class is entered, nested classes included.

Sub-issues track the specific cases:

• Reading a field of a class declared later in the file loses its refinement #316 Field reads of a class declared later lose its refinement
• Nested classes wipe the outer class's field refinements #317 Nested classes wipe the outer class's field refinements
• Fields with the same name in different classes collide #318 Fields with the same name in different classes collide