From 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 09:37:31 +0100 Subject: Update the generation of files for external definitions and regenerate the tests --- tests/fstar/betree/BetreeMain.Funs.fst | 2 +- tests/fstar/betree/BetreeMain.FunsExternal.fsti | 35 +++++++++++++++++++++++++ tests/fstar/betree/BetreeMain.Opaque.fsti | 35 ------------------------- 3 files changed, 36 insertions(+), 36 deletions(-) create mode 100644 tests/fstar/betree/BetreeMain.FunsExternal.fsti delete mode 100644 tests/fstar/betree/BetreeMain.Opaque.fsti (limited to 'tests/fstar/betree') diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 537ec32e..fef8a8e1 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -3,7 +3,7 @@ module BetreeMain.Funs open Primitives include BetreeMain.Types -include BetreeMain.Opaque +include BetreeMain.FunsExternal include BetreeMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti new file mode 100644 index 00000000..cd2f956f --- /dev/null +++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti @@ -0,0 +1,35 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external function declarations *) +module BetreeMain.FunsExternal +open Primitives +include BetreeMain.Types + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [betree_main::betree_utils::load_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 98:0-98:63 *) +val betree_utils_load_internal_node + : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t))) + +(** [betree_main::betree_utils::store_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 115:0-115:71 *) +val betree_utils_store_internal_node + : + u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state & + unit) + +(** [betree_main::betree_utils::load_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 132:0-132:55 *) +val betree_utils_load_leaf_node + : u64 -> state -> result (state & (betree_List_t (u64 & u64))) + +(** [betree_main::betree_utils::store_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 145:0-145:63 *) +val betree_utils_store_leaf_node + : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) + +(** [core::option::{core::option::Option}::unwrap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) +val core_option_Option_unwrap + (t : Type0) : option t -> state -> result (state & t) + diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti deleted file mode 100644 index b89c8718..00000000 --- a/tests/fstar/betree/BetreeMain.Opaque.fsti +++ /dev/null @@ -1,35 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external function declarations *) -module BetreeMain.Opaque -open Primitives -include BetreeMain.Types - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [betree_main::betree_utils::load_internal_node]: forward function - Source: 'src/betree_utils.rs', lines 98:0-98:63 *) -val betree_utils_load_internal_node - : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t))) - -(** [betree_main::betree_utils::store_internal_node]: forward function - Source: 'src/betree_utils.rs', lines 115:0-115:71 *) -val betree_utils_store_internal_node - : - u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state & - unit) - -(** [betree_main::betree_utils::load_leaf_node]: forward function - Source: 'src/betree_utils.rs', lines 132:0-132:55 *) -val betree_utils_load_leaf_node - : u64 -> state -> result (state & (betree_List_t (u64 & u64))) - -(** [betree_main::betree_utils::store_leaf_node]: forward function - Source: 'src/betree_utils.rs', lines 145:0-145:63 *) -val betree_utils_store_leaf_node - : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) - -(** [core::option::{core::option::Option}::unwrap]: forward function - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) -val core_option_Option_unwrap - (t : Type0) : option t -> state -> result (state & t) - -- cgit v1.2.3 From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 10:29:25 +0100 Subject: Generate a dedicated file for the external types --- tests/fstar/betree/BetreeMain.Types.fst | 61 +++++++++++++++++++++++ tests/fstar/betree/BetreeMain.Types.fsti | 63 ------------------------ tests/fstar/betree/BetreeMain.TypesExternal.fsti | 10 ++++ 3 files changed, 71 insertions(+), 63 deletions(-) create mode 100644 tests/fstar/betree/BetreeMain.Types.fst delete mode 100644 tests/fstar/betree/BetreeMain.Types.fsti create mode 100644 tests/fstar/betree/BetreeMain.TypesExternal.fsti (limited to 'tests/fstar/betree') diff --git a/tests/fstar/betree/BetreeMain.Types.fst b/tests/fstar/betree/BetreeMain.Types.fst new file mode 100644 index 00000000..b87219b2 --- /dev/null +++ b/tests/fstar/betree/BetreeMain.Types.fst @@ -0,0 +1,61 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: type definitions *) +module BetreeMain.Types +open Primitives +include BetreeMain.TypesExternal + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [betree_main::betree::List] + Source: 'src/betree.rs', lines 17:0-17:23 *) +type betree_List_t (t : Type0) = +| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t +| Betree_List_Nil : betree_List_t t + +(** [betree_main::betree::UpsertFunState] + Source: 'src/betree.rs', lines 63:0-63:23 *) +type betree_UpsertFunState_t = +| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t +| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t + +(** [betree_main::betree::Message] + Source: 'src/betree.rs', lines 69:0-69:23 *) +type betree_Message_t = +| Betree_Message_Insert : u64 -> betree_Message_t +| Betree_Message_Delete : betree_Message_t +| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t + +(** [betree_main::betree::Leaf] + Source: 'src/betree.rs', lines 167:0-167:11 *) +type betree_Leaf_t = { id : u64; size : u64; } + +(** [betree_main::betree::Internal] + Source: 'src/betree.rs', lines 156:0-156:15 *) +type betree_Internal_t = +{ + id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t; +} + +(** [betree_main::betree::Node] + Source: 'src/betree.rs', lines 179:0-179:9 *) +and betree_Node_t = +| Betree_Node_Internal : betree_Internal_t -> betree_Node_t +| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t + +(** [betree_main::betree::Params] + Source: 'src/betree.rs', lines 187:0-187:13 *) +type betree_Params_t = { min_flush_size : u64; split_size : u64; } + +(** [betree_main::betree::NodeIdCounter] + Source: 'src/betree.rs', lines 201:0-201:20 *) +type betree_NodeIdCounter_t = { next_node_id : u64; } + +(** [betree_main::betree::BeTree] + Source: 'src/betree.rs', lines 218:0-218:17 *) +type betree_BeTree_t = +{ + params : betree_Params_t; + node_id_cnt : betree_NodeIdCounter_t; + root : betree_Node_t; +} + diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti deleted file mode 100644 index a098ec19..00000000 --- a/tests/fstar/betree/BetreeMain.Types.fsti +++ /dev/null @@ -1,63 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) -module BetreeMain.Types -open Primitives - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [betree_main::betree::List] - Source: 'src/betree.rs', lines 17:0-17:23 *) -type betree_List_t (t : Type0) = -| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t -| Betree_List_Nil : betree_List_t t - -(** [betree_main::betree::UpsertFunState] - Source: 'src/betree.rs', lines 63:0-63:23 *) -type betree_UpsertFunState_t = -| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t -| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t - -(** [betree_main::betree::Message] - Source: 'src/betree.rs', lines 69:0-69:23 *) -type betree_Message_t = -| Betree_Message_Insert : u64 -> betree_Message_t -| Betree_Message_Delete : betree_Message_t -| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t - -(** [betree_main::betree::Leaf] - Source: 'src/betree.rs', lines 167:0-167:11 *) -type betree_Leaf_t = { id : u64; size : u64; } - -(** [betree_main::betree::Internal] - Source: 'src/betree.rs', lines 156:0-156:15 *) -type betree_Internal_t = -{ - id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t; -} - -(** [betree_main::betree::Node] - Source: 'src/betree.rs', lines 179:0-179:9 *) -and betree_Node_t = -| Betree_Node_Internal : betree_Internal_t -> betree_Node_t -| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t - -(** [betree_main::betree::Params] - Source: 'src/betree.rs', lines 187:0-187:13 *) -type betree_Params_t = { min_flush_size : u64; split_size : u64; } - -(** [betree_main::betree::NodeIdCounter] - Source: 'src/betree.rs', lines 201:0-201:20 *) -type betree_NodeIdCounter_t = { next_node_id : u64; } - -(** [betree_main::betree::BeTree] - Source: 'src/betree.rs', lines 218:0-218:17 *) -type betree_BeTree_t = -{ - params : betree_Params_t; - node_id_cnt : betree_NodeIdCounter_t; - root : betree_Node_t; -} - -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/BetreeMain.TypesExternal.fsti new file mode 100644 index 00000000..1b2c53a6 --- /dev/null +++ b/tests/fstar/betree/BetreeMain.TypesExternal.fsti @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external type declarations *) +module BetreeMain.TypesExternal +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** The state type used in the state-error monad *) +val state : Type0 + -- cgit v1.2.3