WIP

6 files changed, 206 insertions, 40 deletions

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"}}]}