update from origin/master branch (#852)

- #850

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

@@ -60,6 +60,18 @@ Definedness of the list and list elements is also guaranteed.
   rule #Ceil(#mapOffset(L, _)[I]) => #Ceil(L) #And {true #Equals 0 <=Int I} #And {true #Equals I <Int size(L)} [simplification]
 
   rule #Ceil(#mapOffset(L, _)) => #Ceil(L) [simplification]
+
+  rule #adjustRef(VAL:Value, 0) => VAL [simplification]
+
+  rule #adjustRef(#adjustRef(VAL, OFFSET1), OFFSET2)
+    => #adjustRef(VAL, OFFSET1 +Int OFFSET2)
+    [simplification]
+
+  rule #mapOffset(L, 0) => L [simplification]
+
+  rule #mapOffset(#mapOffset(L, OFFSET1), OFFSET2)
+    => #mapOffset(L, OFFSET1 +Int OFFSET2)
+    [simplification]
 ```
 
 ## Simplifications for Int
@@ -196,4 +208,4 @@ Finally, the magnitude of a value converted from bytes is known to be within the
 
 ```k
 endmodule
-```
+```

kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected

@@ -41,14 +41,14 @@
    ┃  │
    ┃  │  (6 steps)
    ┃  ├─ 10
-   ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( #mapOff
+   ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset (
    ┃  │   span: 87
    ┃  ┃
    ┃  ┃ (1 step)
    ┃  ┣━━┓
    ┃  ┃  │
    ┃  ┃  ├─ 11
-   ┃  ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset (
+   ┃  ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( range ( #map
    ┃  ┃  │   span: 87
    ┃  ┃  │
    ┃  ┃  │  (113 steps)
@@ -59,7 +59,7 @@
    ┃  ┗━━┓
    ┃     │
    ┃     └─ 12 (stuck, leaf)
-   ┃         #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( #mapOff
+   ┃         #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset (
    ┃         span: 87
    ┃
    ┗━━┓