Add model for vstd Set and prove its axioms

Author: matthias-brun

source/rust_verify_test/tests/sets.rs

@@ -111,7 +111,7 @@ test_verify_one_file! {
 
         proof fn test() {
             let s: Set<nat> = set![9];
-            reveal_with_fuel(Set::fold, 10);
+            broadcast use fold::lemma_fold_insert, fold::lemma_fold_empty;
             assert(s.finite());
             assert(s.len() > 0);
             assert(s.fold(0, |p: nat, a: nat| p + a) == 9);

source/vstd/map.rs

@@ -41,13 +41,13 @@ impl<K, V> Map<K, V> {
 
     /// Gives a `Map<K, V>` whose domain contains every key, and maps each key
     /// to the value given by `fv`.
-    pub open spec fn total(fv: impl Fn(K) -> V) -> Map<K, V> {
+    pub open spec fn total(fv: spec_fn(K) -> V) -> Map<K, V> {
         Set::full().mk_map(fv)
     }
 
     /// Gives a `Map<K, V>` whose domain is given by the boolean predicate on keys `fk`,
     /// and maps each key to the value given by `fv`.
-    pub open spec fn new(fk: impl Fn(K) -> bool, fv: impl Fn(K) -> V) -> Map<K, V> {
+    pub open spec fn new(fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V) -> Map<K, V> {
         Set::new(fk).mk_map(fv)
     }