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/fstar/betree/BetreeMain.FunsExternal.fsti | 6 ------ 1 file changed, 6 deletions(-) (limited to 'tests/fstar/betree') 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}::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) - -- 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/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 ++++++ 4 files changed, 18 insertions(+), 12 deletions(-) (limited to 'tests/fstar/betree') 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}::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] -- 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(-) (limited to 'tests/fstar/betree') 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 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(-) (limited to 'tests/fstar/betree') 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 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'tests/fstar/betree') 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 -- cgit v1.2.3