prove map axioms

verus-lang · Jul 20, 2023 · a6c72a8 · a6c72a8
1 parent 90f7499
commit a6c72a8
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 7 deletions.
diff --git a/source/pervasive/map.rs b/source/pervasive/map.rs
@@ -516,23 +516,31 @@ pub proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
 {
 }
 
-// TODO: might not have brought this over correctly
 // Ported from Dafny prelude
-#[verifier(external_body)]
+//#[verifier(external_body)]
 //#[verifier(broadcast_forall)]
 pub proof fn axiom_map_new_domain<K,V>(fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V)
     ensures
         #[trigger] Map::<K,V>::new(fk,fv).dom() == Set::<K>::new(|k: K| fk(k))
-{}
+{
+    assert(Set::new(fk) =~= Set::<K>::new(|k: K| fk(k)));
+}
 
-// TODO: might not have brought this over correctly
 // Ported from Dafny prelude
-#[verifier(external_body)]
+//#[verifier(external_body)]
 //#[verifier(broadcast_forall)]
 pub proof fn axiom_map_new_values<K,V>(fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V)
     ensures
-        #[trigger] Map::<K,V>::new(fk,fv).values() == Set::<V>::new(|v: V| exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v),
-{}
+        #[trigger] Map::<K,V>::new(fk,fv).values() == Set::<V>::new(|v: V| (exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v)),
+{
+    let keys = Set::<K>::new(fk);
+    let values = Map::<K,V>::new(fk,fv).values();
+    let map = Map::<K,V>::new(fk,fv);
+
+    assert(map.dom() =~= keys);
+    assert(forall |k: K| #[trigger] fk(k) ==> keys.contains(k));
+    assert(values =~= Set::<V>::new(|v: V| (exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v)));
+}
 
 #[verifier(external_body)]
 #[verifier(broadcast_forall)]

diff --git a/source/pervasive/seq.rs b/source/pervasive/seq.rs
@@ -664,6 +664,9 @@ macro_rules! seq {
     };
 }
 
+//TODO: change all names from axiom to lemma
+// change seq_magic to lemma_seq_properties or something
+//TODO: move as much as you can to seq_lib
 // auto style axiom bundle
 pub proof fn seq_magic<A>() 
     ensures

diff --git a/source/pervasive/set.rs b/source/pervasive/set.rs
@@ -1,3 +1,7 @@
+// TODO: make a table of every Dafny lemma/axiom and the verus equivalent
+// include notes of any skipped lemmas
+// include this in PR description
+
 use core::marker;
 
 #[allow(unused_imports)]
@@ -649,6 +653,8 @@ macro_rules! set {
     };
 }
 
+//TODO: change all names from axiom to lemma (and magic to properties????)
+//TODO: move as much as you can to set_lib
 // auto style axiom bundle
 pub proof fn set_magic<A>()
     ensures