From 9b281e021b3b2dbfa6ff265cc843e0aac3b400ac Mon Sep 17 00:00:00 2001
From: Zyad Hassan
Date: Fri, 12 Apr 2024 10:48:03 -0700
Subject: Add core::option::unwrap builtin

---
 backends/lean/Base/Primitives/Base.lean   | 5 +++++
 backends/lean/Base/Primitives/Core.lean   | 8 ++++++++
 backends/lean/Base/Primitives/Scalar.lean | 5 -----
 compiler/ExtractBuiltin.ml                | 2 ++
 4 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 4c5b2795..ac4fd340 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -76,6 +76,11 @@ def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) :
   | fail _ | div => by contradiction
   | ok x => x
 
+def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a :=
+  match x with
+  | some x => ok x
+  | none => fail e
+
 /- DO-DSL SUPPORT -/
 
 def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean
index 99f65985..b7dd6d2c 100644
--- a/backends/lean/Base/Primitives/Core.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -51,4 +51,12 @@ def clone.CloneBool : clone.Clone Bool := {
   clone := fun b => ok (clone.impls.CloneBool.clone b)
 }
 
+namespace option
+
+/- [core::option::{core::option::Option<T>}::unwrap] -/
+def Option.unwrap (T : Type) (x : Option T) : Result T :=
+  Result.ofOption x Error.panic
+
+end option -- core.option
+
 end core
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 014decb1..2bee8a2f 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -364,11 +364,6 @@ def Scalar.tryMkOpt (ty : ScalarTy) (x : Int) : Option (Scalar ty) :=
     some (Scalar.ofIntCore x (Scalar.check_bounds_imp_in_bounds h))
   else none
 
-def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a :=
-  match x with
-  | some x => ok x
-  | none => fail e
-
 def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
   Result.ofOption (tryMkOpt ty x) integerOverflow
 
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index a9b939b5..e84d5896 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -383,6 +383,8 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
        @A>>}::deref_mut"
       (Some "alloc.vec.DerefMutVec.deref_mut")
       (Some [ true; false ]);
