From 6db835db88c4bcf0e00ce1a7a6bc396382b393c3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 11 Nov 2022 21:34:29 +0100
Subject: Reorganize the project to prepare for new backends

---
 .../BetreeMain.Clauses.Template.fst                | 106 ---------------------
 1 file changed, 106 deletions(-)
 delete mode 100644 tests/betree_back_stateful/BetreeMain.Clauses.Template.fst

(limited to 'tests/betree_back_stateful/BetreeMain.Clauses.Template.fst')

diff --git a/tests/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/betree_back_stateful/BetreeMain.Clauses.Template.fst
deleted file mode 100644
index d48213d3..00000000
--- a/tests/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ /dev/null
@@ -1,106 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: templates for the decreases clauses *)
-module BetreeMain.Clauses.Template
-open Primitives
-open BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::num::u64::{10}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
-(** [betree_main::betree::List::{1}::len]: decreases clause *)
-unfold
-let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : nat =
-  admit ()
-
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
-unfold
-let betree_list_split_at_decreases (t : Type0) (self : betree_list_t t)
-  (n : u64) : nat =
-  admit ()
-
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
-unfold
-let betree_list_partition_at_pivot_decreases (t : Type0)
-  (self : betree_list_t (u64 & t)) (pivot : u64) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
-unfold
-let betree_node_lookup_first_message_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [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) (st : state) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
-unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
-  (st : state) : nat =
-  admit ()
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
-unfold
-let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
-  (key : u64) (st : state) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_mut_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
-unfold
-let betree_node_apply_messages_to_leaf_decreases
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
-unfold
-let betree_node_filter_messages_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
-unfold
-let betree_node_lookup_first_message_after_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases clause *)
-unfold
-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)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
-unfold
-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::Internal::{4}::flush]: decreases clause *)
-unfold
-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 ()
-
-- 
cgit v1.2.3