From 40e7df701d246faa453003374206014606ca6b6d Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Thu, 2 Feb 2023 23:36:14 -0800
Subject: WIP

---
 backends/lean/primitives.lean                      |  76 +++++++++-----
 compiler/Extract.ml                                |  10 +-
 compiler/ExtractBase.ml                            |   4 +-
 compiler/Translate.ml                              |  21 +++-
 tests/lean/hashmap_on_disk/Base/Primitives.lean    |  76 +++++++++-----
 .../HashmapMain/Clauses/Template.lean              | 113 +++++++++++++++++++++
 tests/lean/hashmap_on_disk/HashmapMain/Funs.lean   |   8 +-
 tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean |  18 ++--
 tests/lean/hashmap_on_disk/HashmapMain/Types.lean  |   4 +-
 tests/lean/hashmap_on_disk/lake-manifest.json      |  27 +++++
 10 files changed, 286 insertions(+), 71 deletions(-)
 create mode 100644 tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean
 create mode 100644 tests/lean/hashmap_on_disk/lake-manifest.json

diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean
index 0a51aacd..79958d94 100644
--- a/backends/lean/primitives.lean
+++ b/backends/lean/primitives.lean
@@ -1,4 +1,5 @@
 import Lean
+import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
 
@@ -75,7 +76,7 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
 -- Silly example of the kind of reasoning that this notation enables
 #eval do
   let h: y <-- .ret (0: Nat)
-  let _: y = 0 := by cases h; simp
+  let _: y = 0 := by cases h; decide
   let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩
   .ret r
 
@@ -111,6 +112,23 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
 -- library_search." Try to settle this with a Lean expert on what is the most
 -- productive way to go about this?
 
+-- One needs to perform a little bit of reasoning in order to successfully
+-- inject constants into USize, so we provide a general-purpose macro
+
+syntax "intlit" : tactic
+
+macro_rules
+  | `(tactic| intlit) => `(tactic|
+    match USize.size, usize_size_eq with
+    | _, Or.inl rfl => decide
+    | _, Or.inr rfl => decide)
+
+-- This is how the macro is expected to be used
+#eval USize.ofNatCore 0 (by intlit)
+
+-- Also works for other integer types (at the expense of a needless disjunction)
+#eval UInt32.ofNatCore 0 (by intlit)
+
 -- Further thoughts: look at what has been done here:
 -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean
 -- and
@@ -133,7 +151,12 @@ def USize.checked_sub (n: USize) (m: USize): result USize :=
     fail integerOverflow
 
 def USize.checked_add (n: USize) (m: USize): result USize :=
-  if h: n.val + m.val < USize.size then
+  if h: n.val.val + m.val.val <= 4294967295 then
+    .ret ⟨ n.val.val + m.val.val, by
+      have h': 4294967295 < USize.size := by intlit
+      apply Nat.lt_of_le_of_lt h h'
+    ⟩
+  else if h: n.val + m.val < USize.size then
     .ret ⟨ n.val + m.val, h ⟩
   else
     .fail integerOverflow
@@ -149,7 +172,12 @@ def USize.checked_rem (n: USize) (m: USize): result USize :=
     .fail integerOverflow
 
 def USize.checked_mul (n: USize) (m: USize): result USize :=
-  if h: n.val * m.val < USize.size then
+    if h: n.val.val * m.val.val <= 4294967295 then
+    .ret ⟨ n.val.val * m.val.val, by
+      have h': 4294967295 < USize.size := by intlit
+      apply Nat.lt_of_le_of_lt h h'
+    ⟩
+  else if h: n.val * m.val < USize.size then
     .ret ⟨ n.val * m.val, h ⟩
   else
     .fail integerOverflow
@@ -187,22 +215,6 @@ def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineIntege
   else
     .fail integerOverflow
 
--- One needs to perform a little bit of reasoning in order to successfully
--- inject constants into USize, so we provide a general-purpose macro
-
-syntax "intlit" : tactic
-
-macro_rules
-  | `(tactic| intlit) => `(tactic|
-    match USize.size, usize_size_eq with
-    | _, Or.inl rfl => decide
-    | _, Or.inr rfl => decide)
-
--- This is how the macro is expected to be used
-#eval USize.ofNatCore 0 (by intlit)
-
--- Also works for other integer types (at the expense of a needless disjunction)
-#eval UInt32.ofNatCore 0 (by intlit)
 
 -- Test behavior...
 #eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0
@@ -267,7 +279,14 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec 
 
 def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α)
   :=
-  if h : List.length v.val + 1 < USize.size then
+  if h : List.length v.val + 1 <= 4294967295 then
+    return ⟨ List.concat v.val x,
+      by
+        rw [List.length_concat]
+        have h': 4294967295 < USize.size := by intlit
+        apply Nat.lt_of_le_of_lt h h'
+    ⟩
+  else if h: List.length v.val + 1 < USize.size then
     return ⟨List.concat v.val x,
       by
         rw [List.length_concat]
@@ -340,10 +359,15 @@ syntax (name := assert) "#assert" term: command
 
 @[command_elab assert]
 def assertImpl : CommandElab := fun (_stx: Syntax) => do
-  logInfo "Hello World"
-
-def ignore (a: Prop) (_x: a) := ()
-
-#eval ignore (2 == 2) (by simp)
-
+  logInfo "Reducing and asserting: "
+  logInfo _stx[1]
+  runTermElabM (fun _ => do
+    let e ← Term.elabTerm _stx[1] none
+    logInfo (Expr.dbgToString e)
+    -- How to evaluate the term and compare the result to true?
+    pure ())
+  -- logInfo (Expr.dbgToString (``true))
+  -- throwError "TODO: assert"
+
+#eval 2 == 2
 #assert (2 == 2)
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index d707dc81..e1b2b23f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -476,8 +476,10 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   in
   let fun_name (fname : fun_name) (num_loops : int) (loop_id : LoopId.id option)
       (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int)
+      (missing_body: bool)
       : string =
     let fname = fun_name_to_snake_case fname in
+    let fname = if !backend = Lean && missing_body then "opaque_defs." ^ fname else fname in
     (* Compute the suffix *)
     let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
     (* Concatenate *)
@@ -1371,7 +1373,6 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
       ctx
   in
   let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in
