REMOVE BEFORE MERGING: Add cargo-verus demo

Just to aid discussion and review.

source/Cargo.toml

@@ -20,6 +20,13 @@ 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",
+]
+
+exclude = [
+  "cargo-verus-illustration/rust-verify-examples",
 ]
 
 # do not modify the following two lines

source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/Cargo.toml

@@ -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"]

source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/src

@@ -0,0 +1 @@
+../doubly-linked-xor/src/

source/cargo-verus-illustration/doubly-linked-xor-test/Cargo.toml

@@ -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"]

source/cargo-verus-illustration/doubly-linked-xor-test/src/main.rs

@@ -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!

source/cargo-verus-illustration/doubly-linked-xor/Cargo.toml

@@ -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