From 2b40c5c3de1ee2caca2c0072f812fea04b5a0238 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 14:59:10 +0200
Subject: tests: Merge the hashmap test files

---
 tests/src/hashmap.rs       | 29 ++++++++++++++++++++++++++++-
 tests/src/hashmap_main.rs  | 22 ----------------------
 tests/src/hashmap_utils.rs | 13 -------------
 3 files changed, 28 insertions(+), 36 deletions(-)
 delete mode 100644 tests/src/hashmap_main.rs
 delete mode 100644 tests/src/hashmap_utils.rs

(limited to 'tests/src')

diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 4552e4f2..ccb96e1e 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,9 +1,11 @@
+//@ charon-args=--opaque=hashmap_utils
+//@ aeneas-args=-state -split-files
 //@ [coq] aeneas-args=-use-fuel
-//@ aeneas-args=-split-files
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 //@ [lean] aeneas-args=-no-gen-lib-entry
 // ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not
 // want to overwrite it.
+// Possible to add `--no-code-duplication` if we use the optimized MIR
 // TODO: reactivate -test-trans-units
 
 //! A hashmap implementation.
@@ -314,6 +316,31 @@ impl<T> HashMap<T> {
     }
 }
 
+// This is a module so we can tell charon to leave it opaque
+mod hashmap_utils {
+    use crate::*;
+
+    /// Serialize a hash map - we don't have traits, so we fix the type of the
+    /// values (this is not the interesting part anyway)
+    pub(crate) fn serialize(_hm: HashMap<u64>) {
+        unimplemented!();
+    }
+    /// Deserialize a hash map - we don't have traits, so we fix the type of the
+    /// values (this is not the interesting part anyway)
+    pub(crate) fn deserialize() -> HashMap<u64> {
+        unimplemented!();
+    }
+}
+
+pub fn insert_on_disk(key: Key, value: u64) {
+    // Deserialize
+    let mut hm = hashmap_utils::deserialize();
+    // Update
+    hm.insert(key, value);
+    // Serialize
+    hashmap_utils::serialize(hm);
+}
+
 /// I currently can't retrieve functions marked with the attribute #[test],
 /// while I want to extract the unit tests and use the normalize on them,
 /// so I have to define the test functions somewhere and call them from
diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs
deleted file mode 100644
index 0c827844..00000000
--- a/tests/src/hashmap_main.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-//@ charon-args=--opaque=hashmap_utils
-//@ aeneas-args=-state -split-files
-//@ [coq] aeneas-args=-use-fuel
-//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
-// Possible to add `--no-code-duplication` if we use the optimized MIR
-// TODO: reactivate -test-trans-units
-mod hashmap;
-mod hashmap_utils;
-
-use crate::hashmap::*;
-use crate::hashmap_utils::*;
-
-pub fn insert_on_disk(key: Key, value: u64) {
-    // Deserialize
-    let mut hm = deserialize();
-    // Update
-    hm.insert(key, value);
-    // Serialize
-    serialize(hm);
-}
-
-pub fn main() {}
diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs
deleted file mode 100644
index 33de49e1..00000000
--- a/tests/src/hashmap_utils.rs
+++ /dev/null
@@ -1,13 +0,0 @@
-//@ skip
-use crate::hashmap::*;
-
-/// Serialize a hash map - we don't have traits, so we fix the type of the
-/// values (this is not the interesting part anyway)
-pub(crate) fn serialize(_hm: HashMap<u64>) {
-    unimplemented!();
-}
-/// Deserialize a hash map - we don't have traits, so we fix the type of the
-/// values (this is not the interesting part anyway)
-pub(crate) fn deserialize() -> HashMap<u64> {
-    unimplemented!();
-}
-- 
cgit v1.3.1


From 9cc69020773cc77965a6faa6f0d46f179de3d8b8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 17:22:07 +0200
Subject: runner: Store options for crate tests in a separate file

---
 tests/src/betree/aeneas-test-options |  4 ++++
 tests/test_runner/run_test.ml        | 40 +++++++++---------------------------
 2 files changed, 14 insertions(+), 30 deletions(-)
 create mode 100644 tests/src/betree/aeneas-test-options

(limited to 'tests/src')

diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options
new file mode 100644
index 00000000..c71e01df
--- /dev/null
+++ b/tests/src/betree/aeneas-test-options
@@ -0,0 +1,4 @@
+charon-args=--polonius --opaque=betree_utils
+aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
+[coq] aeneas-args=-use-fuel
+[fstar] aeneas-args=-decreases-clauses -template-clauses
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index a7b83e88..c626b4d1 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -100,31 +100,6 @@ module Command = struct
     | Failure -> ()
 end
 
-let aeneas_options_for_test backend test_name =
-  if test_name = "betree" then
-    let options =
-      [
-        "-backward-no-state-update";
-        "-test-trans-units";
-        "-state";
-        "-split-files";
-      ]
-    in
-    let extra_options =
-      match backend with
-      | Backend.Coq -> [ "-use-fuel" ]
-      | Backend.FStar -> [ "-decreases-clauses"; "-template-clauses" ]
-      | _ -> []
-    in
-    List.append extra_options options
-  else []
-
-(* File-specific options *)
-let charon_options_for_test test_name =
-  match test_name with
-  | "betree" -> [ "--polonius"; "--opaque=betree_utils" ]
-  | _ -> []
-
 (* The data for a specific test input *)
 module Input = struct
   type kind = SingleFile | Crate
@@ -218,13 +193,10 @@ module Input = struct
       else failwith ("`" ^ path ^ "` is not a file or a directory.")
     in
     let actions = BackendMap.make (fun _ -> Normal) in
-    let charon_options = charon_options_for_test name in
     let subdirs =
       BackendMap.make (fun backend -> default_subdir backend name)
     in
-    let aeneas_options =
-      BackendMap.make (fun backend -> aeneas_options_for_test backend name)
-    in
+    let aeneas_options = BackendMap.make (fun _ -> []) in
     let check_output = BackendMap.make (fun _ -> true) in
     let input =
       {
@@ -232,12 +204,14 @@ module Input = struct
         name;
         kind;
         actions;
-        charon_options;
+        charon_options = [];
         subdirs;
         aeneas_options;
         check_output;
       }
     in
+    (* For crates, we store the special comments in a separate file. *)
+    let crate_config_file = Filename.concat path "aeneas-test-options" in
     match kind with
     | SingleFile ->
         let file_lines = Core.In_channel.read_lines path in
@@ -251,6 +225,11 @@ module Input = struct
         List.fold_left
           (fun input comment -> apply_special_comment comment input)
           input special_comments
+    | Crate when Sys.file_exists crate_config_file ->
+        let special_comments = Core.In_channel.read_lines crate_config_file in
+        List.fold_left
+          (fun input comment -> apply_special_comment comment input)
+          input special_comments
     | Crate -> input
 end
 
@@ -300,6 +279,7 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
       let cmd = { cmd with redirect_out = Some out } in
       Command.run_command_expecting_failure cmd;
       Unix.close out
+
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : runner_env) (case : Input.t) =
   match case.kind with
-- 
cgit v1.3.1


From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 17:33:56 +0200
Subject: Add some tests

---
 tests/coq/misc/Issue194RecursiveStructProjector.v  | 54 ++++++++++++++++++++++
 .../misc/Issue194RecursiveStructProjector.fst      | 24 ++++++++++
 tests/fstar/misc/Matches.fst                       | 12 +++++
 tests/lean/Issue194RecursiveStructProjector.lean   | 35 ++++++++++++++
 tests/lean/Matches.lean                            | 16 +++++++
 tests/src/infinite-loop.rs                         | 11 +++++
 tests/src/issue-194-recursive-struct-projector.rs  | 16 +++++++
 tests/src/matches.rs                               | 10 ++++
 8 files changed, 178 insertions(+)
 create mode 100644 tests/coq/misc/Issue194RecursiveStructProjector.v
 create mode 100644 tests/fstar/misc/Issue194RecursiveStructProjector.fst
 create mode 100644 tests/fstar/misc/Matches.fst
 create mode 100644 tests/lean/Issue194RecursiveStructProjector.lean
 create mode 100644 tests/lean/Matches.lean
 create mode 100644 tests/src/infinite-loop.rs
 create mode 100644 tests/src/issue-194-recursive-struct-projector.rs
 create mode 100644 tests/src/matches.rs

(limited to 'tests/src')