-  (* Register the function names *)
   let register_fun ctx f = ctx_add_fun_decl (keep_fwd, def) f ctx in
   let register_funs ctx fl = List.fold_left register_fun ctx fl in
   (* Register the forward functions' names *)
@@ -2227,7 +2228,12 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   let use_forall = is_opaque_coq && def.signature.type_params <> [] in
   (* *)
   let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
-  F.pp_print_string fmt (qualif ^ " " ^ def_name);
+  (* For Lean: we generate a record of assumed functions *)
+  if not (!backend = Lean && (kind = Assumed || kind = Declared)) then begin
+    F.pp_print_string fmt qualif;
+    F.pp_print_space fmt ()
+  end;
+  F.pp_print_string fmt def_name;
   F.pp_print_space fmt ();
   if use_forall then (
     F.pp_print_string fmt ":";
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 77170b5b..98a29daf 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -168,6 +168,7 @@ type formatter = {
     int ->
     region_group_info option ->
     bool * int ->
+    bool ->
     string;
       (** Compute the name of a regular (non-assumed) function.
 
@@ -187,6 +188,7 @@ type formatter = {
               The number of extracted backward functions if not necessarily
               equal to the number of region groups, because we may have
               filtered some of them.
+          - whether there is a body or not (indicates assumed function)
           TODO: use the fun id for the assumed functions.
        *)
   decreases_clause_name :
@@ -774,7 +776,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   in
   let name =
     ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
-      (keep_fwd, num_backs)
+      (keep_fwd, num_backs) (def.body = None)
   in
   ctx_add
     (FunId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0a1c8f9a..df7a750d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -661,13 +661,24 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
    *)
   if config.extract_state_type && config.extract_fun_decls then
     export_state_type ();
+  if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean then begin
+    Format.pp_print_break fmt 0 0;
+    Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr;
+    Format.pp_print_string fmt "structure OpaqueDefs where";
+    Format.pp_print_break fmt 0 0
+  end;
   List.iter export_decl_group ctx.crate.declarations;
+  if config.extract_opaque && !Config.backend = Lean then begin
+    Format.pp_close_box fmt ()
+  end;
   if config.extract_state_type && not config.extract_fun_decls then
     export_state_type ()
 
 let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
     (rust_module_name : string) (module_name : string) (custom_msg : string)
-    (custom_imports : string list) (custom_includes : string list) : unit =
+    ?(custom_variables: string list = [])
+    (custom_imports : string list) (custom_includes : string list)
+    : unit =
   (* Open the file and create the formatter *)
   let out = open_out filename in
   let fmt = Format.formatter_of_out_channel out in
@@ -720,7 +731,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
       (* Add the custom imports *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
       (* Add the custom includes *)
-      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes
+      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes;
+      if custom_variables <> [] then begin
+        Printf.fprintf out "\n";
+        List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables
+      end
   );
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
@@ -1016,8 +1031,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
         [ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"]
       else []
     in
+    let custom_variables = if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ] else [] in
     extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
       ": function definitions" []
+      ~custom_variables
       ([ types_module ] @ opaque_funs_module @ clauses_module))
   else
     let gen_config =
diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean
index 0a51aacd..79958d94 100644
--- a/tests/lean/hashmap_on_disk/Base/Primitives.lean
+++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean
@@ -1,4 +1,5 @@
 import Lean
+import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
 
@@ -75,7 +76,7 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
 -- Silly example of the kind of reasoning that this notation enables
 #eval do
   let h: y <-- .ret (0: Nat)
-  let _: y = 0 := by cases h; simp
+  let _: y = 0 := by cases h; decide
   let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩
   .ret r
 
@@ -111,6 +112,23 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
 -- library_search." Try to settle this with a Lean expert on what is the most
 -- productive way to go about this?
 
+-- One needs to perform a little bit of reasoning in order to successfully
+-- inject constants into USize, so we provide a general-purpose macro
+
+syntax "intlit" : tactic
+
+macro_rules
+  | `(tactic| intlit) => `(tactic|
+    match USize.size, usize_size_eq with
+    | _, Or.inl rfl => decide
+    | _, Or.inr rfl => decide)
+
+-- This is how the macro is expected to be used
+#eval USize.ofNatCore 0 (by intlit)
+
+-- Also works for other integer types (at the expense of a needless disjunction)
+#eval UInt32.ofNatCore 0 (by intlit)
+
 -- Further thoughts: look at what has been done here:
 -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean
 -- and
@@ -133,7 +151,12 @@ def USize.checked_sub (n: USize) (m: USize): result USize :=
     fail integerOverflow
 
 def USize.checked_add (n: USize) (m: USize): result USize :=
-  if h: n.val + m.val < USize.size then
+  if h: n.val.val + m.val.val <= 4294967295 then
+    .ret ⟨ n.val.val + m.val.val, by
+      have h': 4294967295 < USize.size := by intlit
+      apply Nat.lt_of_le_of_lt h h'
+    ⟩
+  else if h: n.val + m.val < USize.size then
     .ret ⟨ n.val + m.val, h ⟩
   else
     .fail integerOverflow
@@ -149,7 +172,12 @@ def USize.checked_rem (n: USize) (m: USize): result USize :=
     .fail integerOverflow
 
 def USize.checked_mul (n: USize) (m: USize): result USize :=
-  if h: n.val * m.val < USize.size then
+    if h: n.val.val * m.val.val <= 4294967295 then
+    .ret ⟨ n.val.val * m.val.val, by
+      have h': 4294967295 < USize.size := by intlit
+      apply Nat.lt_of_le_of_lt h h'
+    ⟩
+  else if h: n.val * m.val < USize.size then
     .ret ⟨ n.val * m.val, h ⟩
   else
     .fail integerOverflow
@@ -187,22 +215,6 @@ def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineIntege
   else
     .fail integerOverflow
 
--- One needs to perform a little bit of reasoning in order to successfully
--- inject constants into USize, so we provide a general-purpose macro
-
-syntax "intlit" : tactic
-
-macro_rules
-  | `(tactic| intlit) => `(tactic|
-    match USize.size, usize_size_eq with
-    | _, Or.inl rfl => decide
-    | _, Or.inr rfl => decide)
-
--- This is how the macro is expected to be used
-#eval USize.ofNatCore 0 (by intlit)
-
--- Also works for other integer types (at the expense of a needless disjunction)
-#eval UInt32.ofNatCore 0 (by intlit)
 
 -- Test behavior...
 #eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0
@@ -267,7 +279,14 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec 
 
 def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α)
   :=
-  if h : List.length v.val + 1 < USize.size then
+  if h : List.length v.val + 1 <= 4294967295 then
+    return ⟨ List.concat v.val x,
+      by
+        rw [List.length_concat]
+        have h': 4294967295 < USize.size := by intlit
+        apply Nat.lt_of_le_of_lt h h'
+    ⟩
+  else if h: List.length v.val + 1 < USize.size then
     return ⟨List.concat v.val x,
       by
         rw [List.length_concat]
@@ -340,10 +359,15 @@ syntax (name := assert) "#assert" term: command
 
 @[command_elab assert]
 def assertImpl : CommandElab := fun (_stx: Syntax) => do
-  logInfo "Hello World"
-
-def ignore (a: Prop) (_x: a) := ()
-
-#eval ignore (2 == 2) (by simp)
-
+  logInfo "Reducing and asserting: "
+  logInfo _stx[1]
+  runTermElabM (fun _ => do
+    let e ← Term.elabTerm _stx[1] none
+    logInfo (Expr.dbgToString e)
+    -- How to evaluate the term and compare the result to true?
+    pure ())
+  -- logInfo (Expr.dbgToString (``true))
+  -- throwError "TODO: assert"
+
+#eval 2 == 2
 #assert (2 == 2)
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean
new file mode 100644
index 00000000..bf331d6e
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean
@@ -0,0 +1,113 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: templates for the decreases clauses
+import Base.Primitives
+import HashmapMain.Types
+
+/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: termination measure -/
+@[simp]
+def hashmap_hash_map_allocate_slots_loop_terminates (T : Type)
+  (slots : vec (hashmap_list_t T)) (n : USize) :=
+  (slots, n)
+
+syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) =>
+  `(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/
+@[simp]
+def hashmap_hash_map_clear_slots_loop_terminates (T : Type)
+  (slots : vec (hashmap_list_t T)) (i : USize) :=
+  (slots, i)
+
+syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) =>
+  `(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/
+@[simp]
+def hashmap_hash_map_insert_in_list_loop_terminates (T : Type) (key : USize)
+  (value : T) (ls : hashmap_list_t T) :=
+  (key, value, ls)
+
+syntax "hashmap_hash_map_insert_in_list_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_insert_in_list_loop_decreases $key $value $ls) =>
+  `(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: termination measure -/
+@[simp]
+def hashmap_hash_map_move_elements_from_list_loop_terminates (T : Type)
+  (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) :=
+  (ntable, ls)
+
+syntax "hashmap_hash_map_move_elements_from_list_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_move_elements_from_list_loop_decreases $ntable
+$ls) =>`(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::move_elements]: termination measure -/
+@[simp]
+def hashmap_hash_map_move_elements_loop_terminates (T : Type)
+  (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize)
+  :=
+  (ntable, slots, i)
+
+syntax "hashmap_hash_map_move_elements_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_move_elements_loop_decreases $ntable $slots $i) =>
+  `(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: termination measure -/
+@[simp]
+def hashmap_hash_map_contains_key_in_list_loop_terminates (T : Type)
+  (key : USize) (ls : hashmap_list_t T) :=
+  (key, ls)
+
+syntax "hashmap_hash_map_contains_key_in_list_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_contains_key_in_list_loop_decreases $key $ls) =>
+  `(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: termination measure -/
+@[simp]
+def hashmap_hash_map_get_in_list_loop_terminates (T : Type) (key : USize)
+  (ls : hashmap_list_t T) :=
+  (key, ls)
+
+syntax "hashmap_hash_map_get_in_list_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_get_in_list_loop_decreases $key $ls) =>`(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: termination measure -/
+@[simp]
+def hashmap_hash_map_get_mut_in_list_loop_terminates (T : Type)
+  (ls : hashmap_list_t T) (key : USize) :=
+  (ls, key)
+
+syntax "hashmap_hash_map_get_mut_in_list_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_get_mut_in_list_loop_decreases $ls $key) =>
+  `(tactic| sorry)
+
+/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: termination measure -/
+@[simp]
+def hashmap_hash_map_remove_from_list_loop_terminates (T : Type) (key : USize)
+  (ls : hashmap_list_t T) :=
+  (key, ls)
+
+syntax "hashmap_hash_map_remove_from_list_loop_decreases" term+ : tactic
+
+macro_rules
+| `(tactic| hashmap_hash_map_remove_from_list_loop_decreases $key $ls) =>
+  `(tactic| sorry)
+
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 5e78d9cf..ffe3416a 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -5,6 +5,8 @@ import HashmapMain.Types
 import HashmapMain.Opaque
 import HashmapMain.Clauses.Template
 
+section variable (opaque_defs: OpaqueDecls)
+
 /- [hashmap_main::hashmap::hash_key] -/
 def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k
 
@@ -637,15 +639,15 @@ def hashmap_test1_fwd : result Unit :=
             
 
 /- Unit test for [hashmap_main::hashmap::test1] -/
-#assert (hashmap_test1_fwd = ret ())
+#assert (hashmap_test1_fwd = .ret ())
 
 /- [hashmap_main::insert_on_disk] -/
 def insert_on_disk_fwd
   (key : USize) (value : UInt64) (st : state) : result (state × Unit) :=
   do
-    let (st0, hm) <- hashmap_utils_deserialize_fwd st 
+    let (st0, hm) <- opaque_defs.hashmap_utils_deserialize_fwd st 
     let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value 
-    let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 
+    let (st1, _) <- opaque_defs.hashmap_utils_serialize_fwd hm0 st0 
     result.ret (st1, ())
 
 /- [hashmap_main::main] -/
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
index 87b10c59..8b41934d 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
@@ -3,11 +3,13 @@
 import Base.Primitives
 import HashmapMain.Types
 
-/- [hashmap_main::hashmap_utils::deserialize] -/
-axiom hashmap_utils_deserialize_fwd
-  : state -> result (state × (hashmap_hash_map_t UInt64))
-
-/- [hashmap_main::hashmap_utils::serialize] -/
-axiom hashmap_utils_serialize_fwd
-  : hashmap_hash_map_t UInt64 -> state -> result (state × Unit)
-
+structure OpaqueDecls where
+  
+  /- [hashmap_main::hashmap_utils::deserialize] -/
+  hashmap_utils_deserialize_fwd
+    : state -> result (state × (hashmap_hash_map_t UInt64))
+  
+  /- [hashmap_main::hashmap_utils::serialize] -/
+  hashmap_utils_serialize_fwd
+    : hashmap_hash_map_t UInt64 -> state -> result (state × Unit)
+  
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
index d1cd9579..2a3ea462 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
@@ -15,7 +15,5 @@ structure hashmap_hash_map_t (T : Type) where
   hashmap_hash_map_max_load : USize
   hashmap_hash_map_slots : vec (hashmap_list_t T)
 
-
-/- The state type used in the state-error monad -/
-axiom state : Type
+/- The state type used in the state-error monad -/ axiom state : Type
 
diff --git a/tests/lean/hashmap_on_disk/lake-manifest.json b/tests/lean/hashmap_on_disk/lake-manifest.json
new file mode 100644
index 00000000..8ac53836
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "./lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "583f6cfa4bced545c797216b32600d6211b753f9",
+    "name": "mathlib",
+    "inputRev?": null}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "ccff5d4ae7411c5fe741f3139950e8bddf353dea",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "cda27d551340756d5ed6f9b83716a9db799c5537",
+    "name": "std",
+    "inputRev?": "main"}}]}
-- 
cgit v1.2.3