[Don't Merge] Reproduce Issues

.gitignore

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

tests/README.md

@@ -0,0 +1,41 @@
+### Reproduce stuck in `entrypoint::test_process_initialize_multisig`
+
+```
+#traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... provSize: 0 , allocId: allocId ( 98 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty ( 500125 ) , typeInfoRefType ( ty ( 500016 ) ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts )
+```
+
+Can be reproduced through `thunk_decode_constant.rs`, see details in `thunk_decode_constant.md`
+
+```
+#traverseProjection ( toLocal ( 8 ) , thunk ( #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... provSize: 0 , allocId: allocId ( 0 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty ( 25 ) , typeInfoRefType ( ty ( 16 ) ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts )
+```
+
+## TypeError: 'NoneType' object is not subscriptable
+
+mock_borrow_data_unchecked.rs
+
+```
+INFO 2025-08-19 13:08:34,055 kmir.cargo - Deleted: /Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/tests/mock_borrow_data_unchecked.smir.json
+Traceback (most recent call last):
+  File "/Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/kmir/.venv/bin/kmir", line 10, in <module>
+    sys.exit(main())
+  File "/Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/kmir/src/kmir/__main__.py", line 451, in main
+    kmir(sys.argv[1:])
+  File "/Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/kmir/src/kmir/__main__.py", line 218, in kmir
+    _kmir_prove_rs(opts)
+  File "/Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/kmir/src/kmir/__main__.py", line 66, in _kmir_prove_rs
+    proof = kmir.prove_rs(opts)
+  File "/Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/kmir/src/kmir/kmir.py", line 186, in prove_rs
+    smir_info = smir_info.reduce_to(opts.start_symbol)
+  File "/Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/kmir/src/kmir/smir.py", line 156, in reduce_to
+    _LOGGER.debug(f'Reducing items, starting at {start_ty}. Call Edges {self.call_edges}')
+  File "/opt/homebrew/Cellar/[email protected]/3.10.17/Frameworks/Python.framework/Versions/3.10/lib/python3.10/functools.py", line 981, in __get__
+    val = self.func(instance)
+  File "/Users/steven/Desktop/projs/solana-token/p-token/test-properties/mir-semantics/kmir/src/kmir/smir.py", line 183, in call_edges
+    for b in item['mono_item_kind']['MonoItemFn']['body']['blocks']
+TypeError: 'NoneType' object is not subscriptable
+```
+
+## Mock borrow_data_unchecked but encountered different stuck
+
+`mock_borrow_data_unchecked_failed.rs`

tests/closure/closure_array_access.rs

@@ -0,0 +1,15 @@
+fn main() {
+    // Simple data structure
+    let numbers = [10, 20, 30, 40, 50];
+
+    // Keep closure function and list call style
+    let get_value = |index: usize| {
+        numbers[index]
+    };
+
+    // Use list call style
+    let result = get_value(2);
+
+    // Verify result
+    assert_eq!(result, 30);
+}

tests/closure/closure_async.rs

@@ -0,0 +1,28 @@
+// This example demonstrates async closures
+// Note: This requires an async runtime like tokio to actually execute
+
+fn main() {
+    let numbers = [1, 2, 3, 4, 5];
+
+    // Async closure that captures by value
+    let async_process = |index: usize| async move {
+        // Simulate async operation (e.g., network request, file I/O)
+        std::thread::sleep(std::time::Duration::from_millis(10));
+        numbers[index] * 2
+    };
+
+    // Async closure that captures by reference (requires 'static lifetime)
+    let async_process_ref = |index: usize| async move {
+        // This would work if numbers had 'static lifetime
+        // For demonstration, we'll use a different approach
+        index * 2
+    };
+
+    // Note: To actually run these async closures, you would need:
+    // 1. tokio or another async runtime
+    // 2. #[tokio::main] attribute on main function
+    // 3. .await calls to execute the futures
+
+    println!("Async closures defined successfully");
+    println!("To execute: use tokio::spawn(async_process(2).await)");
+}

tests/closure/closure_borrow_checker.rs

@@ -0,0 +1,16 @@
+fn main() {
+    let mut data = vec![1, 2, 3, 4, 5];
+
+    // Test borrow checker
+    let get_value = |index: usize| {
+        data[index]
+    };
+
+    let result = get_value(2);
+    assert_eq!(result, 3);
+
+    // Can modify data because closure only borrows
+    data[2] = 10;
+    let new_result = get_value(2);
+    assert_eq!(new_result, 10);
+}

tests/closure/closure_capture.rs

@@ -0,0 +1,12 @@
+fn main() {
+    let multiplier = 5;
+    let numbers = [1, 2, 3, 4, 5];
+
+    // Closure capturing external variables
+    let multiply_by = |x: i32| {
+        x * multiplier
+    };
+
+    let result = multiply_by(numbers[2]);
+    assert_eq!(result, 15);
+}

tests/closure/closure_complex_capture.rs

@@ -0,0 +1,151 @@
+// Test complex capture patterns
+
+fn main() {
+    // Test 1: Partial move - some fields moved, others borrowed
+    struct Person {
+        name: String,
+        age: i32,
+        scores: Vec<i32>,
+    }
+
+    let person = Person {
+        name: "Alice".to_string(),
+        age: 25,
+        scores: vec![85, 90, 88],
+    };
+
+    // Move name and scores, borrow age
+    let name_and_scores = move || {
+        (person.name, person.scores)
+    };
+
+    let result = name_and_scores();
+    assert_eq!(result.0, "Alice");
+    assert_eq!(result.1, vec![85, 90, 88]);
+
+    // Test 2: Mixed capture - some by value, some by reference
+    let mut counter = 0;
+    let data = vec![1, 2, 3, 4, 5];
+
+    let mixed_closure = move |index: usize| {
+        // data is moved into closure
+        // counter is captured by mutable reference
+        counter += 1;
+        data[index] + counter
+    };
+
+    // This won't compile because counter is captured by reference
+    // but data is moved. Let's fix this:
+
+    let mut counter2 = 0;
+    let data2 = vec![1, 2, 3, 4, 5];
+
+    let mixed_closure2 = |index: usize| {
+        counter2 += 1;
+        data2[index] + counter2
+    };
+
+    let result1 = mixed_closure2(2);
+    let result2 = mixed_closure2(2);
+
+    assert_eq!(result1, 4); // 3 + 1
+    assert_eq!(result2, 5); // 3 + 2
+
+    // Test 3: Closure capturing different parts of a struct
+    struct ComplexData {
+        numbers: Vec<i32>,
+        metadata: String,
+        flag: bool,
+    }
+
+    let complex = ComplexData {
+        numbers: vec![10, 20, 30],
+        metadata: "test".to_string(),
+        flag: true,
+    };
+
+    // Capture numbers by value, metadata by reference
+    let numbers_closure = move || {
+        complex.numbers
+    };
+
+    let numbers_result = numbers_closure();
+    assert_eq!(numbers_result, vec![10, 20, 30]);
+
+    // Test 4: Closure with conditional capture
+    let condition = true;
+    let value1 = vec![1, 2, 3];
+    let value2 = vec![4, 5, 6];
+
+    let conditional_closure = if condition {
+        move || value1
+    } else {
+        move || value2
+    };
+
+    let conditional_result = conditional_closure();
+    assert_eq!(conditional_result, vec![1, 2, 3]);
+
+    // Test 5: Closure capturing enum variants
+    enum Data {
+        Numbers(Vec<i32>),
+        Text(String),
+    }
+
+    let enum_data = Data::Numbers(vec![1, 2, 3]);
+
+    let enum_closure = move || {
+        match enum_data {
+            Data::Numbers(nums) => nums,
+            Data::Text(_) => vec![],
+        }
+    };
+
+    let enum_result = enum_closure();
+    assert_eq!(enum_result, vec![1, 2, 3]);
+
+    // Test 6: Closure with nested captures
+    let outer_data = vec![1, 2, 3];
+    let inner_data = vec![4, 5, 6];
+
+    let nested_closure = move || {
+        let inner_closure = move |index: usize| {
+            outer_data[index] + inner_data[index]
+        };
+        inner_closure(0)
+    };
+
+    let nested_result = nested_closure();
+    assert_eq!(nested_result, 5); // 1 + 4
+
+    // Test 7: Closure capturing tuple with mixed ownership
+    let tuple_data = (vec![1, 2, 3], "hello".to_string(), 42);
+
+    let tuple_closure = move |index: usize| {
+        (tuple_data.0[index], tuple_data.1.clone(), tuple_data.2)
+    };
+
+    let tuple_result = tuple_closure(1);
+    assert_eq!(tuple_result, (2, "hello".to_string(), 42));
+
+    // Test 8: Closure with reference counting for shared ownership
+    use std::rc::Rc;
+
+    let shared_data = Rc::new(vec![1, 2, 3, 4, 5]);
+
+    let rc_closure1 = {
+        let data = Rc::clone(&shared_data);
+        move |index: usize| data[index]
+    };
+
+    let rc_closure2 = {
+        let data = Rc::clone(&shared_data);
+        move |index: usize| data[index] * 2
+    };
+
+    let rc_result1 = rc_closure1(2);
+    let rc_result2 = rc_closure2(2);
+
+    assert_eq!(rc_result1, 3);
+    assert_eq!(rc_result2, 6);
+}