+    mk_fun "core::option::{core::option::Option<@T>}::unwrap"
+      (Some "core.option.Option.unwrap") None;
   ]
   @ List.flatten
       (List.map
-- 
cgit v1.2.3


From 97a70ecd3e70d08fae544dc11cca0fb1e06e5a66 Mon Sep 17 00:00:00 2001
From: Zyad Hassan
Date: Wed, 24 Apr 2024 09:28:38 -0700
Subject: Update tests

---
 tests/coq/betree/BetreeMain_FunsExternal_Template.v           | 7 -------
 tests/coq/misc/External_FunsExternal_Template.v               | 7 -------
 tests/fstar/betree/BetreeMain.FunsExternal.fsti               | 6 ------
 tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti | 6 ------
 tests/fstar/misc/External.FunsExternal.fsti                   | 6 ------
 tests/lean/BetreeMain/FunsExternal_Template.lean              | 6 ------
 tests/lean/External/FunsExternal_Template.lean                | 6 ------
 7 files changed, 44 deletions(-)

diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
index 1367bac2..58be2733 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -37,11 +37,4 @@ Axiom betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
 .
 
-(** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
 End BetreeMain_FunsExternal_Template.
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 24dd2d47..8658236f 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -25,11 +25,4 @@ Axiom core_num_nonzero_NonZeroU32_new
   : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
 .
 
-(** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
 End External_FunsExternal_Template.
diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
index 3aad9390..8be98acf 100644
--- a/tests/fstar/betree/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
@@ -28,9 +28,3 @@ val betree_utils_load_leaf_node
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
-(** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-val core_option_Option_unwrap
-  (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
index 3aad9390..8be98acf 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -28,9 +28,3 @@ val betree_utils_load_leaf_node
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
-(** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-val core_option_Option_unwrap
-  (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index 4c1c58b7..64d6d883 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -17,9 +17,3 @@ val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
 val core_num_nonzero_NonZeroU32_new
   : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
 
-(** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-val core_option_Option_unwrap
-  (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index 0b3e4ef4..0dcce5ca 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -28,9 +28,3 @@ axiom betree_utils.load_leaf_node
 axiom betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit)
 
-/- [core::option::{core::option::Option<T>}::unwrap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-   Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
-axiom core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T)
-
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index 38151dc9..34b0552a 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -18,9 +18,3 @@ axiom core.mem.swap
 axiom core.num.nonzero.NonZeroU32.new
   : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
 
-/- [core::option::{core::option::Option<T>}::unwrap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-   Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
-axiom core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T)
-
-- 
cgit v1.2.3


From 1728dced8484befe35ef61fdf4ccd62b93fbb19d Mon Sep 17 00:00:00 2001
From: Zyad Hassan
Date: Wed, 24 Apr 2024 10:01:27 -0700
Subject: Fix a couple of tests

---
 tests/lean/BetreeMain/Funs.lean         | 4 ++--
 tests/lean/BetreeMain/FunsExternal.lean | 5 -----
 tests/lean/External/Funs.lean           | 3 ++-
 tests/lean/External/FunsExternal.lean   | 5 -----
 4 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 0c31b9bc..57b334fa 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -238,11 +238,11 @@ divergent def betree.Node.apply_upserts
       betree.Node.apply_upserts msgs1 (some v) key st
   else
     do
-    let (st1, v) ← core.option.Option.unwrap U64 prev st
+    let v ← core.option.Option.unwrap U64 prev
     let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
-    Result.ok (st1, (v, msgs1))
+    Result.ok (st, (v, msgs1))
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/BetreeMain/FunsExternal.lean
index 71d26da4..d26177fb 100644
--- a/tests/lean/BetreeMain/FunsExternal.lean
+++ b/tests/lean/BetreeMain/FunsExternal.lean
@@ -28,8 +28,3 @@ def betree_utils.load_leaf_node
 def betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit) :=
   fun _ _ _ => .fail .panic
-
-/- [core::option::Option::{0}::unwrap] -/
-def core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T) :=
-  fun _ _ => .fail .panic
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 78e0f95c..3bdd70e3 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -19,7 +19,8 @@ def test_new_non_zero_u32
   (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) :=
   do
   let (st1, o) ← core.num.nonzero.NonZeroU32.new x st
-  core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st1
+  let o1 ← core.option.Option.unwrap core.num.nonzero.NonZeroU32 o
+  Result.ok (st1, o1)
 
 /- [external::test_vec]:
    Source: 'src/external.rs', lines 17:0-17:17 -/
diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean
index b6efc65f..7adf0922 100644
--- a/tests/lean/External/FunsExternal.lean
+++ b/tests/lean/External/FunsExternal.lean
@@ -15,8 +15,3 @@ def core.mem.swap
 def core.num.nonzero.NonZeroU32.new :
   U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) :=
   fun _ _ => .fail .panic
-
-/- [core::option::Option::{0}::unwrap] -/
-def core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T) :=
-  fun _ _ => .fail .panic
-- 
cgit v1.2.3


From eb5b2e76de6e2c6780b9817c1424777276ea5e00 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 25 Apr 2024 16:27:43 +0200
Subject: Update the backend and ExtractBuiltin.ml

---
 backends/coq/Primitives.v               | 7 +++++++
 backends/fstar/Primitives.fst           | 6 ++++++
 backends/lean/Base/Primitives/Core.lean | 2 +-
 compiler/ExtractBuiltin.ml              | 5 ++++-
 4 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean
index b7dd6d2c..14a51bc1 100644
--- a/backends/lean/Base/Primitives/Core.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -51,7 +51,7 @@ def clone.CloneBool : clone.Clone Bool := {
   clone := fun b => ok (clone.impls.CloneBool.clone b)
 }
 
-namespace option
+namespace option -- core.option
 
 /- [core::option::{core::option::Option<T>}::unwrap] -/
 def Option.unwrap (T : Type) (x : Option T) : Result T :=
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index d4a6f736..248d0fa8 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -554,14 +554,17 @@ let builtin_fun_effects =
       (fun n -> (n, { can_fail = false; stateful = false }))
       no_fail_no_state_funs
   in
+  (* TODO: all the functions registered in the [builtin_funs] above should
+     be considered a not using a state. There is a lot of redundancy
+     right now. *)
   let no_state_funs =
     [
-      (* TODO: redundancy with the funs information above *)
       "alloc::vec::{alloc::vec::Vec<@T, @A>}::push";
       "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
        @I>}::index";
       "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
        @I>}::index_mut";
+      "core::option::{core::option::Option<@T>}::unwrap";
     ]
   in
   let no_state_funs =
-- 
cgit v1.2.3


From 036756d6bddbcf9bc936489779ed36c7e4d22d14 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 25 Apr 2024 16:28:30 +0200
Subject: Regenerate and fix the tests

---
 tests/coq/arrays/Primitives.v                      |  7 +++++++
 tests/coq/betree/BetreeMain_Funs.v                 | 24 ++++++++++------------
 tests/coq/betree/BetreeMain_FunsExternal.v         |  6 ------
 tests/coq/betree/Primitives.v                      |  7 +++++++
 tests/coq/demo/Primitives.v                        |  7 +++++++
 tests/coq/hashmap/Primitives.v                     |  7 +++++++
 tests/coq/hashmap_on_disk/Primitives.v             |  7 +++++++
 tests/coq/misc/Primitives.v                        |  7 +++++++
 tests/coq/traits/Primitives.v                      |  7 +++++++
 tests/fstar/arrays/Primitives.fst                  |  6 ++++++
 tests/fstar/betree/BetreeMain.Clauses.Template.fst |  2 +-
 tests/fstar/betree/BetreeMain.Clauses.fst          |  2 +-
 tests/fstar/betree/BetreeMain.Funs.fst             | 20 +++++++++---------
 tests/fstar/betree/Primitives.fst                  |  6 ++++++
 .../BetreeMain.Clauses.Template.fst                |  2 +-
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst | 20 +++++++++---------
 tests/fstar/betree_back_stateful/Primitives.fst    |  6 ++++++
 tests/fstar/demo/Primitives.fst                    |  6 ++++++
 tests/fstar/hashmap/Primitives.fst                 |  6 ++++++
 tests/fstar/hashmap_on_disk/Primitives.fst         |  6 ++++++
 tests/fstar/misc/Primitives.fst                    |  6 ++++++
 tests/fstar/traits/Primitives.fst                  |  6 ++++++
 tests/lean/BetreeMain/Funs.lean                    | 18 ++++++++--------
 23 files changed, 140 insertions(+), 51 deletions(-)

diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/tests/coq/arrays/Primitives.v
+++ b/tests/coq/arrays/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 80518eab..c31713be 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -275,8 +275,8 @@ Fixpoint betree_Node_lookup_in_bindings
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 Fixpoint betree_Node_apply_upserts
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) :
-  result (state * (u64 * (betree_List_t (u64 * betree_Message_t))))
+  (key : u64) :
+  result (u64 * (betree_List_t (u64 * betree_Message_t)))
   :=
   match n with
   | O => Fail_ OutOfFuel
@@ -292,15 +292,14 @@ Fixpoint betree_Node_apply_upserts
       | Betree_Message_Delete => Fail_ Failure
       | Betree_Message_Upsert s =>
         v <- betree_upsert_update prev s;
-        betree_Node_apply_upserts n1 msgs1 (Some v) key st
+        betree_Node_apply_upserts n1 msgs1 (Some v) key
       end)
     else (
-      p <- core_option_Option_unwrap u64 prev st;
-      let (st1, v) := p in
+      v <- core_option_Option_unwrap u64 prev;
       msgs1 <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);
