summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v4
-rw-r--r--tests/coq/hashmap/Hashmap_FunsExternal.v8
-rw-r--r--tests/coq/hashmap/Hashmap_FunsExternal_Template.v9
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst4
-rw-r--r--tests/fstar/hashmap/Hashmap.FunsExternal.fsti8
-rw-r--r--tests/fstar/hashmap/Hashmap.Properties.fst8
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsScript.sml4
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig4
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml4
-rw-r--r--tests/lean/Hashmap/Funs.lean4
-rw-r--r--tests/lean/Hashmap/FunsExternal.lean8
-rw-r--r--tests/lean/Hashmap/FunsExternal_Template.lean9
-rw-r--r--tests/src/hashmap.rs8
13 files changed, 40 insertions, 42 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 89f90210..04df873a 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -508,10 +508,10 @@ Definition hashMap_remove
Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *)
Definition insert_on_disk
(n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) :=
- p <- hashmap_utils_deserialize st;
+ p <- utils_deserialize st;
let (st1, hm) := p in
hm1 <- hashMap_insert u64 n hm key value;
- hashmap_utils_serialize hm1 st1
+ utils_serialize hm1 st1
.
(** [hashmap::test1]:
diff --git a/tests/coq/hashmap/Hashmap_FunsExternal.v b/tests/coq/hashmap/Hashmap_FunsExternal.v
index bcf12c17..3bc6c98a 100644
--- a/tests/coq/hashmap/Hashmap_FunsExternal.v
+++ b/tests/coq/hashmap/Hashmap_FunsExternal.v
@@ -9,13 +9,13 @@ Require Export Hashmap_Types.
Import Hashmap_Types.
Module Hashmap_FunsExternal.
-(** [hashmap::hashmap_utils::deserialize]:
+(** [hashmap::utils::deserialize]:
Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *)
-Axiom hashmap_utils_deserialize : state -> result (state * (HashMap_t u64)).
+Axiom utils_deserialize : state -> result (state * (HashMap_t u64)).
-(** [hashmap::hashmap_utils::serialize]:
+(** [hashmap::utils::serialize]:
Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *)
-Axiom hashmap_utils_serialize : HashMap_t u64 -> state -> result (state * unit)
+Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit)
.
End Hashmap_FunsExternal.
diff --git a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v
index c35b8e14..c58b021d 100644
--- a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v
+++ b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v
@@ -11,13 +11,12 @@ Require Import Hashmap_Types.
Include Hashmap_Types.
Module Hashmap_FunsExternal_Template.
-(** [hashmap::hashmap_utils::deserialize]:
+(** [hashmap::utils::deserialize]:
Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *)
-Axiom hashmap_utils_deserialize : state -> result (state * (HashMap_t u64)).
+Axiom utils_deserialize : state -> result (state * (HashMap_t u64)).
-(** [hashmap::hashmap_utils::serialize]:
+(** [hashmap::utils::serialize]:
Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *)
-Axiom hashmap_utils_serialize : HashMap_t u64 -> state -> result (state * unit)
-.
+Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit).
End Hashmap_FunsExternal_Template.
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index a85be4ed..0e991720 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -380,9 +380,9 @@ let hashMap_remove
Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *)
let insert_on_disk
(key : usize) (value : u64) (st : state) : result (state & unit) =
- let* (st1, hm) = hashmap_utils_deserialize st in
+ let* (st1, hm) = utils_deserialize st in
let* hm1 = hashMap_insert u64 hm key value in
- hashmap_utils_serialize hm1 st1
+ utils_serialize hm1 st1
(** [hashmap::test1]:
Source: 'tests/src/hashmap.rs', lines 350:0-350:10 *)
diff --git a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
index 6e3964c7..f2f305e6 100644
--- a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
+++ b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
@@ -6,11 +6,11 @@ include Hashmap.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [hashmap::hashmap_utils::deserialize]:
+(** [hashmap::utils::deserialize]:
Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *)
-val hashmap_utils_deserialize : state -> result (state & (hashMap_t u64))
+val utils_deserialize : state -> result (state & (hashMap_t u64))
-(** [hashmap::hashmap_utils::serialize]:
+(** [hashmap::utils::serialize]:
Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *)
-val hashmap_utils_serialize : hashMap_t u64 -> state -> result (state & unit)
+val utils_serialize : hashMap_t u64 -> state -> result (state & unit)
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 0d6372c1..ed118c46 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -18,18 +18,18 @@ val state_v : state -> hashMap_t u64
/// [serialize] updates the hash map stored on disk
assume
val serialize_lem (hm : hashMap_t u64) (st : state) : Lemma (
- match hashmap_utils_serialize hm st with
+ match utils_serialize hm st with
| Fail _ -> True
| Ok (st', ()) -> state_v st' == hm)
- [SMTPat (hashmap_utils_serialize hm st)]
+ [SMTPat (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 st with
+ match utils_deserialize st with
| Fail _ -> True
| Ok (st', hm) -> hm == state_v st /\ st' == st)
- [SMTPat (hashmap_utils_deserialize st)]
+ [SMTPat (utils_deserialize st)]
(*** Lemmas *)
diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
index c1e30aa6..2a17d185 100644
--- a/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
@@ -628,9 +628,9 @@ val insert_on_disk_fwd_def = Define ‘
insert_on_disk_fwd
(key : usize) (value : u64) (st : state) : (state # unit) result =
do
- (st0, hm) <- hashmap_utils_deserialize_fwd st;
+ (st0, hm) <- utils_deserialize_fwd st;
hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
- (st1, _) <- hashmap_utils_serialize_fwd hm0 st0;
+ (st1, _) <- utils_serialize_fwd hm0 st0;
Return (st1, ())
od
’
diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
index d4e43d9a..c19673bb 100644
--- a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
@@ -583,9 +583,9 @@ sig
⊢ ∀key value st.
insert_on_disk_fwd key value st =
do
- (st0,hm) <- hashmap_utils_deserialize_fwd st;
+ (st0,hm) <- utils_deserialize_fwd st;
hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
- (st1,_) <- hashmap_utils_serialize_fwd hm0 st0;
+ (st1,_) <- utils_serialize_fwd hm0 st0;
Return (st1,())
od
diff --git a/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
index f7221d92..9c29c0e0 100644
--- a/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
@@ -6,10 +6,10 @@ open hashmapMain_TypesTheory
val _ = new_theory "hashmapMain_Opaque"
-(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd",
+(** [hashmap_main::utils::deserialize]: forward function *)val _ = new_constant ("utils_deserialize_fwd",
“:state -> (state # u64 hashmap_hash_map_t) result”)
-(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd",
+(** [hashmap_main::utils::serialize]: forward function *)val _ = new_constant ("utils_serialize_fwd",
“:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
val _ = export_theory ()
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index e76912cc..d7ac3b05 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -386,9 +386,9 @@ def HashMap.remove
def insert_on_disk
(key : Usize) (value : U64) (st : State) : Result (State × Unit) :=
do
- let (st1, hm) ← hashmap_utils.deserialize st
+ let (st1, hm) ← utils.deserialize st
let hm1 ← HashMap.insert U64 hm key value
- hashmap_utils.serialize hm1 st1
+ utils.serialize hm1 st1
/- [hashmap::test1]:
Source: 'tests/src/hashmap.rs', lines 350:0-350:10 -/
diff --git a/tests/lean/Hashmap/FunsExternal.lean b/tests/lean/Hashmap/FunsExternal.lean
index 7454696b..329e5d82 100644
--- a/tests/lean/Hashmap/FunsExternal.lean
+++ b/tests/lean/Hashmap/FunsExternal.lean
@@ -6,14 +6,14 @@ open hashmap
-- TODO: fill those bodies
-/- [hashmap::hashmap_utils::deserialize]:
+/- [hashmap::utils::deserialize]:
Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/
-def hashmap_utils.deserialize
+def utils.deserialize
: State → Result (State × (HashMap U64)) :=
fun _ => .fail .panic
-/- [hashmap::hashmap_utils::serialize]:
+/- [hashmap::utils::serialize]:
Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/
-def hashmap_utils.serialize
+def utils.serialize
: HashMap U64 → State → Result (State × Unit) :=
fun _ _ => .fail .panic
diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean
index 16b4b6af..2af57d10 100644
--- a/tests/lean/Hashmap/FunsExternal_Template.lean
+++ b/tests/lean/Hashmap/FunsExternal_Template.lean
@@ -6,12 +6,11 @@ import Hashmap.Types
open Primitives
open hashmap
-/- [hashmap::hashmap_utils::deserialize]:
+/- [hashmap::utils::deserialize]:
Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/
-axiom hashmap_utils.deserialize : State → Result (State × (HashMap U64))
+axiom utils.deserialize : State → Result (State × (HashMap U64))
-/- [hashmap::hashmap_utils::serialize]:
+/- [hashmap::utils::serialize]:
Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/
-axiom hashmap_utils.serialize
- : HashMap U64 → State → Result (State × Unit)
+axiom utils.serialize : HashMap U64 → State → Result (State × Unit)
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index ccb96e1e..19832a84 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,4 +1,4 @@
-//@ charon-args=--opaque=hashmap_utils
+//@ charon-args=--opaque=utils
//@ aeneas-args=-state -split-files
//@ [coq] aeneas-args=-use-fuel
//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
@@ -317,7 +317,7 @@ impl<T> HashMap<T> {
}
// This is a module so we can tell charon to leave it opaque
-mod hashmap_utils {
+mod utils {
use crate::*;
/// Serialize a hash map - we don't have traits, so we fix the type of the
@@ -334,11 +334,11 @@ mod hashmap_utils {
pub fn insert_on_disk(key: Key, value: u64) {
// Deserialize
- let mut hm = hashmap_utils::deserialize();
+ let mut hm = utils::deserialize();
// Update
hm.insert(key, value);
// Serialize
- hashmap_utils::serialize(hm);
+ utils::serialize(hm);
}
/// I currently can't retrieve functions marked with the attribute #[test],
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 05:54:31 +0000