Skip to content

ArrayPtr: support for null pointer, converting from ref#500

Merged
tahina-pro merged 9 commits into
mainfrom
_taramana_arrayptr_null
Nov 7, 2025
Merged

ArrayPtr: support for null pointer, converting from ref#500
tahina-pro merged 9 commits into
mainfrom
_taramana_arrayptr_null

Conversation

@tahina-pro

Copy link
Copy Markdown
Member

Pulse.Lib.ArrayPtr.ptr is the abstraction for flexible C pointer arithmetic used when extracting Pulse.Lib.Slice to C. This PR adds support for the null pointer in ArrayPtr (but not Slice), as well as the ability to convert from a Pulse.Lib.Reference.ref.

This is needed to define EverCBOR's safe C API with as few preconditions as possible.

(This only affects C extraction. In Rust, Slice enjoys primitive extraction and ArrayPtr cannot be used.)

Comment thread lib/pulse/lib/Pulse.Lib.ArrayPtr.fst Outdated
type base_t ([@@@strictly_positive] a: Type0) =
| Null
| Ref of R.ref a
| Array of A.array a

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FYI, these days array a has both null pointers (A.null) and you can convert references to arrays (R.to_array).

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks Gabriel! I reimplemented from_ref, etc. accordingly.

@tahina-pro
tahina-pro force-pushed the _taramana_arrayptr_null branch from 2169669 to 6c276f7 Compare November 7, 2025 19:34
@tahina-pro
tahina-pro merged commit f0b12c9 into main Nov 7, 2025
2 checks passed
@tahina-pro
tahina-pro deleted the _taramana_arrayptr_null branch November 7, 2025 21:59
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.

2 participants