diff options
author | Nadrieril | 2024-05-28 11:18:35 +0200 |
---|---|---|
committer | Nadrieril | 2024-05-28 11:36:31 +0200 |
commit | c4d2af051c18c4c81b1e57a45210c37c89c8330f (patch) | |
tree | a72fae46702fc4c2eb32e1361a2538eb7a5f5545 /tests | |
parent | c81c96f20b1dbf428a9ed42e83b910e798e1a225 (diff) |
tests: Rename hashmap_utils -> utils
Diffstat (limited to '')
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 4 | ||||
-rw-r--r-- | tests/coq/hashmap/Hashmap_FunsExternal.v | 8 | ||||
-rw-r--r-- | tests/coq/hashmap/Hashmap_FunsExternal_Template.v | 9 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 4 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.FunsExternal.fsti | 8 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Properties.fst | 8 | ||||
-rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_FunsScript.sml | 4 | ||||
-rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig | 4 | ||||
-rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml | 4 | ||||
-rw-r--r-- | tests/lean/Hashmap/Funs.lean | 4 | ||||
-rw-r--r-- | tests/lean/Hashmap/FunsExternal.lean | 8 | ||||
-rw-r--r-- | tests/lean/Hashmap/FunsExternal_Template.lean | 9 | ||||
-rw-r--r-- | tests/src/hashmap.rs | 8 |
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], |