vir: catch delayed-init reassignment for ghost/tracked locals

[Marti2203]

Fixes #2865.

let ghost x = ...;/let tracked x = ...; at exec-top-level (per #1169/#2864) desugars into let x; (no VIR-level initializer) followed by a separate assignment establishing the value - true whether or not the user wrote a surface-level = <expr>. The existing check in simplify_one_expr looks up a ScopeEntry whose init flag is set once, statically, from whether the declaration statement itself had an initializer - so for this desugared shape, init is false forever, and every assignment (not just the first) looks like a legitimate first-time initialization. A real reassignment like:

let ghost x = X { };
proof { x = X { }; }

was silently accepted instead of requiring mut, exactly as @tjhance found reviewing #2864.

Fix: a new DelayedInitChecker (in ast_simplify.rs) walks each function, tracking, per straight-line execution path, whether a no-initializer/non-mut variable has already consumed its one free "this is the initial value" assignment. It runs as its own separate pass rather than extending simplify_one_expr's existing check, specifically so it can be control-flow aware: each branch of an if/match/loop body starts with a fresh, empty "already assigned" set, not a copy of whatever was already true on the path leading into it.

The tradeoff: wrapping a real reassignment in a trivial if true { x = ...; } would dodge this check - acceptable given the existing check's own documented scope ("no longer needed for soundness... nonetheless picks up a few situations... much of the time caught by borrowck anyway").

Updated three existing tests whose comments/TODOs already anticipated this exact fix:

• modes.rs's decl_init_let_spec_fail2.
• modes.rs's decl_init_let_spec_fail/_fail3.
• lifetime.rs's assign_twice_no_lifetime; its sibling test_no_lifetime_mut_check already exercises the identical design intent for a different pattern.

Verified:

• vstd still verifies fully (2045 verified, 0 errors).
• Ran the complete rust_verify_test suite (141 of 142 test files - cargo.rs excluded, unrelated environment/sandboxing limitation) twice (once before, once after fixing the branch-independence bug found via proph.rs) with zero regressions both times,
• plus the full 149-example suite with zero failures.

Assisted-by: Claude Code:claude-sonnet-5

_{By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license (https://github.com/verus-lang/verus/blob/main/LICENSE).}

[tjhance]

I have to think about this one ...

This analysis is difficult to do accurately; it's not really possible with this kind of straightforward traversal. You need a full-fledged CFG like resolution_inference uses, but I also don't want to modify resolution_inference for this bug, since resolution_inference is already very complex and soundness-critical, whereas this issue simply isn't very important.

I'm tempted to say "good is better than perfect" on this one, but I also want to think about exactly what that entails ... I'd advise not spending much time on this until I come to a conclusion.

[Marti2203]

Hi @tjhance! I can leave it as a draft PR if you want to make it clear for subsequent views. I fully understand not spending time on this; this is just a minimal check implementation, and if borrowck can capture it, it is not too bad. Thanks for the feedback!