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

Allow using hax-lib in #![no_std] environments #443

Closed
wants to merge 1 commit into from

Conversation

sivadeilra
Copy link

This tiny PR allows using hax-lib in Rust #![no_std] environments. These environments are common in embedded devices, low-level operating system contexts, etc.

This PR does not have any sort of penalty or cost for environments that do not use #![no_std].

@sivadeilra
Copy link
Author

Is there anything more that needs to be done before merging this?

@franziskuskiefer
Copy link
Member

Is there anything more that needs to be done before merging this?

Not directly. But it would be nice if we'd have a CI run that makes sure that this actually works.
Can you add a job that is building the library for a no_std target?

@sivadeilra
Copy link
Author

Not directly. But it would be nice if we'd have a CI run that makes sure that this actually works.
Can you add a job that is building the library for a no_std target?

Can you be a bit more specific?

I did this work because I am working on code changes in the libcrux repo, which will enable libcrux to be used in embedded contexts that don't have libstd. This PR works, in the sense that it does allow me to compile libcrux (and dependent crates) using #![no_std].

What form of verification are you looking for, in this repo, though? I've worked with many no_std crates before, and this is generally so reliable that there is no need to test it. After all, this doesn't create a new configuration for hax-lib, it just changes how hax-lib already works, and in a way that is compatible with all current uses of hax-lib.

@franziskuskiefer
Copy link
Member

I did this work because I am working on code changes in the libcrux repo, which will enable libcrux to be used in embedded contexts that don't have libstd.

Interesting. Looking forward to those changes!

This PR works, in the sense that it does allow me to compile libcrux (and dependent crates) using #![no_std].

We should actually drop that dependency again. But making it work for no_std is still worthwhile as we have other projects where this will be needed.

What form of verification are you looking for, in this repo, though? I've worked with many no_std crates before, and this is generally so reliable that there is no need to test it. After all, this doesn't create a new configuration for hax-lib, it just changes how hax-lib already works, and in a way that is compatible with all current uses of hax-lib.
Can you be a bit more specific?

The code can change and no_std may be broken in subtle (or direct) ways. To avoid that, we can add a build for a target without std support, for example thumbv7em-none-eabi, to the CI. This will catch any breakage of the no_std build.

@franziskuskiefer franziskuskiefer mentioned this pull request Jan 25, 2024
@franziskuskiefer
Copy link
Member

Thanks for the PR @sivadeilra! I added the CI on top in #457 and merge it there. I'm closing this.

@sivadeilra
Copy link
Author

Thank you!

@sivadeilra sivadeilra deleted the no_std branch January 26, 2024 04:49
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