From 262cb9d72593b349af522596cbae29dff03525ea Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Mon, 23 Jan 2023 18:18:33 -0800
Subject: Add a sample test to illustrate potential project structure

---
 tests/lean/hashmap_on_disk/.gitignore              |   5 +
 tests/lean/hashmap_on_disk/Hashmap.lean            |   1 +
 tests/lean/hashmap_on_disk/Hashmap/Funs.lean       | 535 +++++++++++++++++++++
 tests/lean/hashmap_on_disk/Hashmap/Opaque.lean     |  11 +
 tests/lean/hashmap_on_disk/Hashmap/Primitives.lean | 155 ++++++
 tests/lean/hashmap_on_disk/Hashmap/Types.lean      |  23 +
 tests/lean/hashmap_on_disk/Main.lean               |   5 +
 tests/lean/hashmap_on_disk/lakefile.lean           |  15 +
 tests/lean/hashmap_on_disk/lean-toolchain          |   1 +
 9 files changed, 751 insertions(+)
 create mode 100644 tests/lean/hashmap_on_disk/.gitignore
 create mode 100644 tests/lean/hashmap_on_disk/Hashmap.lean
 create mode 100644 tests/lean/hashmap_on_disk/Hashmap/Funs.lean
 create mode 100644 tests/lean/hashmap_on_disk/Hashmap/Opaque.lean
 create mode 100644 tests/lean/hashmap_on_disk/Hashmap/Primitives.lean
 create mode 100644 tests/lean/hashmap_on_disk/Hashmap/Types.lean
 create mode 100644 tests/lean/hashmap_on_disk/Main.lean
 create mode 100644 tests/lean/hashmap_on_disk/lakefile.lean
 create mode 100644 tests/lean/hashmap_on_disk/lean-toolchain

