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

SAW Rust tutorial requires rotate_left override, which isn't included in crucible-mir submodule #2003

Closed
RyanGlScott opened this issue Jan 10, 2024 · 0 comments · Fixed by #2004
Assignees
Labels
PR: submodule bump Pull requests that include a submodule bump subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json

Comments

@RyanGlScott
Copy link
Contributor

The SAW Rust tutorial added in #1939 requires the use of a rotate_left override, which was added to crucible-mir in GaloisInc/crucible#1158. However, SAW's crucible submodule does not yet include the changes from GaloisInc/crucible#1158, which makes it impossible to follow along with the Rust tutorial at the moment. We should bump the crucible submodule accordingly to fix this.

@RyanGlScott RyanGlScott added PR: submodule bump Pull requests that include a submodule bump subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json labels Jan 10, 2024
@RyanGlScott RyanGlScott self-assigned this Jan 10, 2024
RyanGlScott added a commit that referenced this issue Jan 10, 2024
This bumps the `crucible` submodule to a commit that brings in the changes from
GaloisInc/crucible#1158. Among other things, this adds
an override for the Rust `rotate_left` function, which is crucial to making the
SAW Rust tutorial work.

Fixes #2003.
@mergify mergify bot closed this as completed in #2004 Jan 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: submodule bump Pull requests that include a submodule bump subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant