diff options
| author | Son Ho | 2022-03-04 14:50:09 +0100 |
|---|---|---|
| committer | Son Ho | 2022-03-04 14:50:09 +0100 |
| commit | 26e057de4a77b12c904b5cf33b2db955da6eb17f (patch) | |
| tree | 10ff3a21031078d2c6d1d1f0daf56b3375978f48 | |
| parent | e0c8fb779e433c966ed7a12ea8aab8507bb23d36 (diff) | |
Make minor modifications
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Properties.fst | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Properties.fst b/tests/hashmap_on_disk/HashmapMain.Properties.fst index 8bf395ed..8a47cdf4 100644 --- a/tests/hashmap_on_disk/HashmapMain.Properties.fst +++ b/tests/hashmap_on_disk/HashmapMain.Properties.fst @@ -33,9 +33,10 @@ val deserialize_lem (st : state) : Lemma ( (*** Lemmas - auxiliary *) -/// The below proofs are trivial: we just prove that the hashmap insert function -/// doesn't update the state... As F* is made for *intrinsic* proofs, we have -/// to copy-paste the definitions, hence the huge verbosity... +/// The below proofs are trivial (and were done super quickly): we just prove that +/// the hashmap insert function doesn't update the state... As F* is made for +/// *intrinsic* proofs, we have to copy-paste the definitions and to insert the proper +/// lemma calls wherever needed, hence the verbosity... /// We will probably do some analysis in the future to use the proper monad when /// generating the definitions (no monad if functions can't fail, error monad if @@ -269,9 +270,8 @@ let hashmap_hash_map_insert_back_lem (*** 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] +/// 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 |