From 38276f00f6aaebb70392775b97577c73a657005a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 May 2022 15:50:00 +0200
Subject: Make the betree work

---
 tests/betree/BetreeMain.Clauses.fst | 114 +++++++++++++++++++++++-------------
 1 file changed, 72 insertions(+), 42 deletions(-)

(limited to 'tests/betree/BetreeMain.Clauses.fst')

diff --git a/tests/betree/BetreeMain.Clauses.fst b/tests/betree/BetreeMain.Clauses.fst
index b241e756..8fb43e07 100644
--- a/tests/betree/BetreeMain.Clauses.fst
+++ b/tests/betree/BetreeMain.Clauses.fst
@@ -7,88 +7,118 @@ open BetreeMain.Types
 
 (** [betree_main::betree::List::{1}::len]: decreases clause *)
 unfold
-let betree_list_1_len_decreases (t : Type0) (self : betree_list_t t) : nat =
-  admit ()
+let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : betree_list_t t =
+  self
 
 (** [betree_main::betree::List::{1}::split_at]: decreases clause *)
 unfold
-let betree_list_1_split_at_decreases (t : Type0) (self : betree_list_t t)
+let betree_list_split_at_decreases (t : Type0) (self : betree_list_t t)
   (n : u64) : nat =
-  admit ()
+  n
 
 (** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
 unfold
-let betree_list_2_partition_at_pivot_decreases (t : Type0)
-  (self : betree_list_t (u64 & t)) (pivot : u64) : nat =
-  admit ()
+let betree_list_partition_at_pivot_decreases (t : Type0)
+  (self : betree_list_t (u64 & t)) (pivot : u64) : betree_list_t (u64 & t) =
+  self
 
 (** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
 unfold
-let betree_node_5_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
+let betree_node_lookup_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
+  bindings
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
 unfold
-let betree_node_5_lookup_first_message_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
+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
 
 (** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
 unfold
-let betree_node_5_apply_upserts_decreases
+let betree_node_apply_upserts_decreases
   (msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
-  (key : u64) (st : state) : nat =
-  admit ()
+  (key : u64) (st : state) : betree_list_t (u64 & betree_message_t) =
+  msgs
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
 unfold
-let betree_internal_4_lookup_in_children_decreases (self : betree_internal_t)
-  (key : u64) (st : state) : nat =
-  admit ()
+let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
+  (key : u64) (st : state) : betree_internal_t =
+  self
 
 (** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
 unfold
-let betree_node_5_lookup_decreases (self : betree_node_t) (key : u64)
-  (st : state) : nat =
-  admit ()
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
+  (st : state) : betree_node_t =
+  self
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
-let betree_node_5_lookup_mut_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
+let betree_node_lookup_mut_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
+  bindings
+
+unfold
+let betree_node_apply_messages_to_leaf_decreases
+  (bindings : betree_list_t (u64 & u64))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+  new_msgs
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
 unfold
-let betree_node_5_filter_messages_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
+let betree_node_filter_messages_for_key_decreases (key : u64)
+  (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+  msgs
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
 unfold
-let betree_node_5_lookup_first_message_after_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
+let betree_node_lookup_first_message_after_key_decreases (key : u64)
+  (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+  msgs
+
+let betree_node_apply_messages_to_internal_decreases
+  (msgs : betree_list_t (u64 & betree_message_t))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
+  new_msgs
+
+(* This is annoying, we can't use the following trick when defining decrease
+ * clauses as separate functions:
+ * [https://github.com/FStarLang/FStar/issues/138]
+ *
+ * Note that the quantity which effectively decreases is:
+ *
+ *   [betree_size; messages_length]
+ *   where messages_length is 0 when there are no messages
+ *   (and where we use the lexicographic ordering, of course)
+ *
+ * For now, we "patch" the code directly (we need to find a better way...)
+ *)
+let rec betree_size (bt : betree_node_t) : nat =
+  match bt with
+  | BetreeNodeInternal node -> 1 + betree_internal_size node
+  | BetreeNodeLeaf _ -> 1
+
+and betree_internal_size (node : betree_internal_t) : nat =
+  1 + betree_size node.betree_internal_left + betree_size node.betree_internal_right
+
+let rec betree_list_len (#a : Type0) (ls : betree_list_t a) : nat =
+  match ls with
+  | BetreeListCons _ tl -> 1 + betree_list_len tl
+  | BetreeListNil -> 0
+
+(*
 (** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
 unfold
-let betree_internal_4_flush_decreases (self : betree_internal_t)
+let betree_internal_flush_decreases (self : betree_internal_t)
   (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
   admit ()
 
 (** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
 unfold
-let betree_node_5_apply_messages_decreases (self : betree_node_t)
+let betree_node_apply_messages_decreases (self : betree_node_t)
   (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
   admit ()
-
-(** [betree_main::betree::Node::{5}::apply]: decreases clause *)
-unfold
-let betree_node_5_apply_decreases (self : betree_node_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (key : u64) (new_msg : betree_message_t) (st : state) : nat =
-  admit ()
-
+*)
-- 
cgit v1.2.3