Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247#![feature(rustc_private)]#[macro_use]mod common;use common::*;
test_verify_one_file! { #[test] test1 verus_code! { #[verifier(inline)] spec fn fi(x: int, y: int) -> int { x + 2 * y }
spec fn f1(x: int, y: int) -> int { x + 2 * y }
#[verifier(inline)] spec fn f2(x: int, y: int) -> int { f1(x, y) }
#[verifier(inline)] spec fn f3(a: int, b: int) -> int { f1(a, b) }
#[verifier(inline)] spec fn f4(a: int, b: int) -> int { let za = a + 1; let zb = b + 1; f1(za - 1, zb - 1) }
#[verifier(inline)] spec fn fg<A, B>(a: A, b: B) -> (B, A) { (b, a) }
uninterp spec fn fx(x: int) -> bool;
#[verifier(inline)] spec fn fy(x: int) -> bool { fx(x) }
uninterp spec fn fpx<A>(x: A) -> bool;
#[verifier(inline)] spec fn fpy<A>(x: A) -> bool { fpx(x) }
proof fn test() requires forall|i: int| fy(i), forall|i: u8| fpy(i), { assert(fi(33, 44) == 121); assert(f1(33, 44) == 121); assert(f2(33, 44) == 121); assert(f3(33, 44) == 121); assert({let za = 44; f4(33, za) == 121}); assert(fg(10u8, true) == (true, 10u8)); assert(fx(7)); assert(fy(6)); assert(fpx(7u8)); assert(fpy(6u8)); } } => Ok(())}
test_verify_one_file! { #[test] test_private_fails verus_code! { #[verifier(inline)] pub closed spec fn f(x: int, y: int) -> int { x + 2 * y } } => Err(err) => assert_vir_error_msg(err, "`inline` is only allowed for private or `open spec` functions")}
test_verify_one_file! { #[test] test_nonspec_fails verus_code! { #[verifier(inline)] proof fn f() { } } => Err(err) => assert_vir_error_msg(err, "`inline` is only allowed for `spec` functions")}
test_verify_one_file! { #[test] test_rec_fails1 verus_code! { #[verifier(inline)] spec fn f(n: nat) -> nat decreases n { 0 } } => Err(err) => assert_vir_error_msg(err, "`inline` functions cannot be recursive")}
test_verify_one_file! { #[test] test_rec_fails2 verus_code! { #[verifier(inline)] spec fn f(n: nat) -> nat { if n == 0 { 0 } else { f((n - 1) as nat) } } } => Err(err) => assert_vir_error_msg(err, "recursive function must have a `decreases` clause")}
test_verify_one_file! { #[test] test_no_body_fails verus_code! { #[verifier(inline)] spec fn f(n: nat) -> nat; } => Err(err) => assert_vir_error_msg(err, "`inline` functions must have a body")}
test_verify_one_file! { #[test] test_spec_fn verus_code! { #[verifier(inline)] spec fn f1(i: int, j: int) -> bool { i <= j }
#[verifier(inline)] spec fn f2(i: int, j: int) -> bool { let x = i; let y = j; x < y }
#[verifier(opaque)] spec fn f3(i: int, j: int) -> bool { f1(j, i) }
fn test_spec_fn(a: int, b: int) { hide(f2);
assume(f2(a, b)); proof { reveal(f2); } assert(f1(a, b));
proof { reveal(f3); } assert(f3(b, a)); assert(f3(a, b)); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] test_ensures_type_inference verus_code! { struct Foo { pub b: bool, }
#[verifier(inline)] spec fn get_b(foo: Foo) -> bool { foo.b }
fn test1() -> (b: Foo) ensures get_b(b) { Foo { b: true } } } => Ok(())}
test_verify_one_file! { #[test] inline_poly verus_code! { use vstd::prelude::*;
#[verifier::inline] spec fn all_contains<A>(s1: Set<A>) -> bool { forall|a: A| s1.contains(a) }
proof fn failing_proof(s: Set<int>) { assert(all_contains(s)); // FAILS } } => Err(err) => assert_one_fails(err)}
test_verify_one_file! { #[test] inline_poly_assoc_type verus_code! { // https://github.com/verus-lang/verus/issues/1303 use vstd::prelude::*; pub type SpecBytes = Seq<u8>; pub type Bytes<'a> = &'a [u8];
pub enum SpecMsg { M0(SpecBytes), }
pub enum Msg<'a> { M0(Bytes<'a>), }
impl View for Msg<'_> { type V = SpecMsg;
open spec fn view(&self) -> Self::V { match self { Msg::M0(m) => SpecMsg::M0(m@), } } } } => Ok(())}
test_verify_one_file! { #[test] default_impl_issue1407 verus_code! { trait Tr { #[verifier::inline] spec fn foo(&self) -> bool { true } }
struct X { }
impl Tr for X { spec fn foo(&self) -> bool { false } }
#[verifier::inline] spec fn foo_wrapper_inlined<T: Tr>(t: &T) -> bool { t.foo() }
proof fn test4() { let x = X { }; assert(foo_wrapper_inlined(&x)); // FAILS }
proof fn test5<T: Tr>(t: &T) { assert(foo_wrapper_inlined(t)); // FAILS } } => Err(err) => assert_fails(err, 2)}