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

Introduce Verus #143

Merged
merged 19 commits into from
May 29, 2024
Merged

Introduce Verus #143

merged 19 commits into from
May 29, 2024

Conversation

nspin
Copy link
Member

@nspin nspin commented May 29, 2024

Verus is a tool for verifying the correctness of code written in Rust.

This PR introduces Verus into the project:

  • Build system changes to enable the use of multiple Rust toolchains via the rustEnvironment construct in Nix
  • The introduction of the Verus tools into the build system
  • A trivial example/test (more to come)

This work depends on a PR to the upstream Verus repository:

verus-lang/verus#1138

For now, we are using this branch of Verus, which includes that patch:

https://github.com/coliasgroup/verus/tree/dev

@nspin nspin mentioned this pull request May 29, 2024
Open
@nspin nspin force-pushed the pr/introduce-verus branch from 06a75fc to c0688cb Compare May 29, 2024 09:51
nspin added 18 commits May 29, 2024 11:10
@nspin
nix: Remove unnecessary condition for test
ea4e02d 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
crates/sel4: Remove unnecessary import
48856de 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Remove useLocal for Dafny derivation
8740534 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Simplify fenix usage
a65d053 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Make vendorLockfile more robust
71c3f62 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
cmm: Refactor for clarity
5b45cc9 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
Don't use #[feature(pointer_is_aligned)] yet
dfae90f 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
Fix usage of pointer::align_offset
6e60af4 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Run Dafny test
3cc7d18 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Add Verus tools and test skeleton
1032ab1 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Improve vendoring attr ergonomics
1062c19 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Rework Rust toolchain handling
12584cf 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Add more structure to targetTriple
c2eb526 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Use alternative Rust toolchain for Verus test
e6b88da 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Implement verifyWithVerus
0115c58 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Enable multiple Rust toolchains in shell
20522d2 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
Add trivial Verus code
27c59ba 
Signed-off-by: Nick Spinale <[email protected]>
@nspin
nix: Use coliasgroup Verus repo
1891ab3 
Signed-off-by: Nick Spinale <[email protected]>
@nspin nspin force-pushed the pr/introduce-verus branch from c0688cb to 1891ab3 Compare May 29, 2024 11:10
@nspin
nix: Fix style
a136ee9 
Signed-off-by: Nick Spinale <[email protected]>
@nspin nspin merged commit 680d6fc into seL4:main May 29, 2024
9 checks passed
@nspin nspin deleted the pr/introduce-verus branch May 29, 2024 11:56
@lsf37
Copy link
Member

lsf37 commented May 29, 2024

Loving the influx of verification tools! :-)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nspin @lsf37