-      Ok (st1, (v, msgs1)))
+      Ok (v, msgs1))
   end
 .
 
@@ -371,14 +370,13 @@ with betree_Node_lookup
             let (v, node1) := p4 in
             p5 <-
               betree_Node_apply_upserts n1 (Betree_List_Cons (k,
-                Betree_Message_Upsert ufs) l) v key st2;
-            let (st3, p6) := p5 in
-            let (v1, pending1) := p6 in
+                Betree_Message_Upsert ufs) l) v key;
+            let (v1, pending1) := p5 in
             msgs1 <- lookup_first_message_for_key_back pending1;
-            p7 <-
-              betree_store_internal_node node1.(betree_Internal_id) msgs1 st3;
-            let (st4, _) := p7 in
-            Ok (st4, (Some v1, Betree_Node_Internal node1))
+            p6 <-
+              betree_store_internal_node node1.(betree_Internal_id) msgs1 st2;
+            let (st3, _) := p6 in
+            Ok (st3, (Some v1, Betree_Node_Internal node1))
           end
       | Betree_List_Nil =>
         p2 <- betree_Internal_lookup_in_children n1 node key st1;
diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/BetreeMain_FunsExternal.v
index 2d77c4ed..099a2e8f 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal.v
@@ -36,10 +36,4 @@ Axiom betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
 .
 
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
 End BetreeMain_FunsExternal.
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/coq/demo/Primitives.v b/tests/coq/demo/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/tests/coq/demo/Primitives.v
+++ b/tests/coq/demo/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v
index 5ffda12f..b29fce43 100644
--- a/tests/coq/traits/Primitives.v
+++ b/tests/coq/traits/Primitives.v
@@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+Definition core_option_Option_unwrap (T : Type) (x : option T) : result T :=
+  match x with
+  | None => Fail_ Failure
+  | Some x => Ok x
+  end.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/fstar/arrays/Primitives.fst b/tests/fstar/arrays/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/arrays/Primitives.fst
+++ b/tests/fstar/arrays/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index de56ba46..b317dca4 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -45,7 +45,7 @@ let betree_Node_lookup_in_bindings_decreases (key : u64)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) : nat =
+  (key : u64) : nat =
   admit ()
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst
index ed5c5069..b95d4c7e 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.fst
@@ -134,7 +134,7 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) : betree_List_t (u64 & betree_Message_t) =
+  (key : u64) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 8e64f43f..89396df0 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -223,9 +223,9 @@ let rec betree_Node_lookup_in_bindings
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) :
-  Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t)))))
-  (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
+  (key : u64) :
+  Tot (result (u64 & (betree_List_t (u64 & betree_Message_t))))
+  (decreases (betree_Node_apply_upserts_decreases msgs prev key))
   =
   let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
@@ -237,14 +237,14 @@ let rec betree_Node_apply_upserts
     | Betree_Message_Delete -> Fail Failure
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update prev s in
-      betree_Node_apply_upserts msgs1 (Some v) key st
+      betree_Node_apply_upserts msgs1 (Some v) key
     end
   else
-    let* (st1, v) = core_option_Option_unwrap u64 prev st in
+    let* v = core_option_Option_unwrap u64 prev in
     let* msgs1 =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in
-    Ok (st1, (v, msgs1))
+    Ok (v, msgs1)
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
@@ -298,12 +298,12 @@ and betree_Node_lookup
         | Betree_Message_Upsert ufs ->
           let* (st2, (v, node1)) =
             betree_Internal_lookup_in_children node key st1 in
-          let* (st3, (v1, pending1)) =
+          let* (v1, pending1) =
             betree_Node_apply_upserts (Betree_List_Cons (k,
-              Betree_Message_Upsert ufs) l) v key st2 in
+              Betree_Message_Upsert ufs) l) v key in
           let* msgs1 = lookup_first_message_for_key_back pending1 in
