From acbd12f656e88abc309b287b49217803b7fd93ac 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 | 7 + .../Cargo.toml | 11 + .../src | 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 ++ .../rust-verify-examples/.gitignore | 2 + .../rust-verify-examples/Cargo.toml | 446 ++++++++++++++++ .../rust-verify-examples/helper.py | 52 ++ .../rust-verify-examples/link | 1 + .../rust-verify-examples/src/lib.rs | 1 + 14 files changed, 1147 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 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 create mode 100644 source/cargo-verus-illustration/rust-verify-examples/.gitignore create mode 100644 source/cargo-verus-illustration/rust-verify-examples/Cargo.toml create mode 100755 source/cargo-verus-illustration/rust-verify-examples/helper.py create mode 120000 source/cargo-verus-illustration/rust-verify-examples/link create mode 100644 source/cargo-verus-illustration/rust-verify-examples/src/lib.rs 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..7bac1acc0d 100644 --- a/source/Cargo.toml +++ b/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 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 b/source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/src new file mode 120000 index 0000000000..f114cd3448 --- /dev/null +++ b/source/cargo-verus-illustration/doubly-linked-xor-test-using-verus-sysroot/src @@ -0,0 +1 @@ +../doubly-linked-xor/src/ \ 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..212d1cd357 --- /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 + +# require VERUS_Z3_PATH and VERUS_SINGULAR_PATH to be set +[ -n "$VERUS_Z3_PATH" ] +[ -n "$VERUS_SINGULAR_PATH" ] + +# for using nightly-only features on stable +export RUSTC_BOOTSTRAP=1 + +cargo build -p verus-driver --features singular + +# verify an example without codegen (like cargo check) and without applying rustc (like rust_verify without --compile) +cargo run -p cargo-verus -- --check --just-verify -p doubly-linked-xor-test + +# verify an example without codegen (like cargo check) +cargo run -p cargo-verus -- --check -p doubly-linked-xor-test + +# build and verify an example with codegen (like cargo build) +cargo run -p cargo-verus -- -p doubly-linked-xor-test + +# this time with an argument for verus +cargo run -p cargo-verus -- -p doubly-linked-xor-test -- --verus-arg=--rlimit=60 + +# run it +../target/debug/doubly-linked-xor-test + +# build and verify examples from ../rust_verify/example +cargo run -p cargo-verus -- --manifest-path rust-verify-examples/Cargo.toml --examples + +# build and verify example using pre-built sysroot + +verus_sysroot_parent=$(realpath ../verus-sysroot-dummy) + +pushd $verus_sysroot_parent +./build-verus-sysroot.sh +popd + +verus_sysroot=$verus_sysroot_parent/verus-sysroot + +VERUS_SYSROOT=$verus_sysroot \ + cargo run -p cargo-verus -- -p doubly-linked-xor-test-using-verus-sysroot + +# specify sysroot another way + +cargo run -p cargo-verus -- -p doubly-linked-xor-test-using-verus-sysroot -- \ + --verus-driver-arg=--verus-sysroot=$verus_sysroot diff --git a/source/cargo-verus-illustration/rust-verify-examples/.gitignore b/source/cargo-verus-illustration/rust-verify-examples/.gitignore new file mode 100644 index 0000000000..042776aad7 --- /dev/null +++ b/source/cargo-verus-illustration/rust-verify-examples/.gitignore @@ -0,0 +1,2 @@ +/Cargo.lock +/target/ diff --git a/source/cargo-verus-illustration/rust-verify-examples/Cargo.toml b/source/cargo-verus-illustration/rust-verify-examples/Cargo.toml new file mode 100644 index 0000000000..4ff2d97525 --- /dev/null +++ b/source/cargo-verus-illustration/rust-verify-examples/Cargo.toml @@ -0,0 +1,446 @@ +[package] +name = "rust-verify-examples" +version = "0.1.0" +edition = "2021" + +[dependencies] +builtin = { path = "../../builtin" } +builtin_macros = { path = "../../builtin_macros" } +state_machines_macros = { path = "../../state_machines_macros" } +vstd = { path = "../../vstd" } + +[package.metadata.verus] +verify = true + +# generated by helpers.py + +[[example]] +name = "adts" +path = "link/adts.rs" + +[[example]] +name = "adts_eq" +path = "link/adts_eq.rs" + +[[example]] +name = "assert_by_compute" +path = "link/assert_by_compute.rs" + +[[example]] +name = "assorted_demo" +path = "link/assorted_demo.rs" + +[[example]] +name = "atomics" +path = "link/atomics.rs" + +[[example]] +name = "bitmap" +path = "link/bitmap.rs" + +[[example]] +name = "bitvector_basic" +path = "link/bitvector_basic.rs" + +[[example]] +name = "bitvector_equivalence" +path = "link/bitvector_equivalence.rs" + +[[example]] +name = "bitvector_garbage_collection" +path = "link/bitvector_garbage_collection.rs" + +[[example]] +name = "calc" +path = "link/calc.rs" + +[[example]] +name = "cells" +path = "link/cells.rs" + +[[example]] +name = "datatypes" +path = "link/datatypes.rs" + +[[example]] +name = "doubly_linked" +path = "link/doubly_linked.rs" + +[[example]] +name = "doubly_linked_xor" +path = "link/doubly_linked_xor.rs" + +[[example]] +name = "even_cell" +path = "link/even_cell.rs" + +[[example]] +name = "extensionality" +path = "link/extensionality.rs" + +[[example]] +name = "external" +path = "link/external.rs" + +[[example]] +name = "fun_ext" +path = "link/fun_ext.rs" + +[[example]] +name = "generics" +path = "link/generics.rs" + +[[example]] +name = "guide-assert_by_compute" +path = "link/guide/assert_by_compute.rs" + +[[example]] +name = "guide-calc" +path = "link/guide/calc.rs" + +[[example]] +name = "guide-equality" +path = "link/guide/equality.rs" + +[[example]] +name = "guide-ext_equal" +path = "link/guide/ext_equal.rs" + +[[example]] +name = "guide-getting_started" +path = "link/guide/getting_started.rs" + +[[example]] +name = "guide-integers" +path = "link/guide/integers.rs" + +[[example]] +name = "guide-interior_mutability" +path = "link/guide/interior_mutability.rs" + +[[example]] +name = "guide-lib_examples" +path = "link/guide/lib_examples.rs" + +[[example]] +name = "guide-modes" +path = "link/guide/modes.rs" + +[[example]] +name = "guide-nonlinear_bitvec" +path = "link/guide/nonlinear_bitvec.rs" + +[[example]] +name = "guide-pervasive_example" +path = "link/guide/pervasive_example.rs" + +[[example]] +name = "guide-quants" +path = "link/guide/quants.rs" + +[[example]] +name = "guide-recursion" +path = "link/guide/recursion.rs" + +[[example]] +name = "guide-requires_ensures" +path = "link/guide/requires_ensures.rs" + +[[example]] +name = "guide-requires_ensures_edit" +path = "link/guide/requires_ensures_edit.rs" + +[[example]] +name = "imo_1988_6" +path = "link/imo_1988_6.rs" + +[[example]] +name = "impl_basic" +path = "link/impl_basic.rs" + +[[example]] +name = "integer_ring-circular_by_d" +path = "link/integer_ring/circular_by_d.rs" + +[[example]] +name = "integer_ring-integer_ring" +path = "link/integer_ring/integer_ring.rs" + +[[example]] +name = "integer_ring-integer_ring_bound_check" +path = "link/integer_ring/integer_ring_bound_check.rs" + +[[example]] +name = "integers" +path = "link/integers.rs" + +[[example]] +name = "invariants" +path = "link/invariants.rs" + +[[example]] +name = "modules" +path = "link/modules.rs" + +[[example]] +name = "multiset" +path = "link/multiset.rs" + +[[example]] +name = "nevd_script" +path = "link/nevd_script.rs" + +[[example]] +name = "pcm-agreement" +path = "link/pcm/agreement.rs" + +[[example]] +name = "pcm-count_to_two" +path = "link/pcm/count_to_two.rs" + +[[example]] +name = "pcm-log" +path = "link/pcm/log.rs" + +[[example]] +name = "pcm-main" +path = "link/pcm/main.rs" + +[[example]] +name = "pcm-monotonic_counter" +path = "link/pcm/monotonic_counter.rs" + +[[example]] +name = "pcm-oneshot" +path = "link/pcm/oneshot.rs" + +[[example]] +name = "playground" +path = "link/playground.rs" + +[[example]] +name = "power_of_2" +path = "link/power_of_2.rs" + +[[example]] +name = "prelude" +path = "link/prelude.rs" + +[[example]] +name = "proposal-rw2022" +path = "link/proposal-rw2022.rs" + +[[example]] +name = "quantifiers" +path = "link/quantifiers.rs" + +[[example]] +name = "recommends" +path = "link/recommends.rs" + +[[example]] +name = "recursion" +path = "link/recursion.rs" + +[[example]] +name = "recursive_types" +path = "link/recursive_types.rs" + +[[example]] +name = "rfmig_script" +path = "link/rfmig_script.rs" + +[[example]] +name = "rw2022_script" +path = "link/rw2022_script.rs" + +[[example]] +name = "set_from_vec" +path = "link/set_from_vec.rs" + +[[example]] +name = "state_machines-adder" +path = "link/state_machines/adder.rs" + +[[example]] +name = "state_machines-adder_generic" +path = "link/state_machines/adder_generic.rs" + +[[example]] +name = "state_machines-adder_with_max" +path = "link/state_machines/adder_with_max.rs" + +[[example]] +name = "state_machines-arc" +path = "link/state_machines/arc.rs" + +[[example]] +name = "state_machines-conditional" +path = "link/state_machines/conditional.rs" + +[[example]] +name = "state_machines-dist_rwlock" +path = "link/state_machines/dist_rwlock.rs" + +[[example]] +name = "state_machines-flat_combine" +path = "link/state_machines/flat_combine.rs" + +[[example]] +name = "state_machines-interner" +path = "link/state_machines/interner.rs" + +[[example]] +name = "state_machines-leader_election_complete" +path = "link/state_machines/leader_election_complete.rs" + +[[example]] +name = "state_machines-maps" +path = "link/state_machines/maps.rs" + +[[example]] +name = "state_machines-petersons_algorithm" +path = "link/state_machines/petersons_algorithm.rs" + +[[example]] +name = "state_machines-reference-examples-strategy_option" +path = "link/state_machines/reference-examples/strategy_option.rs" + +[[example]] +name = "state_machines-refinement" +path = "link/state_machines/refinement.rs" + +[[example]] +name = "state_machines-refinement_labels" +path = "link/state_machines/refinement_labels.rs" + +[[example]] +name = "state_machines-rwlock" +path = "link/state_machines/rwlock.rs" + +[[example]] +name = "state_machines-top_sort_dfs" +path = "link/state_machines/top_sort_dfs.rs" + +[[example]] +name = "state_machines-tutorial-counting_to_2" +path = "link/state_machines/tutorial/counting_to_2.rs" + +[[example]] +name = "state_machines-tutorial-counting_to_n" +path = "link/state_machines/tutorial/counting_to_n.rs" + +[[example]] +name = "state_machines-tutorial-counting_to_n_atomic" +path = "link/state_machines/tutorial/counting_to_n_atomic.rs" + +[[example]] +name = "state_machines-tutorial-fifo" +path = "link/state_machines/tutorial/fifo.rs" + +[[example]] +name = "state_machines-tutorial-pcell_example" +path = "link/state_machines/tutorial/pcell_example.rs" + +[[example]] +name = "state_machines-tutorial-rc" +path = "link/state_machines/tutorial/rc.rs" + +[[example]] +name = "state_machines-tutorial-ref_cell" +path = "link/state_machines/tutorial/ref_cell.rs" + +[[example]] +name = "state_machines-tutorial-unverified_counting_to_2" +path = "link/state_machines/tutorial/unverified_counting_to_2.rs" + +[[example]] +name = "state_machines-tutorial-unverified_counting_to_n" +path = "link/state_machines/tutorial/unverified_counting_to_n.rs" + +[[example]] +name = "state_machines-tutorial-unverified_fifo" +path = "link/state_machines/tutorial/unverified_fifo.rs" + +[[example]] +name = "state_machines-tutorial-unverified_rc" +path = "link/state_machines/tutorial/unverified_rc.rs" + +[[example]] +name = "statements" +path = "link/statements.rs" + +[[example]] +name = "statics" +path = "link/statics.rs" + +[[example]] +name = "std_test-num" +path = "link/std_test/num.rs" + +[[example]] +name = "std_test-option_test" +path = "link/std_test/option_test.rs" +crate-type = ["lib"] + +[[example]] +name = "std_test-result" +path = "link/std_test/result.rs" +crate-type = ["lib"] + +[[example]] +name = "std_test-template" +path = "link/std_test/template.rs" +crate-type = ["lib"] + +[[example]] +name = "structural" +path = "link/structural.rs" + +[[example]] +name = "summer_school-chapter-1-22" +path = "link/summer_school/chapter-1-22.rs" + +[[example]] +name = "summer_school-chapter-2-1" +path = "link/summer_school/chapter-2-1.rs" + +[[example]] +name = "summer_school-chapter-2-2" +path = "link/summer_school/chapter-2-2.rs" + +[[example]] +name = "summer_school-chapter-2-3" +path = "link/summer_school/chapter-2-3.rs" + +[[example]] +name = "summer_school-chapter-6-1" +path = "link/summer_school/chapter-6-1.rs" + +[[example]] +name = "syntax" +path = "link/syntax.rs" + +[[example]] +name = "test" +path = "link/test.rs" + +[[example]] +name = "thread" +path = "link/thread.rs" + +[[example]] +name = "trait_for_fn" +path = "link/trait_for_fn.rs" + +[[example]] +name = "traits" +path = "link/traits.rs" + +[[example]] +name = "vectors" +path = "link/vectors.rs" + +[[example]] +name = "verified_vec" +path = "link/verified_vec.rs" diff --git a/source/cargo-verus-illustration/rust-verify-examples/helper.py b/source/cargo-verus-illustration/rust-verify-examples/helper.py new file mode 100755 index 0000000000..c79f3ddf23 --- /dev/null +++ b/source/cargo-verus-illustration/rust-verify-examples/helper.py @@ -0,0 +1,52 @@ +#!/usr/bin/env python3 + +from pathlib import Path +import subprocess + +BLOCKLIST = set([ + # supposed to fail + "assertions.rs", + "debug.rs", + "debug_expand.rs", + "test_expand_errors.rs", + "trigger_loops.rs", + "guide/higher_order_fns.rs", + # failing because out-of-date + "state_machines/disk_example.rs", + "scache/rwlock.rs" + ]) + +LIB_ONLY = set([ + "std_test/option_test.rs", + "std_test/result.rs", + "std_test/template.rs", + ]) + +def main(): + completed = subprocess.run( + ['find', 'link/', '-type', 'f', '-name', '*.rs', '-printf', '%P\n'], + stdout=subprocess.PIPE, + text=True, + check=True, + ) + + print() + print('# generated by helpers.py') + + for path in sorted(completed.stdout.splitlines()): + if path in BLOCKLIST: + continue + + structured_path = Path(path) + name = '-'.join((structured_path.parent / structured_path.stem).parts) + + print() + print('[[example]]') + print(f'name = "{name}"') + print(f'path = "link/{path}"') + + if path in LIB_ONLY: + print('crate-type = ["lib"]') + +if __name__ == '__main__': + main() diff --git a/source/cargo-verus-illustration/rust-verify-examples/link b/source/cargo-verus-illustration/rust-verify-examples/link new file mode 120000 index 0000000000..3373e99670 --- /dev/null +++ b/source/cargo-verus-illustration/rust-verify-examples/link @@ -0,0 +1 @@ +../../rust_verify/example/ \ No newline at end of file diff --git a/source/cargo-verus-illustration/rust-verify-examples/src/lib.rs b/source/cargo-verus-illustration/rust-verify-examples/src/lib.rs new file mode 100644 index 0000000000..48630b0fb6 --- /dev/null +++ b/source/cargo-verus-illustration/rust-verify-examples/src/lib.rs @@ -0,0 +1 @@ +// dummy