From 00705bba68fed61d3b0bcde2c5fe0ecc83880870 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 18:37:07 +0100
Subject: Update the failing proofs

---
 tests/fstar/hashmap/Hashmap.Properties.fsti | 100 ++++++++++++++--------------
 1 file changed, 50 insertions(+), 50 deletions(-)

(limited to 'tests/fstar/hashmap/Hashmap.Properties.fsti')

diff --git a/tests/fstar/hashmap/Hashmap.Properties.fsti b/tests/fstar/hashmap/Hashmap.Properties.fsti
index 0a4f0134..26c0ec06 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fsti
+++ b/tests/fstar/hashmap/Hashmap.Properties.fsti
@@ -18,11 +18,11 @@ type key : eqtype = usize
 
 type hash : eqtype = usize
 
-val hash_map_t_inv (#t : Type0) (hm : hash_map_t t) : Type0
+val hashMap_t_inv (#t : Type0) (hm : hashMap_t t) : Type0
 
-val len_s (#t : Type0) (hm : hash_map_t t) : nat
+val len_s (#t : Type0) (hm : hashMap_t t) : nat
 
-val find_s (#t : Type0) (hm : hash_map_t t) (k : key) : option t
+val find_s (#t : Type0) (hm : hashMap_t t) (k : key) : option t
 
 (*** Overloading *)
 
@@ -32,16 +32,16 @@ val find_s (#t : Type0) (hm : hash_map_t t) (k : key) : option t
 /// limiting the hash collisions.
 /// This is expressed by the following property, which is maintained in the hash
 /// map invariant.
-val hash_map_not_overloaded_lem (#t : Type0) (hm : hash_map_t t) :
+val hashMap_not_overloaded_lem (#t : Type0) (hm : hashMap_t t) :
   Lemma
-  (requires (hash_map_t_inv hm))
+  (requires (hashMap_t_inv hm))
   (ensures (
     // The capacity is the number of slots
-    let capacity = length hm.hash_map_slots in
+    let capacity = length hm.slots in
     // The max load factor defines a threshold on the number of entries:
     // if there are more entries than a given fraction of the number of slots,
     // we resize the slots vector to limit the hash collisions
-    let (dividend, divisor) = hm.hash_map_max_load_factor in
+    let (dividend, divisor) = hm.max_load_factor in
     // technicality: this postcondition won't typecheck if we don't reveal
     // that divisor > 0 (because of the division)
     divisor > 0 /\
@@ -63,14 +63,14 @@ val hash_map_not_overloaded_lem (#t : Type0) (hm : hash_map_t t) :
 (**** [new'fwd] *)
 
 /// [new] doesn't fail and returns an empty hash map
-val hash_map_new_fwd_lem (t : Type0) :
+val hashMap_new_lem (t : Type0) :
   Lemma
   (ensures (
-    match hash_map_new_fwd t with
+    match hashMap_new t with
     | Fail _ -> False
     | Return hm ->
       // The hash map invariant is satisfied
-      hash_map_t_inv hm /\
+      hashMap_t_inv hm /\
       // The hash map has a length of 0
       len_s hm = 0 /\
       // It contains no bindings
@@ -79,16 +79,16 @@ val hash_map_new_fwd_lem (t : Type0) :
 (**** [clear] *)
 
 /// [clear] doesn't fail and turns the hash map into an empty map
-val hash_map_clear_fwd_back_lem
-  (#t : Type0) (self : hash_map_t t) :
+val hashMap_clear_lem
+  (#t : Type0) (self : hashMap_t t) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_clear_fwd_back t self with
+    match hashMap_clear t self with
     | Fail _ -> False
     | Return hm ->
       // The hash map invariant is satisfied
-      hash_map_t_inv hm /\
+      hashMap_t_inv hm /\
       // The hash map has a length of 0
       len_s hm = 0 /\
       // It contains no bindings
@@ -97,11 +97,11 @@ val hash_map_clear_fwd_back_lem
 (**** [len] *)
 
 /// [len] can't fail and returns the length (the number of elements) of the hash map
-val hash_map_len_fwd_lem (#t : Type0) (self : hash_map_t t) :
+val hashMap_len_lem (#t : Type0) (self : hashMap_t t) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_len_fwd t self with
+    match hashMap_len t self with
     | Fail _ -> False
     | Return l -> l = len_s self))
 
@@ -114,12 +114,12 @@ val hash_map_len_fwd_lem (#t : Type0) (self : hash_map_t t) :
 /// entirely encompassed by the effect of the backward function alone).
 /// 
 /// [insert'fwd_back] simply inserts a binding.
-val hash_map_insert_fwd_back_lem
-  (#t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
+val hashMap_insert_lem
+  (#t : Type0) (self : hashMap_t t) (key : usize) (value : t) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_insert_fwd_back t self key value with
+    match hashMap_insert t self key value with
     | Fail _ ->
       // We can fail only if:
       // - the key is not in the map and we thus need to add it
@@ -128,7 +128,7 @@ val hash_map_insert_fwd_back_lem
       len_s self = usize_max
     | Return hm' ->
       // The invariant is preserved
-      hash_map_t_inv hm' /\
+      hashMap_t_inv hm' /\
       // [key] maps to [value]
       find_s hm' key == Some value /\
       // The other bindings are preserved
@@ -145,24 +145,24 @@ val hash_map_insert_fwd_back_lem
 
 /// [contains_key'fwd] can't fail and returns `true` if and only if there is
 /// a binding for key [key]
-val hash_map_contains_key_fwd_lem
-  (#t : Type0) (self : hash_map_t t) (key : usize) :
+val hashMap_contains_key_lem
+  (#t : Type0) (self : hashMap_t t) (key : usize) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_contains_key_fwd t self key with
+    match hashMap_contains_key t self key with
     | Fail _ -> False
     | Return b -> b = Some? (find_s self key)))
 
 (**** [get'fwd] *)
 
 /// [get] returns (a shared borrow to) the binding for key [key]
-val hash_map_get_fwd_lem
-  (#t : Type0) (self : hash_map_t t) (key : usize) :
+val hashMap_get_lem
+  (#t : Type0) (self : hashMap_t t) (key : usize) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_get_fwd t self key, find_s self key with
+    match hashMap_get t self key, find_s self key with
     | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
@@ -175,12 +175,12 @@ val hash_map_get_fwd_lem
 /// in Rust, which gives the possibility of modifying this element in place. Then,
 /// upon ending the borrow, the effect of the modification is modelled in the
 /// translation through a call to the backward function.
-val hash_map_get_mut_fwd_lem
-  (#t : Type0) (self : hash_map_t t) (key : usize) :
+val hashMap_get_mut_lem
+  (#t : Type0) (self : hashMap_t t) (key : usize) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_get_mut_fwd t self key, find_s self key with
+    match hashMap_get_mut t self key, find_s self key with
     | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
@@ -192,11 +192,11 @@ val hash_map_get_mut_fwd_lem
 /// A call to [get_mut'back] must follow a call to [get_mut'fwd], which gives
 /// us that there must be a binding for key [key] in the map (otherwise we
 /// can't prove the absence of failure).
-val hash_map_get_mut_back_lem
-  (#t : Type0) (hm : hash_map_t t) (key : usize) (ret : t) :
+val hashMap_get_mut_back_lem
+  (#t : Type0) (hm : hashMap_t t) (key : usize) (ret : t) :
   Lemma
   (requires (
-    hash_map_t_inv hm /\
+    hashMap_t_inv hm /\
     // A call to the backward function must follow a call to the forward
     // function, whose success gives us that there is a binding for the key.
     // In the case of *forward* functions, "success" has to be understood as
@@ -207,14 +207,14 @@ val hash_map_get_mut_back_lem
     // "failure" is to be understood as the semantics getting stuck.
     // This is of course true unless we filtered the call to the forward function
     // because its effect is encompassed by the backward function, as with
-    // [hash_map_clear_fwd_back]).
+    // [hashMap_clear]).
     Some? (find_s hm key)))
   (ensures (
-    match hash_map_get_mut_back t hm key ret with
+    match hashMap_get_mut_back t hm key ret with
     | Fail _ -> False // Can't fail
     | Return hm' ->
      // The invariant is preserved
-     hash_map_t_inv hm' /\
+     hashMap_t_inv hm' /\
      // The length is preserved
      len_s hm' = len_s hm /\
      // [key] maps to the update value, [ret]
@@ -228,12 +228,12 @@ val hash_map_get_mut_back_lem
 /// (the rust function *moves* it out of the map). Note that the effect of the update
 /// on the map is modelles through the call to [remove'back] ([remove] takes a
 /// mutable borrow to the hash map as parameter).
-val hash_map_remove_fwd_lem
-  (#t : Type0) (self : hash_map_t t) (key : usize) :
+val hashMap_remove_lem
+  (#t : Type0) (self : hashMap_t t) (key : usize) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_remove_fwd t self key with
+    match hashMap_remove t self key with
     | Fail _ -> False
     | Return opt_x -> opt_x == find_s self key))
 
@@ -243,16 +243,16 @@ val hash_map_remove_fwd_lem
 /// The hash map given as parameter to [remove] is given through a mutable borrow:
 /// hence the backward function which gives back the updated map, without the
 /// binding.
-val hash_map_remove_back_lem
-  (#t : Type0) (self : hash_map_t t) (key : usize) :
+val hashMap_remove_back_lem
+  (#t : Type0) (self : hashMap_t t) (key : usize) :
   Lemma
-  (requires (hash_map_t_inv self))
+  (requires (hashMap_t_inv self))
   (ensures (
-    match hash_map_remove_back t self key with
+    match hashMap_remove_back t self key with
     | Fail _ -> False
     | Return hm' ->
       // The invariant is preserved
-      hash_map_t_inv self /\
+      hashMap_t_inv self /\
       // The binding for [key] is not there anymore
       find_s hm' key == None /\
       // The other bindings are preserved
-- 
cgit v1.2.3