From 2613c1bbc9d21719cffbabe28ab2e52b6a2d84d7 Mon Sep 17 00:00:00 2001 From: Nick Spinale Date: Thu, 23 May 2024 20:30:40 +0000 Subject: [PATCH] REMOVE BEFORE MERGING: Add cargo-verus demo Just to aid discussion and review. --- source/Cargo.lock | 26 + source/Cargo.toml | 3 + .../Cargo.toml | 11 + .../src/main.rs | 1 + .../doubly-linked-xor-test/Cargo.toml | 14 + .../doubly-linked-xor-test/src/main.rs | 31 ++ .../doubly-linked-xor/Cargo.toml | 15 + .../doubly-linked-xor/src/lib.rs | 487 ++++++++++++++++++ source/cargo-verus-illustration/illustrate.sh | 53 ++ 9 files changed, 641 insertions(+) create mode 100644 source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/Cargo.toml create mode 120000 source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/src/main.rs create mode 100644 source/cargo-verus-illustration/doubly-linked-xor-test/Cargo.toml create mode 100644 source/cargo-verus-illustration/doubly-linked-xor-test/src/main.rs create mode 100644 source/cargo-verus-illustration/doubly-linked-xor/Cargo.toml create mode 100644 source/cargo-verus-illustration/doubly-linked-xor/src/lib.rs create mode 100755 source/cargo-verus-illustration/illustrate.sh diff --git a/source/Cargo.lock b/source/Cargo.lock index d963597f46..937ab625eb 100644 --- a/source/Cargo.lock +++ b/source/Cargo.lock @@ -520,6 +520,32 @@ dependencies = [ "subtle", ] +[[package]] +name = "doubly-linked-xor" +version = "0.1.0" +dependencies = [ + "builtin", + "builtin_macros", + "vstd", +] + +[[package]] +name = "doubly-linked-xor-test" +version = "0.1.0" +dependencies = [ + "builtin", + "builtin_macros", + "doubly-linked-xor", + "vstd", +] + +[[package]] +name = "doubly-linked-xor-test-using-verus-sysroot" +version = "0.1.0" +dependencies = [ + "doubly-linked-xor", +] + [[package]] name = "dtoa" version = "1.0.8" diff --git a/source/Cargo.toml b/source/Cargo.toml index 4c45b4b175..68b00f38b7 100644 --- a/source/Cargo.toml +++ b/source/Cargo.toml @@ -20,6 +20,9 @@ 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", ] # do not modify the following two lines diff --git a/source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/Cargo.toml b/source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/Cargo.toml new file mode 100644 index 0000000000..ec4ebe629b --- /dev/null +++ b/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"] diff --git a/source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/src/main.rs b/source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/src/main.rs new file mode 120000 index 0000000000..8ca8d68db3 --- /dev/null +++ b/source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/src/main.rs @@ -0,0 +1 @@ +../../doubly-linked-xor-test/src/main.rs \ No newline at end of file diff --git a/source/cargo-verus-illustration/doubly-linked-xor-test/Cargo.toml b/source/cargo-verus-illustration/doubly-linked-xor-test/Cargo.toml new file mode 100644 index 0000000000..45bad04f67 --- /dev/null +++ b/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"] diff --git a/source/cargo-verus-illustration/doubly-linked-xor-test/src/main.rs b/source/cargo-verus-illustration/doubly-linked-xor-test/src/main.rs new file mode 100644 index 0000000000..7261526d81 --- /dev/null +++ b/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::::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! diff --git a/source/cargo-verus-illustration/doubly-linked-xor/Cargo.toml b/source/cargo-verus-illustration/doubly-linked-xor/Cargo.toml new file mode 100644 index 0000000000..1cd604d49f --- /dev/null +++ b/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 diff --git a/source/cargo-verus-illustration/doubly-linked-xor/src/lib.rs b/source/cargo-verus-illustration/doubly-linked-xor/src/lib.rs new file mode 100644 index 0000000000..1928f429bd --- /dev/null +++ b/source/cargo-verus-illustration/doubly-linked-xor/src/lib.rs @@ -0,0 +1,487 @@ +use vstd::{prelude::*, ptr::*, *}; + +// "XOR Linked List". This is a sorta-cute (if not usually practical) folk data structure: +// A doubly-linked list which saves memory by having each node store the XOR of the two +// pointers to its two neighbors. +// +// This example uses the XOR Linked List to build a deque. +// +// TODO should really use usize, but bit-vector operations on usize aren't supported right now, +// so we use u64 and assume it's equivalent to usize. + +verus! { + +#[verifier::external_body] +proof fn lemma_usize_u64(x: u64) + ensures + x as usize as u64 == x, +{ + unimplemented!(); +} + +// Single node in the list +pub struct Node { + pub xored: u64, + pub v: V, +} + +// Doubly-linked list +// Contains head pointer, tail pointer +// and in ghost code, tracks all the pointers and all the permissions to access the nodes +type MemPerms = (PointsTo>, Dealloc>); + +pub struct DListXor { + pub ptrs: Ghost>>>, + pub perms: Tracked>>, + pub head: u64, + pub tail: u64, +} + +impl DListXor { + pub open spec fn wf_perms(&self) -> bool { + forall|i: nat| 0 <= i < self.ptrs@.len() ==> self.wf_perm(i) + } + + pub open spec fn prev_of(&self, i: nat) -> u64 + recommends + i < self.ptrs@.len(), + { + if i == 0 { + 0 + } else { + self.ptrs@[i - 1].id() as u64 + } + } + + pub open spec fn next_of(&self, i: nat) -> u64 + recommends + i < self.ptrs@.len(), + { + if i + 1 == self.ptrs@.len() { + 0 + } else { + self.ptrs@[i + 1int].id() as u64 + } + } + + pub open spec fn wf_perm(&self, i: nat) -> bool + recommends + i < self.ptrs@.len(), + { + &&& self.perms@.dom().contains(i) + &&& self.perms@[i].0.view().pptr == self.ptrs@[i as int].id() + &&& self.perms@[i].1.view().pptr == self.ptrs@[i as int].id() + &&& 0 < self.ptrs@[i as int].id() + &&& self.ptrs@[i as int].id() < 0x10000000000000000 + &&& self.perms@[i].0.view().value.is_Some() + &&& self.perms@[i].0.view().value.get_Some_0().xored == (self.prev_of(i) ^ self.next_of(i)) + } + + pub open spec fn wf_head(&self) -> bool { + if self.ptrs@.len() == 0 { + self.head == 0 + } else { + self.head == self.ptrs@[0].id() + } + } + + pub open spec fn wf_tail(&self) -> bool { + if self.ptrs@.len() == 0 { + self.tail == 0 + } else { + self.tail == self.ptrs@[self.ptrs@.len() - 1].id() + } + } + + pub open spec fn wf(&self) -> bool { + self.wf_perms() && self.wf_head() && self.wf_tail() + } + + pub open spec fn view(&self) -> Seq + recommends + self.wf(), + { + Seq::::new(self.ptrs@.len(), |i: int| { self.perms@[i as nat].0@.value.get_Some_0().v }) + } + + pub fn new() -> (s: Self) + ensures + s.wf(), + s@.len() == 0, + { + DListXor { + ptrs: Ghost(Seq::empty()), + perms: Tracked(Map::tracked_empty()), + head: 0, + tail: 0, + } + } + + fn push_empty_case(&mut self, v: V) + requires + old(self).wf(), + old(self).ptrs@.len() == 0, + ensures + self.wf(), + self@ == old(self)@.push(v), + { + let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new(Node:: { xored: 0, v }); + proof { + self.ptrs@ = self.ptrs@.push(ptr); + (&perm).is_nonnull(); + self.perms.borrow_mut().tracked_insert((self.ptrs@.len() - 1) as nat, (perm, dealloc)); + } + self.tail = ptr.to_usize() as u64; + self.head = self.tail; + assert(0u64 ^ 0u64 == 0u64) by (bit_vector); + assert(self@ =~= old(self)@.push(v)); + } + + pub fn push_back(&mut self, v: V) + requires + old(self).wf(), + ensures + self.wf(), + self@ == old(self)@.push(v), + { + if self.tail == 0 { + // Special case: list is empty + proof { + assert_by_contradiction!(self.ptrs@.len() == 0, { + assert(self.wf_perm((self.ptrs@.len() - 1) as nat)); + }); + } + self.push_empty_case(v); + } else { + assert(self.ptrs@.len() > 0); + assert(self.wf_perm((self.ptrs@.len() - 1) as nat)); + let tail_ptr_u64 = self.tail; + proof { + lemma_usize_u64(tail_ptr_u64); + } + let tail_ptr = PPtr::>::from_usize(tail_ptr_u64 as usize); + let tracked (mut tail_perm, de): MemPerms = self.perms.borrow_mut().tracked_remove( + (self.ptrs@.len() - 1) as nat, + ); + let mut tail_node = tail_ptr.take(Tracked(&mut tail_perm)); + let second_to_last_ptr = tail_node.xored; + let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new( + Node:: { xored: tail_ptr_u64, v }, + ); + proof { + perm.is_nonnull(); + } + let new_ptr_u64 = ptr.to_usize() as u64; + tail_node.xored = second_to_last_ptr ^ new_ptr_u64; + tail_ptr.put(Tracked(&mut tail_perm), tail_node); + proof { + self.perms.borrow_mut().tracked_insert( + (self.ptrs@.len() - 1) as nat, + (tail_perm, de), + ); + self.perms.borrow_mut().tracked_insert(self.ptrs@.len(), (perm, dealloc)); + self.ptrs@ = self.ptrs@.push(ptr); + } + self.tail = new_ptr_u64; + proof { + assert(tail_ptr_u64 ^ 0 == tail_ptr_u64) by (bit_vector); + let i = (self.ptrs@.len() - 2) as nat; + //assert(self.perms@.dom().contains(i)); + //assert(self.perms@[i]@.pptr == self.ptrs@[i]@); + //assert(self.perms@[i].value.is_Some()); + let prev_of_i = self.prev_of(i); + assert(prev_of_i ^ 0 == prev_of_i) by (bit_vector); + //assert(self.prev_of(i) == second_to_last_ptr); + //assert(self.next_of(i) == new_ptr_int); + //assert(self.perms@[i].value.get_Some_0().xored == ( + // self.prev_of(i) ^ self.next_of(i) + //)); + assert(self.wf_perm((self.ptrs@.len() - 2) as nat)); + assert(self.wf_perm((self.ptrs@.len() - 1) as nat)); + assert(forall|i: nat| + i < self.ptrs@.len() ==> old(self).wf_perm(i) ==> self.wf_perm(i)); + assert(self.wf_perms()); + assert(self.wf_tail()); + assert(self@[self.ptrs@.len() - 1] == v); + assert forall|i: int| 0 <= i < self.ptrs@.len() - 1 implies old(self)@[i] + == self@[i] by { + assert(old(self).wf_perm(i as nat)); // trigger + }; + assert(self@ =~= old(self)@.push(v)); + } + } + } + + pub fn pop_back(&mut self) -> (v: V) + requires + old(self).wf(), + old(self)@.len() > 0, + ensures + self.wf(), + self@ == old(self)@.drop_last(), + v == old(self)@[old(self)@.len() - 1], + { + assert(self.wf_perm((self.ptrs@.len() - 1) as nat)); + let last_u64 = self.tail; + proof { + lemma_usize_u64(last_u64); + } + let last_ptr = PPtr::>::from_usize(last_u64 as usize); + let tracked last_perm: MemPerms = self.perms.borrow_mut().tracked_remove( + (self.ptrs@.len() - 1) as nat, + ); + let last_node = last_ptr.into_inner(Tracked(last_perm.0), Tracked(last_perm.1)); + let penult_u64 = last_node.xored; + let v = last_node.v; + proof { + let self_head = self.head; + assert(self_head ^ 0 == self_head) by (bit_vector); + assert(0u64 ^ 0 == 0) by (bit_vector); + } + if penult_u64 == 0 { + self.tail = 0; + self.head = 0; + proof { + assert_by_contradiction!(self.ptrs@.len() == 1, { + assert(old(self).wf_perm((self.ptrs@.len() - 2) as nat)); + #[verifier::spec] let actual_penult_u64 = self.prev_of((self.ptrs@.len() - 1) as nat); + assert(actual_penult_u64 ^ 0 == actual_penult_u64) by(bit_vector); + }); + } + } else { + self.tail = penult_u64; + assert(old(self)@.len() != 1); + assert(old(self)@.len() >= 2); + assert(old(self).wf_perm((self.ptrs@.len() - 2) as nat)); + proof { + let actual_penult_u64 = self.prev_of((self.ptrs@.len() - 1) as nat); + assert(actual_penult_u64 ^ 0 == actual_penult_u64) by (bit_vector); + lemma_usize_u64(penult_u64); + } + let penult_ptr = PPtr::>::from_usize(penult_u64 as usize); + let tracked (mut penult_perm, de) = self.perms.borrow_mut().tracked_remove( + (self.ptrs@.len() - 2) as nat, + ); + let mut penult_node = penult_ptr.take(Tracked(&mut penult_perm)); + let t: Ghost = Ghost(self.prev_of((self.ptrs@.len() - 2) as nat)); + assert((t@ ^ last_u64) ^ last_u64 == t@ ^ 0) by (bit_vector); + penult_node.xored = penult_node.xored ^ last_u64; + assert(penult_node.xored == t@ ^ 0); + penult_ptr.put(Tracked(&mut penult_perm), penult_node); + proof { + self.perms.borrow_mut().tracked_insert( + (self.ptrs@.len() - 2) as nat, + (penult_perm, de), + ); + } + } + proof { + self.ptrs@ = self.ptrs@.drop_last(); + } + proof { + assert(self.wf_head()); + assert(self.wf_tail()); + if self.ptrs@.len() > 0 { + /*#[verifier::spec] let i = self.ptrs@.len() - 1; + assert(self.ptrs@.len() == old(self).ptrs@.len() - 1); + assert(self.perms@.dom().contains(i)); + assert(self.perms@[i]@.pptr == self.ptrs@[i]@); + assert(0 < self.ptrs@[i]@); + assert(self.ptrs@[i]@ < 0x10000000000000000); + assert(self.perms@[i].value.is_Some()); + assert(self.perms@[i].value.get_Some_0().xored == ( + self.prev_of(i) ^ self.next_of(i) + ));*/ + assert(self.wf_perm((self.ptrs@.len() - 1) as nat)); + } + assert(forall|i: nat| i < self@.len() ==> old(self).wf_perm(i) ==> self.wf_perm(i)); + assert(self.wf_perms()); + assert forall|i: int| 0 <= i < self@.len() implies #[trigger] self@[i] == old( + self, + )@.drop_last()[i] by { + assert(old(self).wf_perm(i as nat)); // trigger + } + assert(self@ =~= old(self)@.drop_last()); + } + v + } + + pub fn pop_front(&mut self) -> (v: V) + requires + old(self).wf(), + old(self)@.len() > 0, + ensures + self.wf(), + self@ == old(self)@.subrange(1, old(self)@.len() as int), + v == old(self)@[0], + { + assert(self.wf_perm(0)); + let first_u64 = self.head; + proof { + lemma_usize_u64(first_u64); + } + let first_ptr = PPtr::>::from_usize(first_u64 as usize); + let tracked first_perm: MemPerms = self.perms.borrow_mut().tracked_remove(0); + let first_node = first_ptr.into_inner(Tracked(first_perm.0), Tracked(first_perm.1)); + let second_u64 = first_node.xored; + let v = first_node.v; + proof { + let self_tail = self.tail; + assert(self_tail ^ 0 == self_tail) by (bit_vector); + assert(0u64 ^ 0 == 0) by (bit_vector); + } + if second_u64 == 0 { + self.tail = 0; + self.head = 0; + proof { + assert_by_contradiction!(self.ptrs@.len() == 1, { + assert(old(self).wf_perm(1)); + #[verifier::spec] let actual_second_u64 = self.next_of(0); + assert(0 ^ actual_second_u64 == actual_second_u64) by(bit_vector); + }); + } + } else { + self.head = second_u64; + assert(old(self)@.len() != 1); + assert(old(self)@.len() >= 2); + assert(old(self).wf_perm(1)); + proof { + let actual_second_u64 = self.next_of(0); + assert(0 ^ actual_second_u64 == actual_second_u64) by (bit_vector); + lemma_usize_u64(second_u64); + } + let second_ptr = PPtr::>::from_usize(second_u64 as usize); + let tracked (mut second_perm, de) = (self.perms.borrow_mut()).tracked_remove(1); + let mut second_node = second_ptr.take(Tracked(&mut second_perm)); + let t: Ghost = Ghost(self.next_of(1)); + assert((first_u64 ^ t@) ^ first_u64 == 0 ^ t@) by (bit_vector); + second_node.xored = second_node.xored ^ first_u64; + assert(second_node.xored == 0 ^ t@); + second_ptr.put(Tracked(&mut second_perm), second_node); + proof { + self.perms.borrow_mut().tracked_insert(1, (second_perm, de)); + assert forall|j: nat| 1 <= j < old(self)@.len() implies self.perms@.dom().contains( + j, + ) by { + assert(old(self).wf_perm(j)); + } + (self.perms.borrow_mut()).tracked_map_keys_in_place( + Map::::new( + |j: nat| 0 <= j < old(self)@.len() - 1, + |j: nat| (j + 1) as nat, + ), + ); + } + } + proof { + self.ptrs@ = self.ptrs@.subrange(1, self.ptrs@.len() as int); + } + proof { + assert(self.wf_tail()); + assert(self.wf_head()); + if self.ptrs@.len() > 0 { + assert(self.wf_perm(0)); + } + assert(forall|i: nat| i < self@.len() ==> old(self).wf_perm(i + 1) ==> self.wf_perm(i)); + assert(self.wf_perms()); + assert forall|i: int| 0 <= i < self@.len() implies #[trigger] self@[i] == old( + self, + )@.subrange(1, old(self)@.len() as int)[i] by { + assert(old(self).wf_perm(i as nat + 1)); // trigger + } + assert(self@ =~= old(self)@.subrange(1, old(self)@.len() as int)); + } + v + } + + pub fn push_front(&mut self, v: V) + requires + old(self).wf(), + ensures + self.wf(), + self@ == seq![v].add(old(self)@), + { + if self.tail == 0 { + // Special case: list is empty + proof { + assert_by_contradiction!(self.ptrs@.len() == 0, { + assert(self.wf_perm((self.ptrs@.len() - 1) as nat)); + }); + } + self.push_empty_case(v); + assert(self@ =~= seq![v].add(old(self)@)); + } else { + assert(self.ptrs@.len() > 0); + assert(self.wf_perm(0)); + let head_ptr_u64 = self.head; + proof { + lemma_usize_u64(head_ptr_u64); + } + let head_ptr = PPtr::>::from_usize(head_ptr_u64 as usize); + let tracked (mut head_perm, de): MemPerms = (self.perms.borrow_mut()).tracked_remove( + 0, + ); + let mut head_node = head_ptr.take(Tracked(&mut head_perm)); + let second_ptr = head_node.xored; + let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new( + Node:: { xored: head_ptr_u64, v }, + ); + proof { + perm.is_nonnull(); + } + let new_ptr_u64 = ptr.to_usize() as u64; + head_node.xored = new_ptr_u64 ^ second_ptr; + head_ptr.put(Tracked(&mut head_perm), head_node); + proof { + self.perms.borrow_mut().tracked_insert(0, (head_perm, de)); + assert forall|j: nat| 0 <= j < old(self)@.len() implies self.perms@.dom().contains( + j, + ) by { + assert(old(self).wf_perm(j)); + } + self.perms.borrow_mut().tracked_map_keys_in_place( + Map::::new( + |j: nat| 1 <= j <= old(self)@.len(), + |j: nat| (j - 1) as nat, + ), + ); + self.perms.borrow_mut().tracked_insert(0, (perm, dealloc)); + self.ptrs@ = seq![ptr].add(self.ptrs@); + } + self.head = new_ptr_u64; + proof { + assert(0 ^ head_ptr_u64 == head_ptr_u64) by (bit_vector); + let i = 1; + //assert(self.perms@.dom().contains(i)); + //assert(self.perms@[i]@.pptr == self.ptrs@[i]@); + //assert(self.perms@[i].value.is_Some()); + let next_of_i = self.next_of(i); + assert(0 ^ next_of_i == next_of_i) by (bit_vector); + //assert(self.prev_of(i) == second_to_last_ptr); + //assert(self.next_of(i) == new_ptr_int); + //assert(self.perms@[i].value.get_Some_0().xored == ( + // self.prev_of(i) ^ self.next_of(i) + //)); + assert(self.perms@.index(1).0@.value.get_Some_0().xored == new_ptr_u64 + ^ second_ptr); + assert(self.perms@.index(0).0@.value.get_Some_0().xored == head_ptr_u64); + assert(self.perms@.index(1).0@.pptr == head_ptr_u64 as int); + assert(self.wf_perm(1)); + assert(self.wf_perm(0)); + assert(forall|i: nat| + 1 <= i <= old(self).ptrs@.len() ==> old(self).wf_perm((i - 1) as nat) + ==> #[trigger] self.wf_perm(i)); + assert(self.wf_perms()); + assert(self.wf_tail()); + assert(self@[0] == v); + assert forall|i: int| 1 <= i <= self.ptrs@.len() - 1 implies old(self)@[i - 1] + == self@[i] by { + assert(old(self).wf_perm((i - 1) as nat)); // trigger + }; + assert(self@ =~= seq![v].add(old(self)@)); + } + } + } +} + +} // verus! diff --git a/source/cargo-verus-illustration/illustrate.sh b/source/cargo-verus-illustration/illustrate.sh new file mode 100755 index 0000000000..69c041c5b8 --- /dev/null +++ b/source/cargo-verus-illustration/illustrate.sh @@ -0,0 +1,53 @@ +#!/usr/bin/env bash + +# This script demonstrates the flow enabled by integration with Cargo. It can be run in a fresh +# checkout of the Verus repository. That is, it does not depend on Vargo or any other current Verus +# project build system code infrastructure. It does, however, require `$VERUS_Z3_PATH` and +# `$VERUS_SINGULAR_PATH` to be set. + +set -eu -o pipefail + +# ensure that VERUS_Z3_PATH and VERUS_SINGULAR_PATH are set +[ -n "$VERUS_Z3_PATH" ] +[ -n "$VERUS_SINGULAR_PATH" ] + +RUSTC_BOOTSTRAP=1 cargo build -p verus-driver --features singular + +cargo build -p cargo-verus + +target_dir=$(cd ../target && pwd) + +export PATH="$target_dir/debug:$PATH" + +# verify an example without codegen (like cargo check) and without applying rustc (like rust_verify +# without --compile) +cargo verus --check --just-verify -p doubly-linked-xor-test + +# verify an example without codegen (like cargo check) +cargo verus --check -p doubly-linked-xor-test + +# build and verify an example with codegen (like cargo build) +cargo verus -p doubly-linked-xor-test + +# this time with an argument for verus +cargo verus -p doubly-linked-xor-test -- --verus-arg=--rlimit=60 + +# run it +$target_dir/debug/doubly-linked-xor-test + +# build and verify example using pre-built sysroot + +verus_sysroot_parent=$(cd ../verus-sysroot-dummy && pwd) + +pushd $verus_sysroot_parent +./build-verus-sysroot.sh +popd + +verus_sysroot=$verus_sysroot_parent/verus-sysroot + +VERUS_SYSROOT=$verus_sysroot cargo verus -p doubly-linked-xor-test-using-verus-sysroot + +# specify sysroot another way + +cargo verus -p doubly-linked-xor-test-using-verus-sysroot -- \ + --verus-driver-arg=--verus-sysroot=$verus_sysroot