fix(rt): remove mutability guard on local variable assignment

[Stevengre]

Summary

Remove the mutabilityOf(...) ==K mutabilityMut guard from #setLocalValue in rt/data.md. MIR's LocalDecl::mutability is a source-level annotation, not an assignment constraint — the Rust compiler validates legality before emitting MIR and may reuse immutable locals across loop iterations.

• Remove mutability guard from the initialized-local #setLocalValue rule
• Preserve original mutability on write (mutabilityOf(...)) instead of forcing mutabilityMut
• Add regression test immutable-local-reassign.rs (loop variable with mutability: Not)

Follow-up: #949 (remove mutability tracking entirely)

Context

A for i in 0..2 loop variable is bound via pattern matching (Some(i)) on each iteration, so rustc marks it as mutability: Not. However, rustc reuses the same MIR local across iterations, producing repeated assignments to an immutable local. This is valid MIR — confirmed via rustc -Z unpretty=mir and the LocalDecl documentation.

Without this fix, proof execution gets stuck at step 693 on #setLocalValue(place(local(8), .ProjectionElems), Integer(1, 64, false)) — the loop counter assignment that no rule can handle.

Proof evidence

Without fix (RED):

APRProof: immutable-local-reassign.main
    status: ProofStatus.FAILED
    stuck: 1, failing: 1

Leaf <k>:
  #setLocalValue(place(local(8), .ProjectionElems), Integer(1, 64, false))
  function: repro

With fix (GREEN):

test_prove_rs[immutable-local-reassign] PASSED (53.31s)

Test plan

• immutable-local-reassign.rs passes with fix, fails (stuck) without fix
• Full integration test suite (make test-integration)

[dkcumming]

The mutability of a Place is not considered when assigning at the MIR level. This is a topic that is currently in some debate amongst the rustc community.

@mariaKt made a post in the stable-mir channel of the Rust zulip where we were informed that mutability is ignored. They directed us to this issue where they discuss if writing to an immutable Local should be considered UB - currently it is not.

Miri evaluates an assignment of a MIR Place by rustc_const_eval interpreter method eval_statement which does not consider mutability at all in the evaluation.

Kani also ignores the mutability of a Local when declaring them for the GOTO C backend as it does not at all read the mutability field of the LocalDecl. Similarly there is no check when for the StatementKind::Assign case for codegen_statement.