Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134use vstd::prelude::*;
// TODO: add some of these explanations to the guide
verus! {
// If treated naively, recursive types can lead to nonterminating proofs:/*struct R { f: spec_fn(R) -> int }proof fn bad() ensures false{ let f1 = |r: R| -> int { (r.f)(r) + 1 }; let r = R { f: f1 }; // from r == R { f: f1 }: assert( r.f == f1 ); assert((r.f)(r) == f1(r)); // from the definition of f1: assert(f1(r) == (r.f)(r) + 1); // taken together: assert(f1(r) == f1(r) + 1);}*/// To prevent this, Verus prohibits recursion in "negative positions" in a recursive type.// Roughly, a negative position is anything on the left-hand side of a function type ->.// For example, the "R" in spec_fn(R) -> int is in a negative position.// Therefore, Verus rejects the definition "struct R { f: spec_fn(R) -> int }" with an error.// If generics are treated naively, they could encode recursion in negative positions.// For example, we could try to wrap the function type in a new type to hide the negative// use of R:/*struct FnWrapper<A, B> { f: spec_fn(A) -> B } // error: A not allowed in negative positionstruct R { f: FnWrapper<R, int> }*/// To prevent this, Verus requires that type parameters used in negative positions (like A)// be annotated with #[verifier::reject_recursive_types]:/*#[verifier::reject_recursive_types(A)]struct FnWrapper<A, B> { f: spec_fn(A) -> B } // okstruct R { f: FnWrapper<R, int> } // error: R not allowed in negative position*/// Based on this annotation on A, Verus knows that the recursive R in FnWrapper<R, int> should// be rejected, and it reports an error in the definition of R.// Recursive types can be used in decreases clauses of recursive specifications and recursive proofs:enum List<A> { Nil, Cons(A, Box<List<A>>),}
spec fn len<A>(list: &List<A>) -> nat decreases list // decreases can be used on values of type List<A> ,{ match list { List::Nil => 0, List::Cons(_, tl) => 1 + len(tl), }}
// To support this, Verus requires that struct and enum datatypes have a well-defined height (rank).// For this, Verus requires that struct and enum datatypes have a non-recursive// "ground" variant that can be used as a base case for defining the height.// For example, the Nil variant in List can be used to construct List values of height 0,// and then the Cons variant can be repeatedly applied to construct bigger and bigger values// with height > 0.// Attempting to declare a datatype with no ground variant will cause an error:/*enum UngroundedList<A> { // error: no ground variant; the only variant is Cons, which recursively uses UngroundedList Cons(A, Box<UngroundedList<A>>),}*/
// If generics are treated naively, they could encode datatypes with no ground variant:/*struct DataWrapper<A> { a: A }enum UngroundedList<A> { // error: no ground variant; the only variant is Cons, which still recursively uses UngroundedList Cons(A, Box<DataWrapper<UngroundedList<A>>>),}*/
// To prevent this, Verus rejects a recursive type definition's ground variant// from instantiating a type parameter A with the recursive type (UngroundedList)// unless the type parameter A is marked #[verifier::accept_recursive_types].// However, if DataWrapper marks A accept_recursive_types,// then DataWrapper must have a ground variant that is not built from A.// Because of this, Verus rejects the following:/*#[verifier::accept_recursive_types(A)]struct DataWrapper<A> { a: A } // error: no ground variant without A*/
// However, by adding a ground variant, we can provide a correct wrapper,// making both DataOption and GroundedList properly grounded:#[verifier::accept_recursive_types(A)]enum DataOption<A> { None, Some(A),} // okenum GroundedList<A> { Cons(A, Box<DataOption<GroundedList<A>>>), // ok}
// Overall, Verus parameters have one of three levels of acceptance of recursive types:// - #[verifier::reject_recursive_types]// - #[verifier::reject_recursive_types_in_ground_variants]// - #[verifier::accept_recursive_types]// reject_recursive_types is added to types that use the type parameter negatively,// and accept_recursive_types may (optionally) be added to types that have a ground variant// that doesn't use the type parameter.// Typical example of reject_recursive_types:#[verifier::reject_recursive_types(A)]struct Set<A> { f: spec_fn(A) -> bool,}
// Typical example of reject_recursive_types_in_ground_variants (which is the default):struct Pair<A, B> { first: A, second: B,}
// Typical example of accept_recursive_types:#[verifier::accept_recursive_types(A)]enum Option<A> { None, Some(A),}
fn main() {}
} // verus!