Make Set and Map finite, add ISet and IMap.

[jaylorch]

Set<A> and Map<A> now represent finite sets and maps, respectively. ISet<A> and IMap<A> are the new names for the old-style possibly-infinite sets and maps.

This new design is motivated because (1) it allows recursive types, such as having an enum T with a Set<T> field; and (2) finite sets are quite common in user code, and it's easy to go down a wild goose chase trying to get an ambient broadcast property to instantiate that turns out to be a missing .finite().

The simplest porting path for existing code is to use the infinite versions, which work like the previous single Set and Map. Replace Set with ISet, Map with IMap, set! with iset!, and map! with imap!.

To exploit the finite sets, use the Set and Map types. Where you might have specified a set domain with a predicate (boolean closure) before, now you might start with a finite constructor and transform it with map or filter.

let evens_lt_100 = Set::<int>::new(|x| 0 <= x < 100 && x%2==0); // old predicate constructor; now produces an `Option<Set<int>>` that you demonstrate is `Some` by proving it's finite.
let evens_lt_100 = Set::<int>::range(0, 100).filter(|x| x % 2 == 0); // new constructor starts with finite int range

let trees = Set::<int>::range(0, 5).map(|x| tree_constructor(x)); // Construct a set of trees, one per int [0,5)

Or, even better, use the recently added set_build! macro to produce a finite set. To produce a finite map, construct the finite domain as a Set and use it as the first parameter to the new Map::new.

This PR addresses issue #1512.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[Catoverflow]

And as Anvil is added to verita, there will be more breaking changes in the future and I don't want to burden Verus developers (thank you @jaylorch!) with proofs on our side. You directly @ me or @marshtompsxd in the breaking PR, we will always be there to help.

[jaylorch]

And as Anvil is added to verita, there will be more breaking changes in the future and I don't want to burden Verus developers (thank you @jaylorch!) with proofs on our side. You directly @ me or @marshtompsxd in the breaking PR, we will always be there to help.

Thanks!!!

[jaylorch]

I noticed that some helper predicates do not exists for finite DS (e.g. submap_of in Map). Do you have plan to add them in the future? I can also help on that.

There is a submap_of in the new (and old) map_lib.rs.

[Catoverflow]

There is a submap_of in the new (and old) map_lib.rs.

I somehow missed it. Thanks!

[Catoverflow]

I tried to fix broken proofs in Anvil and found this proof fails

use vstd::prelude::*;
verus! {
proof fn repro(m: Map<int, int>, k1: int, k2: int)
    requires
        k2 != k1,
{
    assert(m.insert(k1, 0)[k2] == m[k2]);
}
fn main() {}
}

$ verus repro.rs
note: recommendation not met
  --> repro.rs:18:12
   |
18 |     assert(m.insert(k1, 0)[k2] == m[k2]);
   |            ^^^^^^^^^^^^^^^^^^^
   |
  --> vstd/map.rs:87:12
   |
   = note: recommendation not met

error: assertion failed
  --> repro.rs:18:12
   |
18 |     assert(m.insert(k1, 0)[k2] == m[k2]);
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ assertion failed

note: recommendation not met
  --> repro.rs:18:35
   |
18 |     assert(m.insert(k1, 0)[k2] == m[k2]);
   |                                   ^^^^^
   |
  --> vstd/map.rs:87:12
   |
   = note: recommendation not met

verification results:: 1 verified, 1 errors
error: aborting due to 1 previous error

Previously this would pass verus, now without explicit m.dom().contains() the proof fails to use lemma_map_insert_different. I guess for finite map this is expected but it still causes some regressions in Anvil. Would it be better to document this? It took me some time to pinpoint the cause.

[jaylorch]

Interesting observation, thanks! I looked into it more, and found this:

It's always been the case that indexing into a map using a key that isn't in its domain produces a meaningless value. The way insert used to be defined for Map (and is still defined for IMap) ensures that those meaningless results don't change after an insert. But that doesn't work for finite maps, which are defined differently.

So it's not just a triggering issue. For finite maps, indexing into keys outside the domain gives arbitrary results, and those results might be changed by an insert.

In general, it's good practice to not index into maps outside their domain for any type of map. Even for IMap or the old Map, it's still a violation of the recommends clause to do so.

[jaylorch]

As for documenting it, that's a good idea. Where would it have helped to have documentation? On Map::insert, or in the recommends clause for Map::index? Or both?

[jaylorch]

The reason for this behavior is the different signatures of the broadcast lemmas lemma_map_insert_domain and lemma_imap_insert_domain. But I imagine no one is going to look at the documentation for those lemmas to figure out what's going wrong with their proofs. So I just added documentation to Map::insert instead.

[jaylorch]

The ultimate reason why the behavior differs is that the new Map relies on this axiom:

    broadcast axiom fn axiom_new(s: Set<K>, fv: spec_fn(K) -> V)
        ensures
            #![trigger Self::new(s, fv)]
            Self::new(s, fv).dom() == s,
            forall|k| s.contains(k) ==> #[trigger] Self::new(s, fv)[k] == fv(k),
    ;

I could weaken this to remove the s.contains(k) ==> part, for backwards compatibility. But my first inclination is to leave it as is, to make as few assumptions as possible in this trusted axiom.

[jaylorch]

Ah, never mind, the new axiom Map::axiom_new is based on the old axiom_mk_map_index, which did have that requirement. So I should leave that axiom alone.

The issue is just that Map::insert works differently than IMap::insert. So I think it's best to just leave it as is and document the difference.

[Catoverflow]

For finite maps, indexing into keys outside the domain gives arbitrary results

I agree enforcing domain check is better.

On Map::insert, or in the recommends clause for Map::index? Or both?

recommends would be a good place, however, I guess many developers are used to failed recommends in domain check like in this case and may not realize the difference. It may be better to hint for this when recommends fail and point to a explaining page on website.

[jaylorch]

@Chris-Hawblitzel and I just talked, and decided to preserve the property of Map::insert and Map::remove that values outside the domain retain their values when indexed. This requires changing a couple of lemmas to axioms.

[Catoverflow]

Great! A lot of fixing efforts are saved. Thank you @jaylorch. And I guess it may be helpful to this reproduction proof to tests in Verus to prevent such in the future?