Implement Subslice projection and RawPtr aggregate value (#646)

* Aggregate kind `RawPtr` (`RValue`) takes two arguments, a pointer and
metadata, and creates a new pointer.
  No test program (yet).
* Subslice (`ProjectionElem`) : operates on arrays and slices, extracts
a shorter (possibly empty) slice.
Tested using a small program that matches the tail of a slice using `let
[a, b, c, rest @ ..] = input_slice`.

Both are required for the P-token proofs to progress.

Also copied the description of all projections from the docs into the
actual semantics.

Author: jberthold

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

@@ -211,6 +211,29 @@ A variant `#forceSetLocal` is provided for setting the local value without check
 
 ### Traversing Projections for Reads and Writes
 
+A `Place` to read from or write to is a `Local` variable (actually just its index), and a (potentially empty) vector of `ProjectionElem`ents.
+
+There are different kinds of `ProjectionElem`s:
+- `Deref`erencing references or pointers (or `Box`es allocated in the heap)
+  - read data at the address given in the local
+  - operates on a value that is a pointer or reference to another
+- `Field` access in struct.s and tuples
+  - fields are numbered from zero (in source order). The field type is also given.
+  - operates on structs and tuples
+- `Index`ing into arrays or slices
+  - operates on a value that is an array (statically-known size) or slice (variable size)
+  - indexes zero-based from the front
+  - the index is provided in another local
+- `ConstantIndex`ing with a constant offset
+  - operates on a value that is an array (statically-known size) or slice (variable size)
+  - the index was statically known and is therefore a `u64`
+  - the `min_length` of the object to index into is provided as another `u64`
+  - when `from_end` is true, this is  taken to be exact, and indexing happens from the end
+- `Subslice`
+  - a slice from `from` to `to` (the latter either from start or `from_end`)
+  - operates on a value that is an array (statically-known size) or slice (variable size)
+- Casting values (`OpaqueCast` or `Downcast` - variant narrowing) and `Subtype`ing
+
 Read and write operations to places that include (a chain of) projections are handled by a special rewrite symbol `#traverseProjection`.
 This helper does the projection lookup and maintains the context chain along the lookup path, then passes control back to `#readProjection` and `#writeProjection`/`#setMoved`.
 A `Deref` projection in the projections list changes the target of the write operation, while `Field` updates change the value that is being written (updating just one field of it), recursively.
@@ -278,6 +301,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
   // retains information about the value that was deconstructed by a projection
   syntax Context ::= CtxField( VariantIdx, List, Int )
                    | CtxIndex( List , Int ) // array index constant or has been read before
+                   | CtxSubslice( List , Int , Int ) // start and end always counted from beginning
 
   syntax Contexts ::= List{Context, ""}
 
@@ -294,6 +318,12 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
       => #buildUpdate(Range(ELEMS[I <- VAL]), CTXS)
      [preserves-definedness] // valid list indexing checked upon context construction
 
+  // we don't expect an update to happen on an entire _subslice_ but define a rule for it anyway
+  rule #buildUpdate(Range(INNER), CtxSubslice(ELEMS, START, END) CTXS)
+      => #buildUpdate( Range(updateList(ELEMS, START, INNER)), CTXS)
+    requires size(INNER) ==Int END -Int START // ensures updateList is defined
+     [preserves-definedness] // START,END indexes checked before, length check for update here
+
   syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function]
 
   rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL)
@@ -460,6 +490,52 @@ In case of a `ConstantIndex`, the index is provided as an immediate value, toget
   rule #expectUsize(Integer(I, 64, false)) => I
 ```
 
+A `Subslice` projection operates on an array or slice (`Range`) value to extract a slice of the array from a start index to an end index (exclusive) [^subslice].
+Start and end index are given as immediate values.
+Similar to `ConstantIndex`, the slice _end_ index may count from the _end_  or the start of the array if flagged as such.
+
+[^subslice]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/type.ProjectionKind.html#variant.Subslice
+
+```k
+  rule <k> #traverseProjection(
+             DEST,
+             Range(ELEMENTS),
+             projectionElemSubslice(START, END, false) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(
+             DEST,
+             Range(range(ELEMENTS, START, size(ELEMENTS) -Int END)),
+             PROJS,
+             CtxSubslice(ELEMENTS, START, END) CTXTS
+           )
+        ...
+        </k>
+    requires 0 <=Int START andBool START <=Int size(ELEMENTS)
+     andBool 0 <Int END andBool END <=Int size(ELEMENTS)
+     andBool START <Int END
+    [preserves-definedness] // Indexes checked to be in range for ELEMENTS
+
+  rule <k> #traverseProjection(
+             DEST,
+             Range(ELEMENTS),
+             projectionElemSubslice(START, END, true) PROJS, // END from end of ELEMS
+             CTXTS
+           )
+        => #traverseProjection(
+             DEST,
+             Range(range(ELEMENTS, START, END)),
+             PROJS,
+             CtxSubslice(ELEMENTS, START, size(ELEMENTS) -Int END) CTXTS
+           )
+        ...
+        </k>
+    requires 0 <=Int START andBool START <=Int size(ELEMENTS)
+     andBool 0 <=Int END andBool END <Int size(ELEMENTS)
+     andBool START <=Int size(ELEMENTS) -Int END
+    [preserves-definedness] // Indexes checked to be in range for ELEMENTS
+```
+
 #### References
 
 A `Deref` projection operates on `Reference`s or pointers (`PtrLocal`) that refer to locals in the same or
@@ -725,6 +801,24 @@ Literal arrays are also built using this RValue.
        </k>
 ```
 
+The `AggregateKind::RawPtr`, somewhat as a special case of a `struct` aggregate, constructs a raw pointer
+from a given data pointer and metadata[^rawPtrAgg]. In case of a _thin_ pointer, the metadata is a unit value,
+for _fat_ pointers it is a `usize` value indicating the data length.
+
+[^rawPtrAgg]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.AggregateKind.html#variant.RawPtr
+
+```k
+  rule <k> ListItem(PtrLocal(OFFSET, PLACE, _, _)) ListItem(Integer(LENGTH, 64, false)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT))
+        => PtrLocal(OFFSET, PLACE, MUT, ptrEmulation(dynamicSize(LENGTH)))
+        ...
+       </k>
+
+  rule <k> ListItem(PtrLocal(OFFSET, PLACE, _, _)) ListItem(Aggregate(_, .List)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT))
+        => PtrLocal(OFFSET, PLACE, MUT, ptrEmulation(noMetadata))
+        ...
+       </k>
+```
+
 The `Aggregate` type carries a `VariantIdx` to distinguish the different variants for an `enum`.
 This variant index is used to look up the _discriminant_ from a table in the type metadata during evaluation of the `Rvalue::Discriminant`.
 Note that the discriminant may be different from the variant index for user-defined discriminants and uninhabited variants.

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

@@ -0,0 +1,16 @@
+fn main() {
+    let a = [1,2,3u8];
+    f(&a);
+    let a = [4,5,6,7,8,9u8];
+    f(&a);
+}
+
+fn f(xs: &[u8]) {
+    // let [a, b, c, rest @ ..] = xs
+    // else { panic!("Need at least three elements"); };
+    // println!("Array {xs:?} is ( {a}, {b}, {c}, {rest:?} )");
+
+    if let [a, b, c, rest @ ..] = xs {
+        assert!(a + b - c == rest.len() as u8);
+    }
+}