Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196#![feature(rustc_private)]#[macro_use]mod common;use common::*;
const STRUCTS: &str = verus_code_str! { #[derive(PartialEq, Eq, Structural)] struct Car { four_doors: bool, passengers: u64, }
#[derive(PartialEq, Eq, Structural)] enum Vehicle { Car(Car), Train(bool), }};
test_verify_one_file! { #[test] test_structural_eq STRUCTS.to_string() + verus_code_str! { fn test_structural_eq(passengers: u64) { let c1 = Car { passengers, four_doors: true }; let c2 = Car { passengers, four_doors: false }; let c3 = Car { passengers, four_doors: true };
assert(c1 == c3); assert(c1 != c2);
let t = Vehicle::Train(true); let ca = Vehicle::Car(c1);
assert(t != ca); assert(t == ca); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_not_structural_generic verus_code! { #[derive(PartialEq, Eq, Structural)] struct Thing<V> { v: V, }
#[derive(Eq, Structural)] struct Other { }
impl std::cmp::PartialEq for Other { fn eq(&self, other: &Self) -> bool { false } }
fn test_not_structural(passengers: u64) { let v1 = Thing { v: true }; let v2 = Thing { v: true }; assert(v1 == v2); } } => Err(err) => assert_vir_error_msg(err, "structural impl for non-structural type Other")}
test_verify_one_file! { #[test] test_not_structural_fields verus_code! { #[derive(PartialEq, Eq)] struct Other { }
#[derive(PartialEq, Eq, Structural)] struct Thing { o: Other, } } => Err(err) => assert_rust_error_msg(err, "the trait bound `Other: verus_builtin::Structural` is not satisfied")}
test_verify_one_file! { #[test] test_structural_ghost_field verus_code! { #[derive(PartialEq, Structural)] struct S { ghost g: bool } } => Err(err) => assert_vir_error_msg(err, "`Structural` types cannot have ghost or tracked fields")}
test_verify_one_file_with_options! { #[test] test_structural_spoofed_derived_partial_eq ["no-auto-import-verus_builtin"] => code_str! { #![feature(structural_match)] use vstd::prelude::*; }.to_string() + verus_code_str! { #[derive(Structural)] struct T(u8);
#[automatically_derived] impl core::marker::StructuralPartialEq for T {}
impl vstd::std_specs::cmp::PartialEqSpecImpl for T { open spec fn obeys_eq_spec() -> bool { false } open spec fn eq_spec(&self, other: &T) -> bool { false } }
#[automatically_derived] impl PartialEq for T { fn eq(&self, other: &T) -> bool { false } } } => Err(err) => assert_vir_error_msg(err, "`Structural` requires a built-in derived `PartialEq` implementation")}
test_verify_one_file! { #[test] test_structural_enum_with_values verus_code! { #[derive(PartialEq, Structural)] pub enum ValueStatus { Valid = 0, Invalid = 1, } } => Ok(())}
test_verify_one_file! { // https://github.com/verus-lang/verus/issues/178 #[test] test_result_is_structural verus_code! { use vstd::prelude::*;
fn eq_generic<T: PartialEq + Structural>(a: &T, b: &T) -> (r: bool) ensures r == (a == b), { a == b }
fn test_result(a: Result<u32, u32>, b: Result<u32, u32>) { let r = eq_generic(&a, &b); assert(r == (a == b)); } } => Ok(())}
test_verify_one_file! { // https://github.com/verus-lang/verus/issues/178 #[test] test_tuple_is_structural verus_code! { use vstd::prelude::*;
fn eq_generic<T: PartialEq + Structural>(a: &T, b: &T) -> (r: bool) ensures r == (a == b), { a == b }
fn test_tuple(a: (u32, bool), b: (u32, bool)) { let r = eq_generic(&a, &b); assert(r == (a == b)); } } => Ok(())}
test_verify_one_file! { // https://github.com/verus-lang/verus/issues/178 #[test] test_array_is_structural verus_code! { use vstd::prelude::*;
fn eq_generic<T: PartialEq + Structural>(a: &T, b: &T) -> (r: bool) ensures r == (a == b), { a == b }
fn test_array(a: [u32; 3], b: [u32; 3]) { let r = eq_generic(&a, &b); assert(r == (a == b)); } } => Ok(())}
test_verify_one_file_with_options! { #[test] test_structural_trait_bound ["exec_allows_no_decreases_clause"] => verus_code! { use vstd::prelude::*;
// Structural required for Rust eq to connect to SMT == pub struct VecMap<Key,Value> where Key: View + Eq + Structural { v: Vec<(Key,Value)> }
impl<Key,Value> VecMap<Key,Value> where Key: View + Eq + Structural { pub fn get<'a>(&'a self, k: &Key) -> (result: Option<&'a Value>) { let mut i: usize = 0; while i < self.v.len() { if &self.v[i].0 == k { return Some(&self.v[i].1) } } None } }
} => Ok(())}