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.

Sign up for GitHub

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

Jump to bottom

Add mir_fresh_cryptol_var #1970

Closed
RyanGlScott opened this issue Nov 2, 2023 · 0 comments · Fixed by #1971
Closed

Add mir_fresh_cryptol_var #1970

RyanGlScott opened this issue Nov 2, 2023 · 0 comments · Fixed by #1971
Labels
subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: enhancement Issues describing an improvement to an existing feature or capability

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Nov 2, 2023 •
edited
Loading

This would behave much like the existing llvm_fresh_cryptol_var function. This will be important in combination with ghost state (#1929) that uses Cryptol types that cannot be created directly from a MIRType via mir_fresh_var.
@RyanGlScott RyanGlScott added type: enhancement Issues describing an improvement to an existing feature or capability subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json labels Nov 2, 2023
@RyanGlScott RyanGlScott mentioned this issue Nov 2, 2023
Closed
29 tasks
RyanGlScott added a commit that referenced this issue Nov 2, 2023
@RyanGlScott
mir_fresh_cryptol_var
2de845a 
This also adds some very rudimentary test cases. A more impressive test case
would involve ghost state, but we will need #1958 before we can write such a
test case.

Fixes #1970.
@RyanGlScott RyanGlScott mentioned this issue Nov 2, 2023
Merged
RyanGlScott added a commit that referenced this issue Nov 5, 2023
@RyanGlScott
mir_fresh_cryptol_var
98480ae 
This also adds some very rudimentary test cases. A more impressive test case
would involve ghost state, but we will need #1958 before we can write such a
test case.

Fixes #1970.
RyanGlScott added a commit that referenced this issue Nov 9, 2023
@RyanGlScott
mir_fresh_cryptol_var
b2f1f7a 
This also adds some very rudimentary test cases. A more impressive test case
would involve ghost state, but we will need #1958 before we can write such a
test case.

Fixes #1970.
RyanGlScott added a commit that referenced this issue Nov 9, 2023
@RyanGlScott
mir_fresh_cryptol_var
cb4abb5 
This also adds some very rudimentary test cases. A more impressive test case
would involve ghost state, but we will need #1958 before we can write such a
test case.

Fixes #1970.
RyanGlScott added a commit that referenced this issue Nov 22, 2023
@RyanGlScott
mir_fresh_cryptol_var
6d9919f 
This also adds some very rudimentary test cases. A more impressive test case
would involve ghost state, but we will need #1958 before we can write such a
test case.

Fixes #1970.
@mergify mergify bot closed this as completed in #1971 Nov 22, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

mir_fresh_cryptol_var GaloisInc/saw-script
1 participant
@RyanGlScott