Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974#![feature(rustc_private)]#[macro_use]mod common;use common::*;
test_verify_one_file_with_options! { #[test] mut_param_with_loops [] => verus_code! { fn cond() -> bool { true }
fn test(mut x: u64) -> (y: u64) ensures x == y { let z = x; x = 5; return z; }
fn test_fails(mut x: u64) -> (y: u64) ensures x == y { x = 5; return 5; // FAILS }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop(mut x: u64) -> (y: u64) ensures x == y { loop { return x; } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails0(mut x: u64) -> (y: u64) ensures x == y { loop { let z = x; x = 5; return z; // FAILS (requires invariant relating x to old(x)) } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails(mut x: u64) -> (y: u64) ensures x == y { loop { x = 5; return 5; // FAILS } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails2(mut x: u64) -> (y: u64) ensures x == y { x = 1; loop { let z = x; return z; // FAILS } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails3(mut x: u64) -> (y: u64) ensures x == y { loop { if cond() { let z = x; return z; // FAILS } else { x = 1; } } } } => Err(err) => assert_fails(err, 5)}
test_verify_one_file_with_options! { #[test] mut_param_on_closure_with_loops [] => verus_code! { fn cond() -> bool { true }
fn test() { let r = |mut x: u64| -> (y: u64) ensures x == y { let z = x; x = 5; return z; }; }
fn test_fails() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { x = 5; return 5; }; }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop() { let r = |mut x: u64| -> (y: u64) ensures x == y { loop { return x; } }; }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails0() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS (requires invariant relating x to old(x)) { loop { let z = x; x = 5; return z; } }; }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { loop { x = 5; return 5; } }; }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails2() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { x = 1; loop decreases 0int { let z = x; return z; } }; }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails3() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { loop { if cond() { let z = x; return z; } else { x = 1; } } }; } } => Err(err) => assert_fails(err, 5)}
test_verify_one_file_with_options! { #[test] no_confusion_invariants_spec [] => verus_code! { use vstd::prelude::*;
struct X { }
impl vstd::invariant::InvariantPredicate<(), ()> for X { open spec fn inv(k: (), v: ()) -> bool { true } }
fn open(mut x: u64, Tracked(t): Tracked<&vstd::invariant::AtomicInvariant<(), (), X>>) requires t.namespace() == x + 1, x < 10, opens_invariants [x] { x = x + 1; vstd::invariant::open_atomic_invariant!(t => i => { }); } } => Err(err) => assert_vir_error_msg(err, "cannot show invariant namespace is in the mask given by the scope")}
test_verify_one_file_with_options! { #[test] no_confusion_unwind_spec [] => verus_code! { fn panic() { }
fn open(mut x: u64) no_unwind when x != 1 { x = 1; panic(); // FAILS } } => Err(err) => assert_fails(err, 1)}
test_verify_one_file_with_options! { #[test] no_confusion_ensures_recommend_check [] => verus_code! { spec fn rec(x: int) -> bool recommends x == 2 { false }
proof fn test_ens(mut x: int) ensures rec(x) { x = 2; } } => Err(err) => assert_has_recommends_failure(err)}
test_verify_one_file_with_options! { #[test] no_confusion_ensures_recommend_check_closure [] => verus_code! { spec fn rec(x: u64) -> bool recommends x == 2 { false }
fn test_ens() { let r = |mut x: u64| ensures rec(x) { x = 2; }; } } => Err(err) => assert_has_recommends_failure(err)}
test_verify_one_file_with_options! { #[test] no_confusion_decreases_clause [] => verus_code! { #[allow(unconditional_recursion)] fn test(mut x: u64) decreases x { x = 30; test(20); // FAILS } } => Err(err) => assert_fails(err, 1)}
test_verify_one_file_with_options! { #[test] mut_param_with_loops_iso_false [] => verus_code! { fn cond() -> bool { true }
fn test(mut x: u64) -> (y: u64) ensures x == y { let z = x; x = 5; return z; }
fn test_fails(mut x: u64) -> (y: u64) ensures x == y { x = 5; return 5; // FAILS }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop(mut x: u64) -> (y: u64) ensures x == y { loop { return x; } }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails0(mut x: u64) -> (y: u64) ensures x == y { loop { let z = x; x = 5; return z; // FAILS (requires invariant relating x to old(x)) } }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails(mut x: u64) -> (y: u64) ensures x == y { loop { x = 5; return 5; // FAILS } }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails2(mut x: u64) -> (y: u64) ensures x == y { x = 1; loop { let z = x; return z; // FAILS } }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails3(mut x: u64) -> (y: u64) ensures x == y { loop { if cond() { let z = x; return z; // FAILS } else { x = 1; } } } } => Err(err) => assert_fails(err, 5)}
test_verify_one_file_with_options! { #[test] mut_param_on_closure_with_loops_iso_false [] => verus_code! { fn cond() -> bool { true }
fn test() { let r = |mut x: u64| -> (y: u64) ensures x == y { let z = x; x = 5; return z; }; }
fn test_fails() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { x = 5; return 5; }; }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop() { let r = |mut x: u64| -> (y: u64) ensures x == y { loop { return x; } }; }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails0() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS (requires invariant relating x to old(x)) { loop { let z = x; x = 5; return z; } }; }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { loop { x = 5; return 5; } }; }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails2() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { x = 1; loop decreases 0int { let z = x; return z; } }; }
#[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] fn test_loop_fails3() { let r = |mut x: u64| -> (y: u64) ensures x == y // FAILS { loop { if cond() { let z = x; return z; } else { x = 1; } } }; } } => Err(err) => assert_fails(err, 5)}
test_verify_one_file_with_options! { #[test] mutation_conditional_cases [] => verus_code! { fn cond() -> bool { true }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test1(mut x: u64) -> (y: u64) ensures y == x { if cond() { x = 20; loop{} } else { loop { return x; // ok } } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test2(mut x: u64) -> (y: u64) ensures y == x { if cond() { loop { return x; // ok } } else { x = 20; loop{} } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test3(mut x: u64) -> (y: u64) ensures y == x { if cond() { loop{} } else { x = 20; loop { return x; // FAILS } } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test4(mut x: u64) -> (y: u64) ensures y == x { if cond() { x = 20; loop { return x; // FAILS } } else { loop{} } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test5(mut x: u64) -> (y: u64) ensures y == x { if cond() { x = 20; } else { }
loop { return x; // FAILS } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test6(mut x: u64) -> (y: u64) ensures y == x { if cond() { x = 20; }
loop { return x; // FAILS } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test7(mut x: u64) -> (y: u64) ensures y == x { if cond() { } else { x = 20; }
loop { return x; // FAILS } }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test8(mut x: u64) -> (y: u64) ensures y == x { x = 20;
if cond() { } else { }
loop { return x; // FAILS } } } => Err(err) => assert_fails(err, 6)}
test_verify_one_file_with_options! { #[test] mutation_nested_loop [] => verus_code! { fn cond() -> bool { true }
#[verifier::loop_isolation(true)] #[verifier::exec_allows_no_decreases_clause] fn test(mut x: u64) -> (y: u64) ensures y == x { loop { if cond() { return x; // FAILS }
loop { if cond() { x = 20; } if cond() { break; } } } } } => Err(err) => assert_fails(err, 1)}
test_verify_one_file_with_options! { #[test] patterns_in_param_position_without_macro [] => code! { #[verus::internal(verify)] fn add_pair((a, b): (i32, i32)) -> i32 { requires(a == 1 && b == 2); ensures(|result: i32| [result == a + b]); a + b }
#[verus::internal(verify)] fn ignore_arg(_: bool, value: i32, _: u64) -> i32 { ensures(|result: i32| [result == value]); value }
verus! { fn caller() { let r = add_pair((1, 2)); assert(r == 3); let result = ignore_arg(true, 10, 20); assert(result == 10); } } } => Ok(())}
test_verify_one_file_with_options! { #[test] param_patterns ["vstd", "--compile"] => verus_code! { fn first((x, _): (u32, u32)) -> (r: u32) ensures r == x { x }
fn swap<A, B>((a, b): (A, B)) -> (r: (B, A)) ensures r.0 == b && r.1 == a { (b, a) }
struct P { a: u64, b: u64 } struct W(u64, u64); struct V(u32);
fn nested(((a, b), P { a: c, .. }, W(d, _)): ((u8, u8), P, W)) -> (r: u64) requires c < 10, d < 10 ensures r == a + b + c + d { a as u64 + b as u64 + c + d }
fn single(V(x): V) -> (r: u32) ensures r == x { x }
fn refs(&(x, y): &(u32, u32)) -> (r: u32) requires x < 100, y < 100 ensures r == x + y { x + y }
fn mutate((mut x, y): (u32, u32)) -> (r: u32) ensures r == y { x = y; x }
fn by_ref(ref x: u32, ref s: String) -> (r: u32) ensures r == *x { *x }
fn wildcards<T>(_: T, value: u32, _: &mut u64) -> (r: u32) ensures r == value { value }
fn opaque(_: impl Sized, _: &impl Sized) -> (r: (impl Sized, bool)) ensures r.1 { (true, true) }
#[verifier::external_body] fn external_body((s, t): (String, String)) -> (r: String) ensures r == s { let _ = t; s }
#[verifier::external] fn external((s, t): (String, String)) -> (r: String) ensures r == s { let _ = t; s }
fn caller() { let r = first((1, 2)); assert(r == 1); let r = swap((1u8, true)); assert(r.0 && r.1 == 1); let r = nested(((1, 2), P { a: 3, b: 0 }, W(4, 9))); assert(r == 10); let r = single(V(3)); assert(r == 3); let r = refs(&(5, 6)); assert(r == 11); let mut value = 30u64; let r = wildcards(false, 20, &mut value); assert(r == 20); let r = opaque(true, &false); assert(r.1); }
fn double(a @ b: i32) -> (r: i32) requires -100 < a < 100 ensures r == 2 * a { a + b }
fn process(mut whole @ (a, b): (i32, i32)) -> (r: i32) requires whole.0 == 1, b == 2 ensures r == 4 { whole.0 = whole.0 + a; whole.0 + b }
fn incr(x @ _: &mut u32) requires *old(x) < 100 ensures *final(x) == *old(x) + 1 { *x = *x + 1; }
spec fn sum((a, b): (nat, nat)) -> nat decreases a { if a == 0 { b } else { sum(((a - 1) as nat, b)) } }
spec fn zero(_: int) -> int { 0 }
proof fn lemma((a, b): (nat, nat)) ensures sum((a, b)) >= b decreases a { if a > 0 { lemma(((a - 1) as nat, b)); } }
proof fn split<A, B>(tracked (a, b): (A, B)) -> (tracked r: A) ensures r == a { a }
proof fn ignore_ghost(_: int) {}
proof fn ignore_tracked<T>(tracked _: T) -> (r: bool) ensures r { true }
proof fn proof_caller<T>(tracked token: T) { ignore_ghost(10); let r = ignore_tracked(token); assert(r); assert(zero(20) == 0); }
fn opens((x, _): (u32, u32)) opens_invariants none no_unwind when x > 0 { } } => Ok(())}
test_verify_one_file_with_options! { #[test] param_patterns_false_postcondition [] => verus_code! { fn first((x, _): (u32, u32)) -> (r: u32) ensures r == x + 1 // FAILS { x }
fn opaque(_: impl Sized) -> (r: (impl Sized, bool)) ensures r.1 // FAILS { (true, false) } } => Err(err) => assert_fails(err, 2)}
test_verify_one_file_with_options! { #[test] wildcard_tracked_consumes_token [] => verus_code! { proof fn ignore<T>(tracked _: T) {}
proof fn caller<T>(tracked token: T) { ignore(token); ignore(token); } } => Err(err) => assert_rust_error_msg(err, "use of moved value")}
test_verify_one_file_with_options! { #[test] param_patterns_async ["vstd"] => code! { use vstd::prelude::*;
verus! { async fn ignore(_: String) -> (r: bool) ensures r { true }
async fn ignore_at(x @ _: u32) -> (r: u32) ensures r == x { x } }
#[verus_spec(r => ensures r)] async fn ignore_attr(_: String) -> bool { true }
verus! { async fn caller(s: String, t: String) { let r = ignore(s).await; assert(r); let r = ignore_attr(t).await; assert(r); let r = ignore_at(5).await; assert(r == 5); } } } => Ok(())}
test_verify_one_file_with_options! { #[test] wildcard_params_in_trait_methods [] => code! { #[verus::internal(verify)] trait Plain { fn m(&self, _: u32, _: u32); }
verus! { trait T { fn m(&self, _: u32, __verus_param_1: u32) -> (r: u32) ensures r == __verus_param_1; }
struct S;
impl T for S { fn m(&self, _: u32, x: u32) -> u32 { x } }
fn caller() { let r = S.m(1, 2); assert(r == 2); } }
trait A { #[verus_spec(r => ensures r == __verus_param_1)] fn m(&self, _: u32, __verus_param_1: u32) -> u32; } } => Ok(())}
// The generated names can't clash with user items ...test_verify_one_file_with_options! { #[test] param_name_hygiene_items [] => code! { const __verus_param_0: u32 = 0; struct __verus_param_1;
verus! { fn f(_: u32, _: bool) -> (r: u32) ensures r == 1 { fn __verus_param_0() -> bool { true } 1 } }
#[verus_spec(r => ensures r == 1)] fn g(_: u32, _: bool) -> u32 { fn __verus_param_0() -> bool { true } 1 } } => Ok(())}
// ... or with user variablestest_verify_one_file_with_options! { #[test] param_name_hygiene_variables [] => code! { verus! { fn f(_: u32, _: u32, __verus_param_0: u32) -> (__verus_param_1: u32) ensures __verus_param_1 == __verus_param_0 { let __verus_param_x @ (a, b) = (__verus_param_0, 0u32); __verus_param_x.0 } }
#[verus_spec(__verus_param_1 => ensures __verus_param_1 == __verus_param_0)] fn g(_: u32, _: u32, __verus_param_0: u32) -> u32 { let __verus_param_x @ (a, b) = (__verus_param_0, 0u32); __verus_param_x.0 }
verus! { fn param_binder(__verus_param_x @ (a, b): (u32, u32)) -> (r: u32) ensures r == a { __verus_param_x.0 }
fn ref_binder(ref __verus_param_x: u32) -> (r: u32) ensures r == *__verus_param_x { *__verus_param_x } } } => Ok(())}
test_verify_one_file_with_options! { #[test] param_patterns_async_unsupported [] => verus_code! { async fn f(x @ (a, b): (u32, u32)) -> u32 { a }
async fn g((x, _): (u32, u32)) -> (r: u32) ensures r == x { x } } => Err(err) => assert_vir_error_msgs(err, &[ "patterns in async function parameters are not supported", "patterns in async function parameters are not supported", ])}
test_verify_one_file_with_options! { #[test] param_patterns_unsupported [] => verus_code! { fn f<A, B>(tracked (a, b): (A, B)) {}
fn g((x, y): &mut (u64, u64)) {} } => Err(err) => assert_vir_error_msgs(err, &[ "patterns in ghost or tracked parameters of exec functions are not supported", "Verus does not currently support `ref mut` bindings in parameters", ])}
test_verify_one_file_with_options! { #[test] wildcard_param_assume_specification_unsupported [] => verus_code! { #[verifier::external] fn foo(x: u32) -> u32 { x }
pub assume_specification[foo](_: u32) -> u32; } => Err(err) => assert_vir_error_msg(err, "'assume_specification' expects ident, not complex pattern")}