Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239// rust_verify/tests/example.rs expand-errors#![allow(unused_imports)]
use verus_builtin::*;use verus_builtin_macros::*;use vstd::map::*;use vstd::modes::*;use vstd::prelude::*;use vstd::seq::*;use vstd::*;
verus! {
spec fn e() -> bool;
spec fn f() -> bool;
spec fn g() -> bool;
spec fn h() -> bool;
spec fn k(i: int) -> bool;
spec fn z() -> bool { (e() ==> h()) && (forall|i: int| k(i))}
spec fn stuff() -> bool { f() && g() && z()}
proof fn test() requires f(),{ assert(stuff());}
proof fn test_ret() ensures z(),{}
pub spec fn ai(i: int) -> bool;
pub spec fn bi(i: int) -> bool;
pub spec fn ci(i: int) -> bool;
pub open spec fn all_a() -> bool { forall|i: int| ai(i)}
pub open spec fn all_b() -> bool { forall|i: int| bi(i)}
pub open spec fn all_c() -> bool { forall|i: int| ci(i)}
pub proof fn test2(j: int) requires forall|i: int| ai(i), forall|i: int| (#[trigger] ai(i)) ==> bi(i),{ assert(ai(j) && bi(j) && ci(j));}
pub proof fn test_let(j: int) requires ai(j + 1),{ assert({ let k = j + 3; let r = k - 2; ai(r) && bi(r) });}
pub proof fn test_match(m: Option<int>) requires m.is_some(),{ assert(match m { Some(x) => x == 5, None => false, });}
pub proof fn test_match3(foo: Foo) { assert(match foo { Foo::Bar => false, Foo::Qux(z) => z == 0, Foo::Duck(w, y) => w == y, });}
pub proof fn test3(a: bool, b: bool) { assert(a <==> b);}
pub proof fn test_xor(a: bool, b: bool) { assert(a ^ b);}
pub proof fn test4(a: Option<u8>, b: Option<u8>) { assert(a == b);}
pub struct X { pub a: u32, pub b: bool, pub c: u64,}
pub proof fn test5(a: X, b: X) { assert(a == b);}
pub proof fn test6(a: Option<u64>, b: u64) { assert(a == Some(b));}
pub proof fn test7(a: Option<u64>, b: u64) { assert(Some(b) == a);}
pub proof fn test8(a: Option<u64>, b: u64) { assert(a == None);}
pub proof fn test9(a: Option<u64>, b: u64) { assert(None == a);}
pub proof fn test10(a: Option<u64>, b: u64) { assert(None == Some(b));}
pub proof fn test11(a: u64, b: u64) { assert(Some(a) == Some(b));}
#[verifier::external_body]pub struct OpaqueDT { u: u64,}
pub proof fn test12(a: OpaqueDT, b: OpaqueDT) { assert(a == b);}
pub enum Foo { Bar, Qux(u64), Duck(u64, u64),}
pub proof fn test13(a: Foo, b: u64) { assert(a == Foo::Qux(b));}
pub proof fn test14(a: Foo, b: u64, c: u64) { assert(Foo::Duck(b, c) == a);}
pub proof fn test15(a: Foo) { assert(a == Foo::Bar);}
pub proof fn test16(a: Foo, b: u64) { assert(Foo::Bar == a);}
pub proof fn test17(a: u64, b: u64, c: u64) { assert(Foo::Qux(a) == Foo::Duck(b, c));}
pub proof fn test18(b: u64, c: u64, e: u64, f: u64) { assert(Foo::Duck(b, c) == Foo::Duck(e, f));}
#[verifier::opaque]spec fn some_opaque() -> bool { false}
spec fn some_non_opaque() -> bool { false}
proof fn test_opaque1() { assert(some_opaque());}
proof fn test_opaque2() { reveal(some_opaque); assert(some_opaque());}
proof fn test_opaque3() { hide(some_non_opaque); assert(some_non_opaque());}
spec fn other(i: int) -> bool;
spec fn recursive_function(i: int, base: bool) -> bool decreases i,{ if i <= 0 { base } else { recursive_function(i - 1, base) }}
proof fn test_rec() { reveal_with_fuel(recursive_function, 3); assert(recursive_function(3, true)); // should fail with "reached fuel limit for recursion"}
proof fn test_rec2() { reveal_with_fuel(recursive_function, 4); assert(recursive_function(3, true)); // should pass}
proof fn test_rec3() { reveal_with_fuel(recursive_function, 4); assert(recursive_function(3, false));}
fn main() {}
} // verus!