-          let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in
-          Ok (st4, (Some v1, Betree_Node_Internal node1))
+          let* (st3, _) = betree_store_internal_node node1.id msgs1 st2 in
+          Ok (st3, (Some v1, Betree_Node_Internal node1))
         end
     | Betree_List_Nil ->
       let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index de56ba46..b317dca4 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -45,7 +45,7 @@ let betree_Node_lookup_in_bindings_decreases (key : u64)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) : nat =
+  (key : u64) : nat =
   admit ()
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 8e64f43f..89396df0 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -223,9 +223,9 @@ let rec betree_Node_lookup_in_bindings
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) :
-  Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t)))))
-  (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
+  (key : u64) :
+  Tot (result (u64 & (betree_List_t (u64 & betree_Message_t))))
+  (decreases (betree_Node_apply_upserts_decreases msgs prev key))
   =
   let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
@@ -237,14 +237,14 @@ let rec betree_Node_apply_upserts
     | Betree_Message_Delete -> Fail Failure
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update prev s in
-      betree_Node_apply_upserts msgs1 (Some v) key st
+      betree_Node_apply_upserts msgs1 (Some v) key
     end
   else
-    let* (st1, v) = core_option_Option_unwrap u64 prev st in
+    let* v = core_option_Option_unwrap u64 prev in
     let* msgs1 =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in
-    Ok (st1, (v, msgs1))
+    Ok (v, msgs1)
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
@@ -298,12 +298,12 @@ and betree_Node_lookup
         | Betree_Message_Upsert ufs ->
           let* (st2, (v, node1)) =
             betree_Internal_lookup_in_children node key st1 in
-          let* (st3, (v1, pending1)) =
+          let* (v1, pending1) =
             betree_Node_apply_upserts (Betree_List_Cons (k,
-              Betree_Message_Upsert ufs) l) v key st2 in
+              Betree_Message_Upsert ufs) l) v key in
           let* msgs1 = lookup_first_message_for_key_back pending1 in
