A model for Rust slices (and C array pointers) #225
Conversation
| : Lemma (is_slprop2 (is_split s p i left right)) | ||
| [SMTPat (is_slprop2 (is_split s p i left right))] | ||
|
|
||
| noeq type slice_pair (t: Type) = | SlicePair: (fst: slice t) -> (snd: slice t) -> slice_pair t |
There was a problem hiding this comment.
I added this type because Karamel refuses to extract functions returning F* pairs
There was a problem hiding this comment.
This is only an issue with the Rust backend, right? In my experience, C-karamel does pairs just fine.
There was a problem hiding this comment.
if you could file a bug upstream with a precise description, that would be helpful, thank you
| @@ -0,0 +1,269 @@ | |||
| module Pulse.Lib.ArrayPtr | |||
There was a problem hiding this comment.
The files are missing copyright headers.
lib/pulse/lib/Pulse.Lib.ArrayPtr.fst
Outdated
|
|
||
| [@@erasable] | ||
| noeq | ||
| type footprint (t: Type0) = { |
There was a problem hiding this comment.
Why is the extra footprint necessary here? Both fields are determined by the pts_to_range slprop.
lib/pulse/lib/Pulse.Lib.ArrayPtr.fst
Outdated
| ghost | ||
| fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint t) (#v: Seq.seq t) | ||
| requires pts_to s #p fp v ** is_from_array p fp a ** pure ( | ||
| Seq.length v == A.length a |
There was a problem hiding this comment.
This is already implied by is_from_array, right?
| [SMTPat (adjacent fp1 fp2); SMTPat (adjacent fp2 fp3)]; | ||
| ]] | ||
|
|
||
| let split_postcond |
There was a problem hiding this comment.
In Pulse it's usually better to write the pre/postconditions directly without definitions because you need to manually call fold/unfold otherwise (and often spell out the arguments twice!).
There was a problem hiding this comment.
Randomly noticed this comment, but see #143. I've had good experience with using aliases like this one and marking them @@pulse_unfold. This seems to be a pure fact though.
There was a problem hiding this comment.
You're right, this one is pure; there are other definitions here though that are slprops.
I didn't know about @@pulse_unfold, does it also fold automatically when it is part of a precondition?
There was a problem hiding this comment.
does it also fold automatically when it is part of a precondition?
Yes, any top-level name marked with @@pulse_unfold is unfolded in the context eagerly and in goals (like a precondition, but also assert) before we attempt to prove them.
| (requires pts_to arr #p0 fp s0 ** pts_to arr #p1 fp s1) | ||
| (ensures fun _ -> pts_to arr #(p0 +. p1) fp s0 ** pure (s0 == s1)) | ||
|
|
||
| val adjacent (#t: Type): footprint t -> footprint t -> prop |
There was a problem hiding this comment.
I think it would be significantly more ergonomic (and result in a better SMT encoding) to expose base/offset:
val base #t : ptr t -> GTot (A.array t)
val offset #t : ptr t -> GTot nat
let adjacent #t (a: ptr t) (sz: nat) (b: ptr t) : prop =
base a == base b /\ offset a + sz == offset bThen merge_assoc becomes unnecessary as well because Z3 can prove it directly.
lib/pulse/lib/Pulse.Lib.Slice.fst
Outdated
| pure (SZ.v s.len == A.length a) | ||
|
|
||
| ```pulse | ||
| fn from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { |
There was a problem hiding this comment.
What's the purpose of the mutb arguments here and in split?
Was your intention to encode the Rust split/split_mut distinction this way? I don't think that works. The main challenge with the Rust extraction is figuring out whether the type should be &[t] or &mut[t]; once you know the type it's easy to call the right split(_mut) version, but the flag in this function is not enough to infer the Rust type.
|
I have added support for slices in pulse2rust and added test cases too. @tahina-pro There are some small changes in the API:
Unless somebody complains, I'll merge this by tomorrow. |
|
Thanks a lot Gabriel! Your changes greatly improved my initial proposal! |
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.Sliceis implemented on top ofPulse.Lib.ArrayPtr, slices can extract to C, with their lengths becoming explicit.Pulse.Lib.Slice.fstiis meant to model the following slice operations:op_Array_Index(resp.op_Array_Assignment) is modelingget_uncheckedfollowed by a read (resp. update)split false(resp.split true) is modelingsplit_at(resp.split_at_mut)copyis modelingcopy_from_sliceI 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 c003b97, corresponding to the last known good Everest at project-everest/everest@064cc21