Allow field(0) projection as a no-op when target value is a PtrLocal (#871)

The change in #811 allows pointer casts between pointers to data and
pointers to "transparent wrapper structs" containing one field with the
same data. While the code tries to insert `field(0, _)` projections when
casting, this remediation falls short when the cast pointer is of a
second degree, i.e., a pointer to a pointer.
An example of this can be observed in `Iterator<_>::next`, where a
pointer `**T` is cast to a pointer `*NonNull<T>`, `NonNull` being one of
these "transparent wrapper structs".

The proposed code change allows for a `field(0, _)` projection to be
treated as a No-Op when applied to a non-aggregate (nor union),
specifically a `PtrLocal` for the case of `next()`.

This fixes `iter.next()` for cases where `Some(element)` is returned.
The case where it returns `None` is a separate issue tested but not
fixed here.

Author: jberthold

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

@@ -450,6 +450,26 @@ This is done without consideration of the validity of the Downcast[^downcast].
        </k>
 ```
 
+In context with pointer casts, the semantics handles the special case of a _transparent wrapper struct_:
+A pointer to a struct containing a single element can be cast to a pointer to the single element itself.
+While the pointer cast tries to insert and remove field projections to the singleton field,
+it is still possible that a field projection occurs on a value which is not an Aggregate (nor a union).
+This necessitates a special rule which allows the semantics to perform a field projection to field 0 as a Noop.
+The situation typically arises when the stored value is a pointer (`NonNull`), therefore the rule is restricted to this case.
+The context is populated with the correct field access data, so that write-backs will correct the stored value to an Aggregate.
+
+```k
+  rule <k> #traverseProjection(
+             DEST,
+             PtrLocal(_, _, _, _) #as VALUE,
+             projectionElemField(fieldIdx(0), TY) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, VALUE, PROJS, CtxField(variantIdx(0), ListItem(VALUE), 0, TY) CTXTS) ... </k>
+    [preserves-definedness, priority(100)]
+```
+
+
 #### Unions
 ```k
   // Case: Union is in same state as field projection

kmir/src/tests/integration/data/prove-rs/iter_next_1.rs

@@ -0,0 +1,15 @@
+struct Thing { payload: u16 }
+
+fn main() {
+    let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload: 3}];
+
+    let mut i = a.iter();
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 1);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 2);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 3);
+    // let elem = i.next();
+    // assert!(elem.is_none());
+}

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

@@ -0,0 +1,15 @@
+struct Thing { payload: u16 }
+
+fn main() {
+    let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload: 3}];
+
+    let mut i = a.iter();
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 1);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 2);
+    let elem = i.next();
+    assert!(elem.unwrap().payload == 3);
+    let elem = i.next();
+    assert!(elem.is_none());
+}

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

@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (1990 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio
+    span: 146
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/test_integration.py

@@ -58,6 +58,7 @@
     'iterator-simple-fail',
     'unions-fail',
     'transmute-maybe-uninit-fail',
+    'iter_next_2-fail',
 ]