Code

Introduce Verus#143

Code

Merged

nspin merged 19 commits intoseL4:mainseL4/rust-sel4:mainfrom nspin:pr/introduce-verusnspin/rust-sel4:pr/introduce-verusCopy head branch name to clipboardMay 29, 2024

+843-379

Commits

Commits on May 29, 2024

• nix: Remove unnecessary condition for test

  Show description for ea4e02d
  nspin

  committed
  ea4e02d

• crates/sel4: Remove unnecessary import

  Show description for 48856de
  nspin

  committed
  48856de

• nix: Remove useLocal for Dafny derivation

  Show description for 8740534
  nspin

  committed
  8740534

• nix: Simplify fenix usage

  Show description for a65d053
  nspin

  committed
  a65d053

• nix: Make vendorLockfile more robust

  Show description for 71c3f62
  nspin

  committed
  71c3f62

• cmm: Refactor for clarity

  Show description for 5b45cc9
  nspin

  committed
  5b45cc9

• Don't use #[feature(pointer_is_aligned)] yet

  Show description for dfae90f
  nspin

  committed
  dfae90f

• Fix usage of pointer::align_offset

  Show description for 6e60af4
  nspin

  committed
  6e60af4

• nix: Run Dafny test

  Show description for 3cc7d18
  nspin

  committed
  3cc7d18

• nix: Add Verus tools and test skeleton

  Show description for 1032ab1
  nspin

  committed
  1032ab1

• nix: Improve vendoring attr ergonomics

  Show description for 1062c19
  nspin

  committed
  1062c19

• nix: Rework Rust toolchain handling

  Show description for 12584cf
  nspin

  committed
  12584cf

• nix: Add more structure to targetTriple

  Show description for c2eb526
  nspin

  committed
  c2eb526

• nix: Use alternative Rust toolchain for Verus test

  Show description for e6b88da
  nspin

  committed
  e6b88da

• nix: Implement verifyWithVerus

  Show description for 0115c58
  nspin

  committed
  0115c58

• nix: Enable multiple Rust toolchains in shell

  Show description for 20522d2
  nspin

  committed
  20522d2

• Add trivial Verus code

  Show description for 27c59ba
  nspin

  committed
  27c59ba

• nix: Use coliasgroup Verus repo

  Show description for 1891ab3
  nspin

  committed
  1891ab3

• nix: Fix style

  Show description for a136ee9
  nspin

  committed
  a136ee9