Macro set_build 

set_build!() { /* proc-macro */ }

This macro takes an expresion of the form: set_build!{ elem_expr: optional_typ | x1: typ1 in ..., ..., xn: typn in ..., cond1, ..., condm } or just: set_build!{ x: typ in ..., cond1, ..., condm } where each xk: typk in ... has one of the following forms:

• xk: typk for finite types (implementing FiniteFull)
• xk: typk in expr, where expr has type Set
• xk: typk in lo..hi, where lo and hi have type typk, where typk implements FiniteRange
• xk: typk in lo..=hi, where lo and hi have type typk, where typk implements FiniteRange and each condk is a boolean expression. From this, the setbuild macro uses map_by, map_flatten_by, filter, etc. to build a set of elements specified by elem_expr.

(Note: to see the code generated by set_build, use set_build_debug, which is like set_build, but also prints the generated builder to stderr as a side effect.)

Important restriction: by default, the elem_expr must be a variable, tuple, or datatype such that all of the variables x1, …, xn can be easily found with nothing more that tuple/datatype field accesses. In exchange for this restriction, set_build guarantees not to introduce any extra existential quantifiers into to constructed set. This makes it easy for proofs to use sets constructed with set_build, when compared to other forms of Set construction (like Set::map or Set::flatten) that do introduce existential quantifiers. To override this default and remove this restriction, you can mark one or more variables as exists x: typ rather than just x: typ, and set_build will use map/flatten for these variables. This will, however, make proofs about the constructed set more difficult.

Example: finite types

proof fn test() {
    use vstd::contrib::set_build;

    let s: Set<u8> = set_build!{ x: u8 };
    assert(s.finite());
    assert(forall|u: u8| s.contains(u));
}

This generates the set Set::<u8>::from_finite_type(|x: u8| true).

Example: filtering

let s: Set<u8> = set_build!{ x: u8, x < 100 };
assert(forall|u: u8| s.contains(u) <==> u < 100);

This generates the set Set::<u8>::from_finite_type(|x: u8| true).filter(|x: u8| (x < 100)).

Example: ranges

let s: Set<u8> = set_build!{ x: u8 in 10..20 };
assert(forall|u: u8| s.contains(u) <==> 10 <= u < 20);

This generates the set Set::<u8>::range(10, 20).

Example: tuples, mapping, and “exists”

let s1: Set<(u8, u8)> = set_build!{ (x, x): (u8, u8) | exists x: u8, x < 100 };
let s2: Set<(u8, u8)> = set_build!{ (x, x): (u8, u8) | x: u8, x < 100 };

Here, s1 generates a set based on filter and map:

Set::<u8>::from_finite_type(|x: u8| true)
    .filter(|x: u8| (x < 100))
    .map(|x: u8| ((x, x)))

while s2 generates the same set, but uses map_by rather than map:

Set::<u8>::from_finite_type(|x: u8| true)
    .filter(|x: u8| (x < 100))
    .map_by(|x: u8| ((x, x)), |__VERUS_x: (u8, u8)| (__VERUS_x.0))

Although s1 looks simpler, it is harder to work with in proofs. For example, an obvious assertion about s1 fails, while succeeding for s2:

assert(forall|p: (u8, u8)| s1.contains(p) <==> p.0 == p.1 && p.0 < 100); // FAILS
assert(forall|p: (u8, u8)| s2.contains(p) <==> p.0 == p.1 && p.0 < 100);

Nevertheless, s1 and s2 are equal to each other. In fact one way to prove the assertion above about s1 is to first use =~= to establish that s1 and s2 are equal:

assert(s1 =~= s2);
assert(forall|p: (u8, u8)| s1.contains(p) <==> p.0 == p.1 && p.0 < 100);

Example: datatypes

struct Address {
    page: int,
    offset: int,
}

proof fn test() {
    use vstd::contrib::set_build;

    let s: Set<Address> = set_build!{
        Address { page, offset }: Address |
        page: int in 10..20,
        offset: int in 0..4096,
    };
    assert(s.finite());
    assert(s.contains(Address { page: 15, offset: 1024 }));
    assert(!s.contains(Address { page: 5, offset: 1024 }));
}

This generates:

Set::<int>::range(10, 20)
    .map_flatten_by(
        |__VERUS_x: int| {
            let page = __VERUS_x;
            Set::<int>::range(0, 4096)
                .map_by(
                    |offset: int| (Address { page, offset }),
                    |__VERUS_x: Address| (__VERUS_x.offset),
                )
        },
        |__VERUS_x: Address| __VERUS_x.page,
    )

Example: complex expressions

let s = set_build!{ (x, y, y - x): (int, int, int) | x: int in 10..20, y: int in x..20, x + y != 25 };
assert(s.contains((12, 14, 2)));
assert(!s.contains((14, 12, 2))); // because y = 12 is not in 14..20
assert(s.contains((10, 13, 3)));
assert(s.contains((10, 14, 4)));
assert(!s.contains((10, 15, 5))); // because of x + y != 25
assert(s.contains((10, 16, 6)));

From this, set_build generates:

Set::<int>::range(10, 20)
    .map_flatten_by(
        |__VERUS_x: int| {
            let x = __VERUS_x;
            Set::<int>::range(x, 20)
                .filter(|y: int| (x + y != 25))
                .map_by(
                    |y: int| ((x, y, y - x)),
                    |__VERUS_x: (int, int, int)| (__VERUS_x.1),
                )
        },
        |__VERUS_x: (int, int, int)| __VERUS_x.0,
    )