[codex] Preserve outer parameter links in loop invariants

[coord-e]

Summary

• preserve the relationship between non-flow function-argument locals and their OuterFnParam values when binding basic-block parameters
• add paired pass/fail UI coverage for user-supplied loop invariants that refer to function arguments
• document the current equality as an ad-hoc workaround for the invariant syntax limitation

Root cause

A user-supplied loop invariant replaces the inferred basic-block precondition. The current local and its stable function-entry OuterFnParam are then bound independently, so the solver cannot transfer facts between them even though a non-flow local's representation cannot change.

[Copilot]

Pull request overview

This PR addresses a verification soundness/usability gap where user-supplied loop invariants replace inferred preconditions and unintentionally break the link between a function’s entry argument representation (OuterFnParam) and the corresponding “current local” parameter value, preventing fact transfer for non-flow locals.

Changes:

• Add an Env::is_non_flow_local helper to detect locals tracked in the non-flow environment map.
• When binding OuterFnParam basic-block parameters, add an ad-hoc equality assumption to equate the OuterFnParam temp with the current local term for non-flow locals.
• Add paired UI tests demonstrating pass/fail behavior for invariants that refer to function arguments.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.

File	Description
tests/ui/pass/loop_invariant_outer_param.rs	Adds a passing UI test showing an invariant can preserve/prove a postcondition involving a function argument.
tests/ui/fail/loop_invariant_outer_param.rs	Adds a failing UI test showing the postcondition cannot be proven when the invariant does not relate the loop value to the argument.
src/refine/env.rs	Introduces is_non_flow_local to distinguish locals tracked in locals vs flow_locals.
src/analyze/basic_block.rs	Adds a workaround equality assumption to preserve OuterFnParam ↔ current-local linkage for non-flow locals under user invariants.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.