-          let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in
-          Ok (st4, (Some v1, Betree_Node_Internal node1))
+          let* (st3, _) = betree_store_internal_node node1.id msgs1 st2 in
+          Ok (st3, (Some v1, Betree_Node_Internal node1))
         end
     | Betree_List_Nil ->
       let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/fstar/demo/Primitives.fst b/tests/fstar/demo/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/demo/Primitives.fst
+++ b/tests/fstar/demo/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/fstar/traits/Primitives.fst b/tests/fstar/traits/Primitives.fst
index c7c9f9db..9951ccc3 100644
--- a/tests/fstar/traits/Primitives.fst
+++ b/tests/fstar/traits/Primitives.fst
@@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+(** [core::option::{core::option::Option<T>}::unwrap] *)
+let core_option_Option_unwrap (t : Type0) (x : option t) : result t =
+  match x with
+  | None -> Fail Failure
+  | Some x -> Ok x
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 0c31b9bc..f0032d51 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -219,8 +219,8 @@ divergent def betree.Node.lookup_in_bindings
    Source: 'src/betree.rs', lines 819:4-819:90 -/
 divergent def betree.Node.apply_upserts
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
-  (st : State) :
-  Result (State × (U64 × (betree.List (U64 × betree.Message))))
+  :
+  Result (U64 × (betree.List (U64 × betree.Message)))
   :=
   do
   let b ← betree.ListPairU64T.head_has_key betree.Message msgs key
@@ -235,14 +235,14 @@ divergent def betree.Node.apply_upserts
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update prev s
-      betree.Node.apply_upserts msgs1 (some v) key st
+      betree.Node.apply_upserts msgs1 (some v) key
   else
     do
-    let (st1, v) ← core.option.Option.unwrap U64 prev st
+    let v ← core.option.Option.unwrap U64 prev
     let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
-    Result.ok (st1, (v, msgs1))
+    Result.ok (v, msgs1)
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
@@ -307,13 +307,13 @@ divergent def betree.Node.lookup
           let (st2, (v, node1)) ←
             betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1)
               key st1
