Skip to content
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

Adding type support for mutable vs. immutable slices #326

Draft
wants to merge 10 commits into
base: main
Choose a base branch
from

Conversation

tahina-pro
Copy link
Member

@tahina-pro tahina-pro commented Feb 13, 2025

tl;dr Breaking changes

If you need mutable slices, you will need to change your code to use Pulse.Lib.MutableSlice instead of Pulse.Lib.Slice.

Adding type support for mutable vs. immutable slices

With FStarLang/karamel#533, Karamel is on track to supporting F* interfaces implemented in Rust. Thus, mutability analysis requires annotations on the types of such interfaces, to determine which arguments should be mut and which shouldn't. (@msprotz, please correct me if I'm wrong.)

Following a suggestion by @gebner , this PR:

  • makes Pulse.Lib.Slice.slice immutable
  • introduces Pulse.Lib.MutableSlice.slice for mutable slices (although this wouldn't preclude Karamel's whole-program analysis from refining them as immutable.)

To implement immutable slices, I duplicated Pulse.Lib.ArrayPtr as Pulse.Lib.ConstArrayPtr for const array pointers, which I extract to C const pointers. To do so, I rely on type abstraction: supported operations are the same except op_Array_Assignment and copy, which I removed from Pulse.Lib.ConstArrayPtr.

For compatibility purposes, I left interfaces unchanged as much as possible. So, there is a lot of code duplication. Maybe we want a type class for slice operations? I don't know.

I need to:

  • open a PR into Karamel to fix the MiniRust extraction of Pulse.Lib.Slice to mark them immutable, and add support for Pulse.Lib.MutableSlice.

tahina-pro added a commit to FStarLang/karamel that referenced this pull request Feb 14, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant