Support Pulse.Lib.Slice.subslice

[gebner]

This adds support for the missing Pulse builtin Pulse.Lib.Slice.subslice.

[msprotz]

Looks good to me, so this is always an immutable slice?

[msprotz]

I guess mutability inference will kick in later on for this too, so I think we're good.

[gebner]

Yes, I checked that mutability inference triggers. Take this Pulse code, which takes a subslice and writes the subslice's length to its first element:

module Example.Subslice
#lang-pulse
open Pulse
open Pulse.Lib.Slice.Util
module A = Pulse.Lib.Array

fn test (arr: A.array UInt8.t)
    requires pts_to arr seq![0uy; 1uy; 2uy]
    ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 1uy; 1uy]) {
  A.pts_to_len arr;
  let slice = from_array arr 3sz;
  let last_one = subslice slice 2sz 3sz;
  pts_to_len last_one;
  last_one.(0sz) <- Int.Cast.uint64_to_uint8 (SizeT.sizet_to_uint64 (len last_one));
  unfold subslice_rest; join last_one _ _; join _ _ slice;
  to_array slice
}

Karamel correctly adds the &mut here:

#![allow(non_snake_case)]
#![allow(non_upper_case_globals)]
#![allow(non_camel_case_types)]
#![allow(unused_assignments)]
#![allow(unreachable_patterns)]

pub fn test(arr: &mut [u8])
{
    let slice: &mut [u8] = arr;
    let last_one: &mut [u8] = &mut slice[2usize..3usize];
    last_one[0usize] = last_one.len() as u64 as u8
}