Relate OuterFnParam to locals via FnParam::at_here in loop invariants

[coord-e]

Follow-up to #150.

Problem

A user-supplied loop invariant replaces the inferred precondition, so the relationship between a function argument's entry value (OuterFnParam) and its current local at the loop header is no longer carried. #150 patched this by adding an ad-hoc equality on non-flow OuterFnParams. That equality is valid (it always holds for non-flow locals), but ad-hoc: its behavior implicitly changes with the binding's type/mutability, and the invariant cannot express both views of the same argument.

Fix

Let invariants relate the two views explicitly, instead of relying on an implicit equality:

• FnParam::at_here() denotes the argument's current local at the loop header, as opposed to at_entry() (its value at function entry — the OuterFnParam). FnParam itself stays a single value (the entry value, unchanged); at_here() resolves to the argument's separate loop-header local. Concretely, in the lowered formula each invariant parameter i carries its entry value at variable i and its "here" value at variable params.len() + i, and build_invariant_precondition wires the latter to param_of_local. No tuple/new sort is introduced.
• FnParam::is_not_changed() is at_entry() == at_here() — the explicit form of what [codex] Preserve outer parameter links in loop invariants #150 asserted implicitly.
• Referring to a function parameter's local directly (without FnParam) in an invariant signature is now an error, so the entry-vs-current choice is always explicit. self is exempt: it is loop-carried and denotes its current value.

The ad-hoc equality (and is_non_flow_local) are removed.

With this, the #150 case reads:

#[thrust_macros::ensures(result == a)]
#[thrust_macros::invariant_context]
fn keep_argument(a: i64) -> i64 {
    let mut v = a;
    while rand() {
        thrust_macros::invariant!(|a: FnParam<i64>, v: i64| a.is_not_changed() && v == a.at_here());
        v = a;
    }
    v
}

Tests

All new tests come in pass/fail pairs:

• loop_invariant_outer_param — the [codex] Preserve outer parameter links in loop invariants #150 case (immutable argument): is_not_changed() + at_here() discharges result == a; dropping is_not_changed() fails.
• loop_invariant_fn_param_at_here — argument reassigned in the loop (a += 1): at_here() differs from at_entry(); at_entry() <= at_here() discharges result >= a, while claiming is_not_changed() correctly fails.
• loop_invariant_fn_param_at_here_mut_borrow — argument mutably borrowed in the loop (flow-bound: let r = &mut a; *r += 1), the canonical case where at_here() != at_entry(); same pass/fail shape.
• loop_invariant_fn_param_direct — referring to a parameter directly is rejected (fail) vs. the same program written with FnParam (pass).
• Updated the generic invariant tests that referred to a parameter directly to use FnParam + at_here().

Notes

cargo fmt/cargo clippy -D warnings are clean. The full suite passes except tests/ui/fail/option_map.rs, which hangs in this sandbox only — its PCSat (COAR) solver run does not terminate here, and that test uses no invariants/FnParam, so it is unaffected by this change. Worth a confirming CI run.

🤖 Generated with Claude Code

https://claude.ai/code/session_01KKHXf7J5gPQ7uHvnehQsTd