-          let (st3, (v1, pending1)) ←
+          let (v1, pending1) ←
             betree.Node.apply_upserts (betree.List.Cons (k,
-              betree.Message.Upsert ufs) l) v key st2
+              betree.Message.Upsert ufs) l) v key
           let ⟨ i2, i3, n2, n3 ⟩ := node1
           let msgs1 ← lookup_first_message_for_key_back pending1
-          let (st4, _) ← betree.store_internal_node i2 msgs1 st3
-          Result.ok (st4, (some v1, betree.Node.Internal (betree.Internal.mk i2
+          let (st3, _) ← betree.store_internal_node i2 msgs1 st2
+          Result.ok (st3, (some v1, betree.Node.Internal (betree.Internal.mk i2
             i3 n2 n3)))
     | betree.List.Nil =>
       do
-- 
cgit v1.2.3


From dbabb0124814c38f11f839f8a67146011107133d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 26 Apr 2024 10:28:32 +0200
Subject: Update a decreases clause

---
 tests/fstar/betree/BetreeMain.Clauses.fst | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst
index b95d4c7e..fcef89ed 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.fst
@@ -130,12 +130,18 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
+
+let rec list_length (#a : Type0) (ls : betree_List_t a) : nat =
+  match ls with
+  | Betree_List_Cons _ ls -> 1 + list_length ls
+  | Betree_List_Nil -> 0
+
 (** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) : betree_List_t (u64 & betree_Message_t) =
-  msgs
+  list_length msgs
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
 unfold
-- 
cgit v1.2.3


From 518fa3f104d6b98528873d4bf37e182ee1bbe69d Mon Sep 17 00:00:00 2001
From: Son HO
Date: Fri, 26 Apr 2024 10:30:09 +0200
Subject: Update compiler/ExtractBuiltin.ml

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>---
 compiler/ExtractBuiltin.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 248d0fa8..a7ab6da0 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -555,7 +555,7 @@ let builtin_fun_effects =
       no_fail_no_state_funs
   in
   (* TODO: all the functions registered in the [builtin_funs] above should
-     be considered a not using a state. There is a lot of redundancy
+     be considered as not using a state. There is a lot of redundancy
      right now. *)
   let no_state_funs =
     [
-- 
cgit v1.2.3


From 192b0e492c07a8bc5900ba6ebe6eae36a7120a28 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 26 Apr 2024 10:33:52 +0200
Subject: Update the F* clauses for the betree

---
 tests/fstar/betree/BetreeMain.Clauses.fst | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst
index fcef89ed..8f62d66d 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.fst
@@ -130,7 +130,6 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
-
 let rec list_length (#a : Type0) (ls : betree_List_t a) : nat =
   match ls with
   | Betree_List_Cons _ ls -> 1 + list_length ls
@@ -140,7 +139,7 @@ let rec list_length (#a : Type0) (ls : betree_List_t a) : nat =
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) : betree_List_t (u64 & betree_Message_t) =
+  (key : u64) : nat =
   list_length msgs
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
-- 
cgit v1.2.3


From fe8d14cd8b7ba907d5248d574619e93e6d1d253a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 26 Apr 2024 10:44:23 +0200
Subject: Update the decreases clauses for the betree

---
 tests/fstar/betree/BetreeMain.Clauses.fst               | 9 ++-------
 tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst | 2 +-
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst
index 8f62d66d..b95d4c7e 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.fst
@@ -130,17 +130,12 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
-let rec list_length (#a : Type0) (ls : betree_List_t a) : nat =
-  match ls with
-  | Betree_List_Cons _ ls -> 1 + list_length ls
-  | Betree_List_Nil -> 0
-
 (** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) : nat =
-  list_length msgs
+  (key : u64) : betree_List_t (u64 & betree_Message_t) =
+  msgs
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
 unfold
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
index ed5c5069..b95d4c7e 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
@@ -134,7 +134,7 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) : betree_List_t (u64 & betree_Message_t) =
+  (key : u64) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
-- 
cgit v1.2.3