Skip to content

Commit

Permalink
REMOVE BEFORE MERGING: Add cargo-verus demo
Browse files Browse the repository at this point in the history
Just to aid discussion and review.
  • Loading branch information
nspin committed May 24, 2024
1 parent 5293caf commit 3bb30c5
Show file tree
Hide file tree
Showing 13 changed files with 1,152 additions and 0 deletions.
36 changes: 36 additions & 0 deletions source/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 4 additions & 0 deletions source/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,10 @@ members = [
"tools/internals_interface",
"tools/line_count",
"tools/qi-graph",
"cargo-verus-illustration/doubly-linked-xor",
"cargo-verus-illustration/doubly-linked-xor-test",
"cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot",
"cargo-verus-illustration/rust-verify-examples",
]

# do not modify the following two lines
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
[package]
name = "doubly-linked-xor-test-using-verus-sysroot"
version = "0.1.0"
edition = "2021"

[dependencies]
doubly-linked-xor = { path = "../doubly-linked-xor" }

[package.metadata.verus]
verify = true
imports = ["doubly_linked_xor"]
14 changes: 14 additions & 0 deletions source/cargo-verus-illustration/doubly-linked-xor-test/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
[package]
name = "doubly-linked-xor-test"
version = "0.1.0"
edition = "2021"

[dependencies]
vstd = { path = "../../vstd" }
builtin = { path = "../../builtin" }
builtin_macros = { path = "../../builtin_macros" }
doubly-linked-xor = { path = "../doubly-linked-xor", features = ["explicit-verus-deps"] }

[package.metadata.verus]
verify = true
imports = ["doubly_linked_xor"]
31 changes: 31 additions & 0 deletions source/cargo-verus-illustration/doubly-linked-xor-test/src/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
use vstd::{prelude::*, string::*};

use doubly_linked_xor::DListXor;

verus! {

#[verifier::external_body]
fn print_result(msg: StrSlice<'static>, value: u32) {
println!("{}: {value}", msg.into_rust_str());
}

fn main() {
let mut t = DListXor::<u32>::new();
t.push_back(2);
t.push_back(3);
t.push_front(1); // 1, 2, 3
print_result(new_strlit("pushed"), 2);
print_result(new_strlit("pushed"), 3);
print_result(new_strlit("pushed"), 1);
let x = t.pop_back(); // 3
let y = t.pop_front(); // 1
let z = t.pop_front(); // 2
assert(x == 3);
assert(y == 1);
assert(z == 2);
print_result(new_strlit("popped"), x);
print_result(new_strlit("popped"), y);
print_result(new_strlit("popped"), z);
}

} // verus!
15 changes: 15 additions & 0 deletions source/cargo-verus-illustration/doubly-linked-xor/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
[package]
name = "doubly-linked-xor"
version = "0.1.0"
edition = "2021"

[dependencies]
vstd = { path = "../../vstd", optional = true }
builtin = { path = "../../builtin", optional = true }
builtin_macros = { path = "../../builtin_macros", optional = true }

[features]
explicit-verus-deps = ["vstd", "builtin", "builtin_macros"]

[package.metadata.verus]
verify = true
Loading

0 comments on commit 3bb30c5

Please sign in to comment.