A model for Rust slices (and C array pointers)

[tahina-pro]

This PR proposes:

• Pulse.Lib.ArrayPtr, a library of C array pointers with subarray arithmetic, along with C extraction rules.
• Pulse.Lib.Slice, a library of Rust slices.

Since Pulse.Lib.Slice is implemented on top of Pulse.Lib.ArrayPtr, slices can extract to C, with their lengths becoming explicit.

Pulse.Lib.Slice.fsti is meant to model the following slice operations:

• op_Array_Index (resp. op_Array_Assignment) is modeling get_unchecked followed by a read (resp. update)
• split false (resp. split true) is modeling split_at (resp. split_at_mut)
• copy is modeling copy_from_slice

I intend those operations to be extracted by adding rules in Pulse2Rust (which is why they are not marked inline_for_extraction, thus C extraction will produce explicit functions monomorphized by Karamel.) However, at this point, I have no idea how to do that, so this PR does not provide anything to extract slices to Rust. If anyone has any idea, please rise up! Thanks in advance!

NOTE: Currently, this PR is done on top of Pulse commit c003b9733b1f11b6cc895e9c8681f0483cb193ea, corresponding to the last known good Everest at project-everest/everest@064cc2165b8f5b3af33ed279ad4cacded9abd963

[gebner]

I have added support for slices in pulse2rust and added test cases too.

@tahina-pro There are some small changes in the API:

• The footprint arguments are gone. You can just remove the fps everywhere and everything should work fine.
• The pts_to definitions are instances now. You can just replace S.pts_to by pts_to.
• The mutb flag is gone too. You can just remove it.
• I've renamed AP.blit to AP.memcpy (for consistency with Array.memcpy)
• You probably need to remove lots of fold/unfold statements. (The postconditions are now more consistent with the array API, and don't use extra definitions.)

Unless somebody complains, I'll merge this by tomorrow.

[tahina-pro]

Thanks a lot Gabriel! Your changes greatly improved my initial proposal! And, last but not least, many thanks also for adding Rust extraction support!