Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345#![feature(rustc_private)]#[macro_use]mod common;use common::*;
test_verify_one_file! { #[test] test1 verus_code! { spec fn tr(i: int) -> bool { true }
proof fn test1() { assert(tr(300)); assert(exists|i: nat| i >= 0 && tr(i as int)); }
proof fn test1_inference() { assert(tr(300)); assert(exists|i| 0 <= i && tr(i)); } } => Ok(())}
test_verify_one_file! { #[test] test1_fails verus_code! { spec fn tr(i: int) -> bool { true }
proof fn test1() { assert(exists|i: nat| i >= 0 && tr(i as int)); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test2 verus_code! { spec fn tr1(i: int) -> bool { true }
spec fn tr2(i: int) -> bool { true }
proof fn test1() { assert(tr1(300)); assert(exists|i: nat| i >= 0 && tr1(i as int) && tr2(i as int)); } } => Ok(())}
test_verify_one_file! { #[test] test3 verus_code! { spec fn tr1(i: int) -> bool { true }
spec fn tr2(i: int) -> bool { true }
proof fn test1() { assert(tr2(300)); assert(exists|i: nat| i >= 0 && tr1(i as int) && tr2(i as int)); } } => Ok(())}
////
test_verify_one_file! { #[test] test1g verus_code! { spec fn tr<A>(a: A) -> bool { true }
proof fn test1() { assert(tr::<nat>(300)); assert(exists|i: nat| i >= 0 && tr(i)); } } => Ok(())}
test_verify_one_file! { #[test] test1g_fails verus_code! { spec fn tr<A>(a: A) -> bool { true }
proof fn test1() { assert(exists|i: nat| i >= 0 && tr(i)); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test2g verus_code! { spec fn tr1<A>(a: A) -> bool { true }
spec fn tr2<A>(a: A) -> bool { true }
proof fn test1() { assert(tr1::<nat>(300)); assert(exists|i: nat| i >= 0 && tr1(i) && tr2(i)); } } => Ok(())}
test_verify_one_file! { #[test] test3g verus_code! { spec fn tr1<A>(a: A) -> bool { true }
spec fn tr2<A>(a: A) -> bool { true }
proof fn test1() { assert(tr2::<nat>(300)); assert(exists|i: nat| i >= 0 && tr1(i) && tr2(i)); } } => Ok(())}
////
test_verify_one_file! { #[test] test4 verus_code! { spec fn tr1(i: int) -> bool { true }
spec fn tr2(i: int) -> bool { true }
proof fn test1() { assert(tr2(300)); assert(exists|i: nat| i >= 0 && tr1(i as int) && #[trigger] tr2(i as int)); } } => Ok(())}
test_verify_one_file! { #[test] test4_fails verus_code! { spec fn tr1(i: int) -> bool { true }
spec fn tr2(i: int) -> bool { true }
proof fn test1() { assert(tr1(300)); assert(exists|i: nat| i >= 0 && tr1(i as int) && #[trigger] tr2(i as int)); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_nested_assert_forall_by_regression_155 verus_code! { use vstd::map::*;
pub proof fn test<S, T>() { assert forall |m1: Map<S, T>, m2: Map<S, T>, n: S| m1.dom().contains(n) && !m2.dom().contains(n) implies equal(m1.remove(n).union_prefer_right(m2), m1.union_prefer_right(m2).remove(n)) by { let union1 = m1.remove(n).union_prefer_right(m2); let union2 = m1.union_prefer_right(m2).remove(n); assert_maps_equal!(union1, union2); assert(equal(m1.remove(n).union_prefer_right(m2), union2)); assert(equal(union1, m1.union_prefer_right(m2).remove(n))); } }
pub proof fn test_forall_forall<S, T>() { assert forall |m1: Map<S, T>, m2: Map<S, T>, n: S| m1.dom().contains(n) && !m2.dom().contains(n) implies equal(m1.remove(n).union_prefer_right(m2), m1.union_prefer_right(m2).remove(n)) by {
let union1 = m1.remove(n).union_prefer_right(m2); let union2 = m1.union_prefer_right(m2).remove(n);
let mm1 = union1; let mm2 = union2;
assert(equal(mm1, mm2)) by { assert forall |key| imply(#[trigger] mm1.dom().contains(key), mm2.dom().contains(key)) && imply(mm2.dom().contains(key), mm1.dom().contains(key)) && imply(mm1.dom().contains(key) && mm2.dom().contains(key), equal(mm1.index(key), mm2.index(key))) by { {} } assert(mm1 =~= mm2); }
assume(equal(union1, union2)); assert(equal(m1.remove(n).union_prefer_right(m2), union2)); assert(equal(union1, m1.union_prefer_right(m2).remove(n))); } } } => Ok(())}
test_verify_one_file! { #[test] manual_trigger verus_code! { use vstd::seq::*; proof fn test_distinct3(s: Seq<int>) requires 5 <= s.len(), forall|i: int, j: int| #![trigger s[i], s[j]] 0 <= i < j < s.len() ==> s[i] != s[j], { assert(s[4] != s[2]); } } => Ok(())}
test_verify_one_file! { #[test] assert_forall_triggers_regression_335 verus_code! { spec fn f(x:int, y:int) -> bool { true } spec fn g(x:int, y:int) -> bool { true } spec fn h(x:int, y:int) -> bool { true } spec fn i(x:int, y:int) -> int { 5 }
proof fn test(z:int) { assert forall |k:int| #![trigger f(k, z)] f(k, z) && g(z, k) ==> f(z, i(z, k)) by { }; } } => Ok(())}
test_verify_one_file! { #[test] assert_forall_triggers_regression_470 verus_code! { spec fn f(x:int, y:int) -> bool { true } spec fn g(x:int, y:int) -> bool { true } spec fn h(x:int, y:int) -> bool { true } spec fn i(x:int, y:int) -> int { 5 }
proof fn test(z:int) { assert forall |k:int| #![auto] f(k, z) && g(z, k) ==> f(z, i(z, k)) by { }; } } => Ok(())}
test_verify_one_file! { #[test] assert_forall_invalid_attr verus_code! { spec fn f(x:int) -> bool { true }
proof fn test(z:int) { assert forall |k:int| #![autos] f(k) by { }; } } => Err(err) => assert_vir_error_msg(err, "expected trigger")}
test_verify_one_file! { #[test] forall_auto_parens_regression_378 verus_code! { use vstd::seq::*; proof fn foo(s: Seq<int>) requires 5 <= s.len(), forall (|i: int, j: int| #![auto] 0 <= i < j < s.len() ==> s[i] != s[j]), { assert(s[4] != s[2]); } } => Err(err) => assert_vir_error_msg(err, "forall, choose, and exists do not allow parentheses")}
test_verify_one_file! { #[test] test_inner_triggers_broadcast_forall verus_code! { mod M { pub struct A {} impl A { pub uninterp spec fn f1(&self) -> bool; pub uninterp spec fn f2(&self) -> bool; pub uninterp spec fn f3(&self) -> bool; }
#[verifier::external_body] pub broadcast proof fn ab(a: A) ensures #![trigger a.f1()] (a.f1() ==> a.f2()) && a.f3() { } }
use M::*; proof fn p(a: A) requires a.f1(), ensures a.f2(), { broadcast use ab; } } => Ok(())}
test_verify_one_file! { #[test] test_ensures_malformed_trigger_regression_3188 code! { use vstd::prelude::*; verus! { spec fn double(x: int) -> int { 2 * x } spec fn half(x: int) -> int { x / 2 } fn compute(x: u32) -> (r: u64) requires x < 1000, ensures #![trigger double(x as int) half(r as int)] r == double(x as int), { (x as u64) * 3 } } fn main() { let r = compute(5); println!("compute(5) = {} (verified ensures: r == 10)", r); } } => Err(err) => assert_vir_error_msg(err, "unexpected token")}
test_verify_one_file! { #[test] test_trigger_with_expression_should_be_disallowed_regression_1456 verus_code! { spec fn a(x: int) -> bool; spec fn b(x: int) -> bool; spec fn c(x: int) -> bool;
proof fn test(i: int) requires forall|x: int| #[trigger a(x)] c(x) && (a(x) ==> b(x)), a(i), ensures b(i), {
} } => Err(err) => assert_vir_error_msg(err, "invalid trigger attribute: to provide a trigger expression, use the `#![trigger <expr>]` attribute")}