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

## 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](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.LocalDecl.html).

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

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

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -177,21 +177,23 @@ In contrast to regular write operations, the value does not have to be _mutable_
 ### Setting Local Variables
 
 The `#setLocalValue` operation writes a `Value` value to a given `Place` within the `List` of local variables currently on top of the stack.
-This may fail because a local may not be accessible or not mutable.
 If we are setting a value at a `Place` which has `Projection`s in it, then we must first traverse the projections before setting the value.
 A variant `#forceSetLocal` is provided for setting the local value without checking the mutability of the location.
 
+**Note on mutability:** The Rust compiler validates assignment legality and may reuse immutable locals in MIR (e.g., loop variables), so `#setLocalValue` does not guard on mutability.
+
+TODO: `#forceSetLocal` is now functionally identical to `#setLocalValue` and may be removed.
+
 ```k
   syntax KItem ::= #setLocalValue( Place, Evaluation ) [strict(2)]
                  | #forceSetLocal ( Local , Evaluation ) [strict(2)]
 
   rule <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>
        <locals>
-          LOCALS => LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)]
+          LOCALS => LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityOf(getLocal(LOCALS, I)))]
        </locals>
     requires 0 <=Int I andBool I <Int size(LOCALS)
      andBool isTypedValue(LOCALS[I])
-     andBool mutabilityOf(getLocal(LOCALS, I)) ==K mutabilityMut
     [preserves-definedness] // valid list indexing checked
 
   rule <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>

kmir/src/tests/integration/data/prove-rs/immutable-local-reassign.rs

@@ -0,0 +1,11 @@
+fn main() {
+    let _ = repro();
+}
+
+fn repro() -> usize {
+    let mut out = [0usize; 2];
+    for i in 0usize..2usize {
+        out[i] = i;
+    }
+    out[1]
+}

kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected

@@ -49,14 +49,15 @@
       │   #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K
       │   function: main
       │
-      │  (17 steps)
-      └─ 11 (stuck, leaf)
-          #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems )
-          function: main
-          span: 79
-
+      │  (66 steps)
+      ├─ 11 (terminal)
+      │   #EndProgram ~> .K
+      │   function: main
+      │
+      ┊  constraint: true
+      ┊  subst: ...
+      └─ 2 (leaf, target, terminal)
+          #EndProgram ~> .K
 
-┌─ 2 (root, leaf, target, terminal)
-│   #EndProgram ~> .K