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
---
.../fstar/hashmap_on_disk/HashmapMain.Properties.fst | 20 ++++++++++----------
tests/fstar/hashmap_on_disk/Primitives.fst | 18 +++++++++++++++++-
2 files changed, 27 insertions(+), 11 deletions(-)
(limited to 'tests/fstar/hashmap_on_disk')
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
index 106fe05a..358df29e 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
@@ -13,36 +13,36 @@ open HashmapMain.Funs
/// [state_v] gives us the hash map currently stored on disk
assume
-val state_v : state -> hashmap_hash_map_t u64
+val state_v : state -> hashmap_HashMap_t u64
/// [serialize] updates the hash map stored on disk
assume
-val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma (
- match hashmap_utils_serialize_fwd hm st with
+val serialize_lem (hm : hashmap_HashMap_t u64) (st : state) : Lemma (
+ match hashmap_utils_serialize hm st with
| Fail _ -> True
| Return (st', ()) -> state_v st' == hm)
- [SMTPat (hashmap_utils_serialize_fwd hm st)]
+ [SMTPat (hashmap_utils_serialize hm st)]
/// [deserialize] gives us the hash map stored on disk, without updating it
assume
val deserialize_lem (st : state) : Lemma (
- match hashmap_utils_deserialize_fwd st with
+ match hashmap_utils_deserialize st with
| Fail _ -> True
| Return (st', hm) -> hm == state_v st /\ st' == st)
- [SMTPat (hashmap_utils_deserialize_fwd st)]
+ [SMTPat (hashmap_utils_deserialize st)]
(*** Lemmas *)
/// The obvious lemma about [insert_on_disk]: the updated hash map stored on disk
/// is exactly the hash map produced from inserting the binding ([key], [value])
/// in the hash map previously stored on disk.
-val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma (
- match insert_on_disk_fwd key value st with
+val insert_on_disk_lem (key : usize) (value : u64) (st : state) : Lemma (
+ match insert_on_disk key value st with
| Fail _ -> True
| Return (st', ()) ->
let hm = state_v st in
- match hashmap_hash_map_insert_fwd_back u64 hm key value with
+ match hashmap_HashMap_insert u64 hm key value with
| Fail _ -> False
| Return hm' -> hm' == state_v st')
-let insert_on_disk_fwd_lem key value st = ()
+let insert_on_disk_lem key value st = ()
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 71d75c11..3297803c 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
@@ -427,7 +427,7 @@ let alloc_vec_Vec_new (a : Type0) : alloc_vec_Vec a = assert_norm(length #a []
let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
// Helper
-let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result a =
+let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
if i < length v then Return (index v i) else Fail Failure
// Helper
let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
@@ -704,6 +704,22 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
(*** Theorems *)
+let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+ Lemma (
+ alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i ==
+ alloc_vec_Vec_index_usize v i)
+ [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)]
+ =
+ admit()
+
+let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+ Lemma (
+ alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i ==
+ alloc_vec_Vec_index_usize v i)
+ [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)]
+ =
+ admit()
+
let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
Lemma (
alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x ==
--
cgit v1.2.3