diff --git a/tests/coq/misc/Issue194RecursiveStructProjector.v b/tests/coq/misc/Issue194RecursiveStructProjector.v
new file mode 100644
index 00000000..d1a07449
--- /dev/null
+++ b/tests/coq/misc/Issue194RecursiveStructProjector.v
@@ -0,0 +1,54 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [issue_194_recursive_struct_projector] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module Issue194RecursiveStructProjector.
+
+(** [issue_194_recursive_struct_projector::AVLNode]
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 *)
+Inductive AVLNode_t (T : Type) :=
+| mkAVLNode_t :
+  T ->
+  option (AVLNode_t T) ->
+  option (AVLNode_t T) ->
+  AVLNode_t T
+.
+
+Arguments mkAVLNode_t { _ }.
+
+Definition aVLNode_value {T : Type} (x : AVLNode_t T) :=
+  match x with | mkAVLNode_t x1 _ _ => x1 end
+.
+
+Notation "x2 .(aVLNode_value)" := (aVLNode_value x2) (at level 9).
+
+Definition aVLNode_left {T : Type} (x : AVLNode_t T) :=
+  match x with | mkAVLNode_t _ x1 _ => x1 end
+.
+
+Notation "x2 .(aVLNode_left)" := (aVLNode_left x2) (at level 9).
+
+Definition aVLNode_right {T : Type} (x : AVLNode_t T) :=
+  match x with | mkAVLNode_t _ _ x1 => x1 end
+.
+
+Notation "x2 .(aVLNode_right)" := (aVLNode_right x2) (at level 9).
+
+(** [issue_194_recursive_struct_projector::get_val]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 *)
+Definition get_val (T : Type) (x : AVLNode_t T) : result T :=
+  Ok x.(aVLNode_value)
+.
+
+(** [issue_194_recursive_struct_projector::get_left]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 *)
+Definition get_left
+  (T : Type) (x : AVLNode_t T) : result (option (AVLNode_t T)) :=
+  Ok x.(aVLNode_left)
+.
+
+End Issue194RecursiveStructProjector.
diff --git a/tests/fstar/misc/Issue194RecursiveStructProjector.fst b/tests/fstar/misc/Issue194RecursiveStructProjector.fst
new file mode 100644
index 00000000..76368f04
--- /dev/null
+++ b/tests/fstar/misc/Issue194RecursiveStructProjector.fst
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [issue_194_recursive_struct_projector] *)
+module Issue194RecursiveStructProjector
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [issue_194_recursive_struct_projector::AVLNode]
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 *)
+type aVLNode_t (t : Type0) =
+{
+  value : t; left : option (aVLNode_t t); right : option (aVLNode_t t);
+}
+
+(** [issue_194_recursive_struct_projector::get_val]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 *)
+let get_val (t : Type0) (x : aVLNode_t t) : result t =
+  Ok x.value
+
+(** [issue_194_recursive_struct_projector::get_left]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 *)
+let get_left (t : Type0) (x : aVLNode_t t) : result (option (aVLNode_t t)) =
+  Ok x.left
+
diff --git a/tests/fstar/misc/Matches.fst b/tests/fstar/misc/Matches.fst
new file mode 100644
index 00000000..06a9b6df
--- /dev/null
+++ b/tests/fstar/misc/Matches.fst
@@ -0,0 +1,12 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [matches] *)
+module Matches
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [matches::match_u32]:
+    Source: 'tests/src/matches.rs', lines 4:0-4:27 *)
+let match_u32 (x : u32) : result u32 =
+  begin match x with | 0 -> Ok 0 | 1 -> Ok 1 | _ -> Ok 2 end
+
diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean
new file mode 100644
index 00000000..4eb23934
--- /dev/null
+++ b/tests/lean/Issue194RecursiveStructProjector.lean
@@ -0,0 +1,35 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [issue_194_recursive_struct_projector]
+import Base
+open Primitives
+
+namespace issue_194_recursive_struct_projector
+
+/- [issue_194_recursive_struct_projector::AVLNode]
+   Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 -/
+inductive AVLNode (T : Type) :=
+| mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T
+
+@[simp, reducible]
+def AVLNode.value {T : Type} (x : AVLNode T) :=
+  match x with | AVLNode.mk x1 _ _ => x1
+
+@[simp, reducible]
+def AVLNode.left {T : Type} (x : AVLNode T) :=
+  match x with | AVLNode.mk _ x1 _ => x1
+
+@[simp, reducible]
+def AVLNode.right {T : Type} (x : AVLNode T) :=
+  match x with | AVLNode.mk _ _ x1 => x1
+
+/- [issue_194_recursive_struct_projector::get_val]:
+   Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 -/
+def get_val (T : Type) (x : AVLNode T) : Result T :=
+  Result.ok x.value
+
+/- [issue_194_recursive_struct_projector::get_left]:
+   Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 -/
+def get_left (T : Type) (x : AVLNode T) : Result (Option (AVLNode T)) :=
+  Result.ok x.left
+
+end issue_194_recursive_struct_projector
diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
new file mode 100644
index 00000000..3e3a558b
--- /dev/null
+++ b/tests/lean/Matches.lean
@@ -0,0 +1,16 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [matches]
+import Base
+open Primitives
+
+namespace matches
+
+/- [matches::match_u32]:
+   Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
+def match_u32 (x : U32) : Result U32 :=
+  match x with
+  | 0#u32 => Result.ok 0#u32
+  | 1#u32 => Result.ok 1#u32
+  | _ => Result.ok 2#u32
+
+end matches
diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs
new file mode 100644
index 00000000..906fc1fa
--- /dev/null
+++ b/tests/src/infinite-loop.rs
@@ -0,0 +1,11 @@
+//@ [coq,fstar,lean] skip
+//@ [coq,fstar] aeneas-args=-use-fuel
+//@ [coq,fstar] subdir=misc
+// FIXME: make it work
+fn bar() {}
+
+fn foo() {
+    loop {
+        bar()
+    }
+}
diff --git a/tests/src/issue-194-recursive-struct-projector.rs b/tests/src/issue-194-recursive-struct-projector.rs
new file mode 100644
index 00000000..9ebdc2bc
--- /dev/null
+++ b/tests/src/issue-194-recursive-struct-projector.rs
@@ -0,0 +1,16 @@
+//@ [coq,fstar] subdir=misc
+struct AVLNode<T> {
+    value: T,
+    left: AVLTree<T>,
+    right: AVLTree<T>,
+}
+
+type AVLTree<T> = Option<Box<AVLNode<T>>>;
+
+fn get_val<T>(x: AVLNode<T>) -> T {
+    x.value
+}
+
+fn get_left<T>(x: AVLNode<T>) -> AVLTree<T> {
+    x.left
+}
diff --git a/tests/src/matches.rs b/tests/src/matches.rs
new file mode 100644
index 00000000..5710a604
--- /dev/null
+++ b/tests/src/matches.rs
@@ -0,0 +1,10 @@
+//@ [coq] skip
+//@ [coq,fstar] subdir=misc
+//^ note: coq gives "invalid notation for pattern"
+fn match_u32(x: u32) -> u32 {
+    match x {
+        0 => 0,
+        1 => 1,
+        _ => 2,
+    }
+}
-- 
cgit v1.3.1


