Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576use verus_builtin::*;use verus_builtin_macros::*;
verus! {
fn main() {}
spec fn f<A>(a1: A, a2: A) -> bool { true}
spec fn id<A, B>(a: A, b: B, c: A) -> A { a}
fn id_exec<A, B>(a: A, b: B, c: A) -> (r: A) requires f(a, c), ensures f(r, a),{ a}
spec fn id_int(i: int) -> int { id(i, true, 10)}
spec fn id_u64(i: u64) -> u64 { id(i, true, 10)}
fn id_u64_exec(i: u64) -> (r: u64) ensures f(r, id_u64(i)),{ id_exec(i, true, 10)}
struct S<A> { n: A,}
spec fn s_property<B>(s: S<B>) -> int { 7}
spec fn id_s(s: S<int>) -> S<int> { id(s, true, s)}
proof fn s_prop1(x: S<int>, y: S<int>) { assert(s_property(x) == s_property(y));}
proof fn s_prop2<C>(x: S<C>, y: S<C>) { assert(s_property(x) == s_property(y));}
#[verifier::opaque]spec fn g<A>(a: A) -> A { a}
proof fn test_g1(u: u8) { reveal(g::<u8>); // REVIEW: should reveal quantify over all A? assert(g(u) == u);}
proof fn test_g2(u: u8) { assert(g(u) < 256 as int);}
} // verus!