Investigate closure variable capture semantics in MIR

Context

While reviewing code in PR #657 (related to struct field access), a question arose about how closures capture variables from their enclosing scope in MIR semantics.

Current State

Currently, the test file kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs shows a closure that takes a struct reference as an explicit parameter:

let get_value = |struct_ref: &MyStruct| {
    struct_ref.data
};

Investigation Needed

We should investigate how MIR handles closures that capture variables from their enclosing scope, such as:

let struct_list = [/* ... */];
let get_value = |i: usize| { 
    struct_list[i].data  // Capturing struct_list in the closure
};

Tasks

• Research how MIR represents variable capture in closures
• Test different closure capture scenarios (by value, by reference, by mutable reference)
• Document the semantics of closure captures in MIR
• Add test cases for various closure capture patterns
• Verify that our MIR semantics correctly handles all capture modes

Questions to Answer

1. How does MIR differentiate between different capture modes?
2. What are the memory/ownership implications of captures?
3. How are captured variables represented in the MIR closure environment?
4. Are there any edge cases or limitations we need to be aware of?

Related Files

• kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs
• kmir/src/tests/integration/data/run-rs/closures/closure-args.rs
• kmir/src/tests/integration/data/run-rs/closures/closure-no-args.rs

Priority

Medium - This is not blocking current work but would improve our understanding and coverage of Rust's closure semantics.

Source

This investigation was prompted by a comment in PR #657: https://github.com/runtimeverification/mir-semantics/pull/657#pullrequestreview-3142664083

Start by reading kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs and the closure cases in kmir/src/tests/integration/data/run-rs/closures/closure-args.rs and closure-no-args.rs. Compare the existing behavior with by-value, by-reference, and by-mutable-reference capture scenarios. Done means the capture semantics and limitations are documented, representative tests are added, and the MIR handling is verified.