-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
A model for Rust slices (and C array pointers) #225
base: main
Are you sure you want to change the base?
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I added this type because Karamel refuses to extract functions returning F* pairs
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is only an issue with the Rust backend, right? In my experience, C-karamel does pairs just fine.
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 ofPulse.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 modelingget_unchecked
followed by a read (resp. update)split false
(resp.split true
) is modelingsplit_at
(resp.split_at_mut
)copy
is modelingcopy_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 c003b97, corresponding to the last known good Everest at project-everest/everest@064cc21