diff --git a/tests/lean/hashmap_on_disk/.gitignore b/tests/lean/hashmap_on_disk/.gitignore
new file mode 100644
index 00000000..a1735e7c
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/.gitignore
@@ -0,0 +1,5 @@
+/build
+/lean_packages/*
+!/lean_packages/manifest.json
+/build
+/lake-packages/*
diff --git a/tests/lean/hashmap_on_disk/Hashmap.lean b/tests/lean/hashmap_on_disk/Hashmap.lean
new file mode 100644
index 00000000..e99d3a6f
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/Hashmap.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean
new file mode 100644
index 00000000..a4f2e3e0
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean
@@ -0,0 +1,535 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: function definitions
+import Hashmap.Primitives
+import Hashmap.Opaque
+import Hashmap.Types
+
+open result
+open hashmap_list_t
+
+/- [hashmap_main::hashmap::hash_key] -/
+def hashmap_hash_key_fwd (k : USize) : result USize := ret k
+
+/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/
+def hashmap_hash_map_allocate_slots_loop_fwd
+  (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) :
+  result (vec (hashmap_list_t T))
+  :=
+  if n > (USize.ofNatCore 0 (by simp))
+  then do
+    let slots0: vec (hashmap_list_t T) <- @vec_push_back (hashmap_list_t T) slots HashmapListNil
+    let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by simp))
+    hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0
+  else ret slots
+termination_by hashmap_hash_map_allocate_slots_loop_fwd _ _ n => n
+decreasing_by sorry
+
+/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/
+def hashmap_hash_map_allocate_slots_fwd
+  (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) :
+  result (vec (hashmap_list_t T))
+  :=
+  hashmap_hash_map_allocate_slots_loop_fwd T slots n
+
+/- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] -/
+def hashmap_hash_map_new_with_capacity_fwd
+  (T : Type) (capacity : USize) (max_load_dividend : USize)
+  (max_load_divisor : USize) :
+  result (hashmap_hash_map_t T)
+  :=
+  let v <- vec_new (hashmap_list_t T) in
+  let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity in
+  let i <- USize.checked_mul capacity max_load_dividend in
+  let i0 <- USize.checked_div i max_load_divisor in
+  ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp)) (max_load_dividend,
+    max_load_divisor) i0 slots)
+
+/- [hashmap_main::hashmap::HashMap::{0}::new] -/
+def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) :=
+  hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by simp))
+    (USize.ofNatCore 4 (by simp)) (USize.ofNatCore 5 (by simp))
+
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
+def hashmap_hash_map_clear_slots_loop_fwd_back
+  (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) :
+  result (vec (hashmap_list_t T))
+  :=
+  let i0 <- vec_len (hashmap_list_t T) slots in
+  if i < i0
+  then (
+    let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in
+    let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i HashmapListNil
+      in
+    hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1)
+  else ret slots
+
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
+def hashmap_hash_map_clear_slots_fwd_back
+  (T : Type) (slots : vec (hashmap_list_t T)) :
+  result (vec (hashmap_list_t T))
+  :=
+  hashmap_hash_map_clear_slots_loop_fwd_back T slots
+    (USize.ofNatCore 0 (by simp))
+
+/- [hashmap_main::hashmap::HashMap::{0}::clear] -/
+def hashmap_hash_map_clear_fwd_back
+  (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) :=
+  let v <- hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots
+    in
+  ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp))
+    self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)
+
+/- [hashmap_main::hashmap::HashMap::{0}::len] -/
+def hashmap_hash_map_len_fwd
+  (T : Type) (self : hashmap_hash_map_t T) : result USize :=
+  ret self.hashmap_hash_map_num_entries
+
+/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
+def hashmap_hash_map_insert_in_list_loop_fwd
+  (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool :=
+  match ls with
+  | HashmapListCons ckey cvalue tl =>
+    if ckey = key
+    then ret false
+    else hashmap_hash_map_insert_in_list_loop_fwd T key value tl
+  | HashmapListNil => ret true
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
+def hashmap_hash_map_insert_in_list_fwd
+  (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool :=
+  hashmap_hash_map_insert_in_list_loop_fwd T key value ls
+
+/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
+def hashmap_hash_map_insert_in_list_loop_back
+  (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) :
+  result (hashmap_list_t T)
+  :=
+  match ls with
+  | HashmapListCons ckey cvalue tl =>
+    if ckey = key
+    then ret (HashmapListCons ckey value tl)
+    else (
+      let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl in
+      ret (HashmapListCons ckey cvalue l))
+  | HashmapListNil =>
+    let l <- HashmapListNil in ret (HashmapListCons key value l)
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
+def hashmap_hash_map_insert_in_list_back
+  (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) :
+  result (hashmap_list_t T)
+  :=
+  hashmap_hash_map_insert_in_list_loop_back T key value ls
+
+/- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/
+def hashmap_hash_map_insert_no_resize_fwd_back
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) :
+  result (hashmap_hash_map_t T)
+  :=
+  let hash <- hashmap_hash_key_fwd key in
+  let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let hash_mod <- USize.checked_rem hash i in
+  let l <-
+    vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
+    in
+  let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l in
+  if inserted
+  then (
+    let i0 <- USize.checked_add self.hashmap_hash_map_num_entries
+      (USize.ofNatCore 1 (by simp)) in
+    let l0 <- hashmap_hash_map_insert_in_list_back T key value l in
+    let v <-
+      vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor
+      self.hashmap_hash_map_max_load v))
+  else (
+    let l0 <- hashmap_hash_map_insert_in_list_back T key value l in
+    let v <-
+      vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+      self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v))
+
+/- [core::num::u32::{9}::MAX] -/
+def core_num_u32_max_body : result UInt32 :=
+  ret (UInt32.ofNatCore 4294967295 (by simp))
+def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body
+
+/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/
+def hashmap_hash_map_move_elements_from_list_loop_fwd_back
+  (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) :
+  result (hashmap_hash_map_t T)
+  :=
+  match ls with
+  | HashmapListCons k v tl =>
+    let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v in
+    hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl
+  | HashmapListNil => ret ntable
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/
+def hashmap_hash_map_move_elements_from_list_fwd_back
+  (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) :
+  result (hashmap_hash_map_t T)
+  :=
+  hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls
+
+/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/
+def hashmap_hash_map_move_elements_loop_fwd_back
+  (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T))
+  (i : USize) :
+  result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))
+  :=
+  let i0 <- vec_len (hashmap_list_t T) slots in
+  if i < i0
+  then (
+    let l <- vec_index_mut_fwd (hashmap_list_t T) slots i in
+    let ls <- mem_replace_fwd (hashmap_list_t T) l HashmapListNil in
+    let ntable0 <-
+      hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls in
+    let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in
+    let l0 <- mem_replace_back (hashmap_list_t T) l HashmapListNil in
+    let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 in
+    hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1)
+  else ret (ntable, slots)
+
+/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/
+def hashmap_hash_map_move_elements_fwd_back
+  (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T))
+  (i : USize) :
+  result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))
+  :=
+  hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i
+
+/- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/
+def hashmap_hash_map_try_resize_fwd_back
+  (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) :=
+  let max_usize <- scalar_cast U32 Usize core_num_u32_max_c in
+  let capacity <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by simp)) in
+  let (i, i0) <- self.hashmap_hash_map_max_load_factor in
+  let i1 <- USize.checked_div n1 i in
+  if capacity <= i1
+  then (
+    let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by simp)) in
+    let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 in
+    let (ntable0, _) <-
+      hashmap_hash_map_move_elements_fwd_back T ntable
+        self.hashmap_hash_map_slots (USize.ofNatCore 0 (by simp)) in
+    ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
+      ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots))
+  else
+    ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
+      self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+
+/- [hashmap_main::hashmap::HashMap::{0}::insert] -/
+def hashmap_hash_map_insert_fwd_back
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) :
+  result (hashmap_hash_map_t T)
+  :=
+  let self0 <- hashmap_hash_map_insert_no_resize_fwd_back T self key value in
+  let i <- hashmap_hash_map_len_fwd T self0 in
+  if i > self0.hashmap_hash_map_max_load
+  then hashmap_hash_map_try_resize_fwd_back T self0
+  else ret self0
+
+/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/
+def hashmap_hash_map_contains_key_in_list_loop_fwd
+  (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool :=
+  match ls with
+  | HashmapListCons ckey t tl =>
+    if ckey = key
+    then ret true
+    else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl
+  | HashmapListNil => ret false
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/
+def hashmap_hash_map_contains_key_in_list_fwd
+  (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool :=
+  hashmap_hash_map_contains_key_in_list_loop_fwd T key ls
+
+/- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/
+def hashmap_hash_map_contains_key_fwd
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result Bool :=
+  let hash <- hashmap_hash_key_fwd key in
+  let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let hash_mod <- USize.checked_rem hash i in
+  let l <-
+    vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in
+  hashmap_hash_map_contains_key_in_list_fwd T key l
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/
+def hashmap_hash_map_get_in_list_loop_fwd
+  (T : Type) (key : USize) (ls : hashmap_list_t T) : result T :=
+  match ls with
+  | HashmapListCons ckey cvalue tl =>
+    if ckey = key
+    then ret cvalue
+    else hashmap_hash_map_get_in_list_loop_fwd T key tl
+  | HashmapListNil => fail_ panic
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/
+def hashmap_hash_map_get_in_list_fwd
+  (T : Type) (key : USize) (ls : hashmap_list_t T) : result T :=
+  hashmap_hash_map_get_in_list_loop_fwd T key ls
+
+/- [hashmap_main::hashmap::HashMap::{0}::get] -/
+def hashmap_hash_map_get_fwd
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T :=
+  let hash <- hashmap_hash_key_fwd key in
+  let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let hash_mod <- USize.checked_rem hash i in
+  let l <-
+    vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in
+  hashmap_hash_map_get_in_list_fwd T key l
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
+def hashmap_hash_map_get_mut_in_list_loop_fwd
+  (T : Type) (ls : hashmap_list_t T) (key : USize) : result T :=
+  match ls with
+  | HashmapListCons ckey cvalue tl =>
+    if ckey = key
+    then ret cvalue
+    else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key
+  | HashmapListNil => fail_ panic
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
+def hashmap_hash_map_get_mut_in_list_fwd
+  (T : Type) (ls : hashmap_list_t T) (key : USize) : result T :=
+  hashmap_hash_map_get_mut_in_list_loop_fwd T ls key
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
+def hashmap_hash_map_get_mut_in_list_loop_back
+  (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) :
+  result (hashmap_list_t T)
+  :=
+  match ls with
+  | HashmapListCons ckey cvalue tl =>
+    if ckey = key
+    then ret (HashmapListCons ckey ret0 tl)
+    else (
+      let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 in
+      ret (HashmapListCons ckey cvalue l))
+  | HashmapListNil => fail_ panic
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
+def hashmap_hash_map_get_mut_in_list_back
+  (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) :
+  result (hashmap_list_t T)
+  :=
+  hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/
+def hashmap_hash_map_get_mut_fwd
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T :=
+  let hash <- hashmap_hash_key_fwd key in
+  let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let hash_mod <- USize.checked_rem hash i in
+  let l <-
+    vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
+    in
+  hashmap_hash_map_get_mut_in_list_fwd T l key
+
+/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/
+def hashmap_hash_map_get_mut_back
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret0 : T) :
+  result (hashmap_hash_map_t T)
+  :=
+  let hash <- hashmap_hash_key_fwd key in
+  let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let hash_mod <- USize.checked_rem hash i in
+  let l <-
+    vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
+    in
+  let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret0 in
+  let v <-
+    vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
+      l0 in
+  ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+    self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)
+
+/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
+def hashmap_hash_map_remove_from_list_loop_fwd
+  (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) :=
+  match ls with
+  | HashmapListCons ckey t tl =>
+    if ckey = key
+    then
+      let mv_ls <-
+        mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl)
+          HashmapListNil in
+      match mv_ls with
+      | HashmapListCons i cvalue tl0 => ret (@some cvalue)
+      | HashmapListNil => fail_ panic
+      end
+    else hashmap_hash_map_remove_from_list_loop_fwd T key tl
+  | HashmapListNil => ret @none
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
+def hashmap_hash_map_remove_from_list_fwd
+  (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) :=
+  hashmap_hash_map_remove_from_list_loop_fwd T key ls
+
+/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
+def hashmap_hash_map_remove_from_list_loop_back
+  (T : Type) (key : USize) (ls : hashmap_list_t T) :
+  result (hashmap_list_t T)
+  :=
+  match ls with
+  | HashmapListCons ckey t tl =>
+    if ckey = key
+    then
+      let mv_ls <-
+        mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl)
+          HashmapListNil in
+      match mv_ls with
+      | HashmapListCons i cvalue tl0 => ret tl0
+      | HashmapListNil => fail_ panic
+      end
+    else (
+      let l <- hashmap_hash_map_remove_from_list_loop_back T key tl in
+      ret (HashmapListCons ckey t l))
+  | HashmapListNil => ret HashmapListNil
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
+def hashmap_hash_map_remove_from_list_back
+  (T : Type) (key : USize) (ls : hashmap_list_t T) :
+  result (hashmap_list_t T)
+  :=
+  hashmap_hash_map_remove_from_list_loop_back T key ls
+
+/- [hashmap_main::hashmap::HashMap::{0}::remove] -/
+def hashmap_hash_map_remove_fwd
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result (option T) :=
+  let hash <- hashmap_hash_key_fwd key in
+  let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let hash_mod <- USize.checked_rem hash i in
+  let l <-
+    vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
+    in
+  let x <- hashmap_hash_map_remove_from_list_fwd T key l in
+  match x with
+  | @none => ret @none
+  | @some x0 =>
+    let _ <- USize.checked_sub self.hashmap_hash_map_num_entries
+      (USize.ofNatCore 1 (by simp)) in
+    ret (@some x0)
+  end
+
+/- [hashmap_main::hashmap::HashMap::{0}::remove] -/
+def hashmap_hash_map_remove_back
+  (T : Type) (self : hashmap_hash_map_t T) (key : USize) :
+  result (hashmap_hash_map_t T)
+  :=
+  let hash <- hashmap_hash_key_fwd key in
+  let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in
+  let hash_mod <- USize.checked_rem hash i in
+  let l <-
+    vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
+    in
+  let x <- hashmap_hash_map_remove_from_list_fwd T key l in
+  match x with
+  | @none =>
+    let l0 <- hashmap_hash_map_remove_from_list_back T key l in
+    let v <-
+      vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+      self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)
+  | @some x0 =>
+    let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries
+      (USize.ofNatCore 1 (by simp)) in
+    let l0 <- hashmap_hash_map_remove_from_list_back T key l in
+    let v <-
+      vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor
+      self.hashmap_hash_map_max_load v)
+  end
+
+/- [hashmap_main::hashmap::test1] -/
+def hashmap_test1_fwd : result unit :=
+  let hm <- hashmap_hash_map_new_fwd UInt64 in
+  let hm0 <-
+    hashmap_hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by simp))
+      (UInt64.ofNatCore 42 (by simp)) in
+  let hm1 <-
+    hashmap_hash_map_insert_fwd_back UInt64 hm0 (USize.ofNatCore 128 (by simp))
+      (UInt64.ofNatCore 18 (by simp)) in
+  let hm2 <-
+    hashmap_hash_map_insert_fwd_back UInt64 hm1
+      (USize.ofNatCore 1024 (by simp)) (UInt64.ofNatCore 138 (by simp)) in
+  let hm3 <-
+    hashmap_hash_map_insert_fwd_back UInt64 hm2
+      (USize.ofNatCore 1056 (by simp)) (UInt64.ofNatCore 256 (by simp)) in
+  let i <- hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by simp))
+    in
+  if not (i = (UInt64.ofNatCore 18 (by simp)))
+  then fail_ panic
+  else (
+    let hm4 <-
+      hashmap_hash_map_get_mut_back UInt64 hm3 (USize.ofNatCore 1024 (by simp))
+        (UInt64.ofNatCore 56 (by simp)) in
+    let i0 <-
+      hashmap_hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp)) in
+    if not (i0 = (UInt64.ofNatCore 56 (by simp)))
+    then fail_ panic
+    else (
+      let x <-
+        hashmap_hash_map_remove_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp))
+        in
+      match x with
+      | @none => fail_ panic
+      | @some x0 =>
+        if not (x0 = (UInt64.ofNatCore 56 (by simp)))
+        then fail_ panic
+        else (
+          let hm5 <-
+            hashmap_hash_map_remove_back UInt64 hm4
+              (USize.ofNatCore 1024 (by simp)) in
+          let i1 <-
+            hashmap_hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by simp))
+            in
+          if not (i1 = (UInt64.ofNatCore 42 (by simp)))
+          then fail_ panic
+          else (
+            let i2 <-
+              hashmap_hash_map_get_fwd UInt64 hm5
+                (USize.ofNatCore 128 (by simp)) in
+            if not (i2 = (UInt64.ofNatCore 18 (by simp)))
+            then fail_ panic
+            else (
+              let i3 <-
+                hashmap_hash_map_get_fwd UInt64 hm5
+                  (USize.ofNatCore 1056 (by simp)) in
+              if not (i3 = (UInt64.ofNatCore 256 (by simp)))
+              then fail_ panic
+              else ret ())))
+      end))
+
+/- Unit test for [hashmap_main::hashmap::test1] -/
+#assert (hashmap_test1_fwd = ret ())
+
+/- [hashmap_main::insert_on_disk] -/
+def insert_on_disk_fwd
+  (key : USize) (value : UInt64) (st : state) : result (state × unit) :=
+  let (st0, hm) <- hashmap_utils_deserialize_fwd st in
+  let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value in
+  let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 in
+  ret (st1, ())
+
+/- [hashmap_main::main] -/
+def main_fwd : result unit := ret ()
+
+/- Unit test for [hashmap_main::main] -/
+#assert (main_fwd = ret ())
+
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean b/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean
new file mode 100644
index 00000000..164995f0
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean
@@ -0,0 +1,11 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: opaque function definitions
+import Hashmap.Primitives
+import Hashmap.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)
+
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean
new file mode 100644
index 00000000..83de98db
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean
@@ -0,0 +1,155 @@
+-------------
+-- PRELUDE --
+-------------
+
+-- Results & monadic combinators
+
+inductive error where
+   | assertionFailure: error
+   | integerOverflow: error
+   | arrayOutOfBounds: error
+   | maximumSizeExceeded: error
+   | panic: error
+deriving Repr
+
+open error
+
+inductive result (α : Type u) where
+  | ret (v: α): result α
+  | fail (e: error): result α 
+deriving Repr
+
+open result
+
+-- TODO: is there automated syntax for these discriminators?
+def is_ret (α: Type) (r: result α): Bool :=
+  match r with
+  | result.ret _ => true
+  | result.fail _ => false
+
+def eval_global (α: Type) (x: result α) (h: is_ret α x): α :=
+  match x with
+  | result.fail _ => by contradiction
+  | result.ret x => x
+
+def bind (x: result α) (f: α -> result β) : result β :=
+  match x with
+  | ret v  => f v 
+  | fail v => fail v
+
+-- Allows using result in do-blocks
+instance : Bind result where
+  bind := bind
+
+-- Allows using return x in do-blocks
+instance : Pure result where
+  pure := fun x => ret x
+
+def massert (b:Bool) : result Unit :=
+  if b then return () else fail assertionFailure
+
+-- Machine integers
+
+-- NOTE: we reuse the USize type from prelude.lean, because at least we know
+-- it's defined in an idiomatic style that is going to make proofs easy (and
+-- indeed, several proofs here are much shortened compared to Aymeric's earlier
+-- attempt.) This is not stricto sensu the *correct* thing to do, because one
+-- can query at run-time the value of USize, which we do *not* want to do (we
+-- don't know what target we'll run on!), but when the day comes, we'll just
+-- define our own USize.
+-- ANOTHER NOTE: there is USize.sub but it has wraparound semantics, which is
+-- not something we want to define (I think), so we use our own monadic sub (but
+-- is it in line with the Rust behavior?)
+
+-- TODO: I am somewhat under the impression that subtraction is defined as a
+-- total function over nats...? the hypothesis in the if condition is not used
+-- in the then-branch which confuses me quite a bit
+
+-- TODO: add a refinement for the result (just like vec_push_back below) that
+-- explains that the toNat of the result (in the case of success) is the sub of
+-- the toNat of the arguments (i.e. intrinsic specification)
+-- ... do we want intrinsic specifications for the builtins? that might require
+-- some careful type annotations in the monadic notation for clients, but may
+-- give us more "for free"
+
+-- Note from Chris Bailey: "If there's more than one salient property of your
+-- definition then the subtyping strategy might get messy, and the property part
+-- of a subtype is less discoverable by the simplifier or tactics like
+-- library_search." Try to settle this with a Lean expert on what is the most
+-- productive way to go about this?
+
+-- Further thoughts: look at what has been done here:
+-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean
+-- and
+-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean
+-- which both contain a fair amount of reasoning already!
+def USize.checked_sub (n: USize) (m: Nat): result USize :=
+  -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed?
+  if USize.toNat n >= m then
+    let n' := USize.toNat n
+    let r := USize.ofNatCore (n' - m) (by
+      have h: n' - m <= n' := by
+        apply Nat.sub_le_of_le_add
+        case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left
+      apply Nat.lt_of_le_of_lt h
+      apply n.val.isLt
+    )
+    return r
+  else
+    fail integerOverflow
+
+-- TODO: settle the style for usize_sub before we write these
+def USize.checked_mul (n: USize) (m: USize): result USize := sorry
+def USize.checked_div (n: USize) (m: USize): result USize := sorry
+
+#eval USize.checked_sub 10 20
+#eval USize.checked_sub 20 10
+-- NOTE: compare with concrete behavior here, which I do not think we want
+#eval USize.sub 0 1
+#eval UInt8.add 255 255
+
+-- Vectors
+
+def vec (α : Type u) := { l : List α // List.length l < USize.size }
+
+def vec_new : result (vec α) := return ⟨ [], by {
+  match USize.size, usize_size_eq with
+  | _, Or.inl rfl => simp
+  | _, Or.inr rfl => simp
+  } ⟩
+
+def vec_len (v : vec α) : USize :=
+  let ⟨ v, l ⟩ := v
+  USize.ofNatCore (List.length v) l
+
+#eval do
+  return (vec_len (<- @vec_new Nat))
+ 
+def vec_push_fwd (_ : vec α) (_ : α) : Unit := ()
+
+-- TODO: more precise error condition here for the fail case
+-- TODO: I originally wrote `List.length v.val < USize.size - 1`; how can one
+-- make the proof work in that case? Probably need to import tactics from
+-- mathlib to deal with inequalities... would love to see an example.
+def vec_push_back (v : vec α) (x : α) : { res: result (vec α) //
+  match res with | fail _ => True | ret v' => List.length v'.val = List.length v.val + 1}
+  :=
+  if h : List.length v.val + 1 < USize.size then
+    ⟨ return ⟨List.concat v.val x,
+      by
+        rw [List.length_concat]
+        assumption
+     ⟩, by simp ⟩
+  else
+    ⟨ fail maximumSizeExceeded, by simp ⟩
+
+#eval do
+  -- NOTE: the // notation is syntactic sugar for Subtype, a refinement with
+  -- fields val and property. However, Lean's elaborator can automatically
+  -- select the `val` field if the context provides a type annotation. We
+  -- annotate `x`, which relieves us of having to write `.val` on the right-hand
+  -- side of the monadic let.
+  let x: vec Nat ← vec_push_back (<- vec_new) 1
+  -- TODO: strengthen post-condition above and do a demo to show that we can
+  -- safely eliminate the `fail` case
+  return (vec_len x)
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Types.lean b/tests/lean/hashmap_on_disk/Hashmap/Types.lean
new file mode 100644
index 00000000..90022fe5
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/Hashmap/Types.lean
@@ -0,0 +1,23 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: type definitions
+import Hashmap.Primitives
+
+/- [hashmap_main::hashmap::List] -/
+inductive hashmap_list_t (T : Type) :=
+| HashmapListCons : USize -> T -> hashmap_list_t T -> hashmap_list_t T
+| HashmapListNil : hashmap_list_t T
+
+/- [hashmap_main::hashmap::HashMap] -/
+structure hashmap_hash_map_t (T : Type) where
+  hashmap_hash_map_num_entries : USize
+  hashmap_hash_map_max_load_factor : (USize × USize)
+  hashmap_hash_map_max_load : USize
+  hashmap_hash_map_slots : vec (hashmap_list_t T)
+
+/- [core::num::u32::{9}::MAX] -/
+def core_num_u32_max_body : result UInt32 :=
+  return (UInt32.ofNatCore 4294967295 (by simp))
+def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp)
+
+/- The state type used in the state-error monad -/
+axiom state : Type
\ No newline at end of file
diff --git a/tests/lean/hashmap_on_disk/Main.lean b/tests/lean/hashmap_on_disk/Main.lean
new file mode 100644
index 00000000..7bde1315
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/Main.lean
@@ -0,0 +1,5 @@
+import «Hashmap»
+import Hashmap.Primitives
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean
new file mode 100644
index 00000000..d2a31ffe
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/lakefile.lean
@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+package «hashmap» {
+  -- add package configuration options here
+}
+
+lean_lib «Hashmap» {
+  -- add library configuration options here
+}
+
+@[default_target]
+lean_exe «hashmap» {
+  root := `Main
+}
diff --git a/tests/lean/hashmap_on_disk/lean-toolchain b/tests/lean/hashmap_on_disk/lean-toolchain
new file mode 100644
index 00000000..bbf57f10
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-01-21
-- 
cgit v1.2.3