From c4d2af051c18c4c81b1e57a45210c37c89c8330f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 11:18:35 +0200
Subject: tests: Rename hashmap_utils -> utils

---
 tests/coq/hashmap/Hashmap_Funs.v                     | 4 ++--
 tests/coq/hashmap/Hashmap_FunsExternal.v             | 8 ++++----
 tests/coq/hashmap/Hashmap_FunsExternal_Template.v    | 9 ++++-----
 tests/fstar/hashmap/Hashmap.Funs.fst                 | 4 ++--
 tests/fstar/hashmap/Hashmap.FunsExternal.fsti        | 8 ++++----
 tests/fstar/hashmap/Hashmap.Properties.fst           | 8 ++++----
 tests/hol4/hashmap_main/hashmapMain_FunsScript.sml   | 4 ++--
 tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig   | 4 ++--
 tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml | 4 ++--
 tests/lean/Hashmap/Funs.lean                         | 4 ++--
 tests/lean/Hashmap/FunsExternal.lean                 | 8 ++++----
 tests/lean/Hashmap/FunsExternal_Template.lean        | 9 ++++-----
 tests/src/hashmap.rs                                 | 8 ++++----
 13 files changed, 40 insertions(+), 42 deletions(-)

(limited to 'tests/src')

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],
-- 
cgit v1.3.1