Impact: correct code is rejected (false error) whenever a method's return refinement mentions its parameters and the call is an operand of an expression. Found while addressing a review comment on #400.

Description

OperationsChecker (the invocation case of operand refinements) takes the function's refinements via RefinedFunction.getRenamedRefinements, which renames each parameter to its last instance rather than to the call's arguments. When the call is an operand (inc(2) + 1), the parameters are never bound to the arguments, so the return refinement keeps the bare parameter name. The same call assigned directly (int k = inc(2);) works.

Minimal reproducer

import liquidjava.specification.Refinement;

class Inc {
    @Refinement("_ == x + 1")
    static int inc(int x) { return x + 1; }

    @Refinement("_ == length(xs)")
    static int size(int[] xs) { return xs.length; }

    void m() {
        @Refinement("_ == 4") int k = inc(2) + 1;
        int[] arr = new int[2];
        @Refinement("_ == 3") int j = size(arr) + 1;
    }
}

Expected

Correct! Passed Verification.

Actual (main ad055b4)

Refinement Error: k⁷ == x + 2 is not a subtype of k⁷ == 4

Possible fix

For an invocation operand, check the call like a standalone invocation (MethodsFunctionsChecker, which maps arguments to parameters, including spread varargs since #400) and use the resulting refinement of the call, instead of the function's refinements with parameters renamed to their last instances.