Add support for accessing single-element aggregates in #traverseProjection (#657)

- Updated documentation to explain how to directly access elements of an
Aggregate when #traverseProjection becomes stuck.
- Introduced a new rule for handling single-element aggregates in the
semantics.
- Added a new test case for closure access to a struct, ensuring correct
behavior.
- Updated integration tests to include the new failure case for closure
access to structs.

Author: Stevengre

.gitignore

@@ -4,4 +4,5 @@ __pycache__/
 /deps/.stable-mir-json
 /.vscode/
 kmir/src/tests/integration/data/**/target
-.DS_Store
+.DS_Store
+proof/

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

@@ -418,6 +418,30 @@ This is done without consideration of the validity of the Downcast[^downcast].
        </k>
 ```
 
+If an Aggregate contains only one element and #traverseProjection becomes stuck, you can directly access this element.
+
+Without this rule, the test `closure_access_struct-fail.rs` demonstrates the following behavior:
+- The execution gets stuck after 192 steps at `#traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( ... ) ) , ... )`
+- The stuck state occurs because there's a Deref projection that needs to be applied to the single element of this Aggregate, but the existing Deref rules only handle pointers and references, not Aggregates
+
+With this rule enabled:
+- The execution progresses further to 277 steps before getting stuck
+- It gets stuck at a different location: `#traverseProjection ( toLocal ( 19 ) , thunk ( #decodeConstant ( constantKindAll ... ) ) , ... )`
+- The rule automatically unwraps the single-element Aggregate, allowing the field access to proceed
+
+This rule is essential for handling closures that access struct fields, as MIR represents certain struct accesses through single-element Aggregates that need to be unwrapped.
+
+```k
+  rule <k> #traverseProjection(
+             DEST,
+             Aggregate(_, ARGS),
+             PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, getValue(ARGS, 0), PROJS, CTXTS) ... </k>
+    requires size(ARGS) ==Int 1 [preserves-definedness, priority(100)]
+```
+
 #### Ranges
 
 An `Index` projection operates on an array or slice (`Range`) value, to access an element of the array.

kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs

@@ -0,0 +1,25 @@
+struct MyStruct {
+    data: i32
+}
+
+fn main() {
+    // List of MyStruct instances
+    let struct_list = [
+        MyStruct { data: 10 },
+        MyStruct { data: 20 },
+        MyStruct { data: 30 },
+        MyStruct { data: 40 },
+        MyStruct { data: 50 }
+    ];
+    
+    // Closure function that takes &MyStruct reference
+    let get_value = |struct_ref: &MyStruct| {
+        struct_ref.data
+    };
+    
+    // Use list call style, passing reference
+    let result = get_value(&struct_list[2]);
+    
+    // Verify result
+    assert_eq!(result, 30);
+}

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

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (277 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 19 ) , thunk ( #decodeConstant ( constantKindAll
+    function: main
+    span: 106
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/test_integration.py

@@ -52,6 +52,7 @@
     'checked_arithmetic-fail',
     'offset-u8-fail',
     'pointer-cast-length-test-fail',
+    'closure_access_struct-fail',
 ]