summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorSon HO2024-04-26 10:55:47 +0200
committerGitHub2024-04-26 10:55:47 +0200
commit5da597289c1723aa59bf87ad5075675820c18f73 (patch)
treed63e2f44c75634674a3e4eabb57ff08c0ae441ac /tests/fstar
parent2df6dd65b84a2fd9aad4f716f323bf3f85bf82db (diff)
parentfe8d14cd8b7ba907d5248d574619e93e6d1d253a (diff)
Merge pull request #125 from zhassan-aws/core-option-unwrap
Add `core::option::unwrap` builtin
Diffstat (limited to 'tests/fstar')
-rw-r--r--tests/fstar/arrays/Primitives.fst6
-rw-r--r--tests/fstar/betree/BetreeMain.Clauses.Template.fst2
-rw-r--r--tests/fstar/betree/BetreeMain.Clauses.fst2
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst20
-rw-r--r--tests/fstar/betree/BetreeMain.FunsExternal.fsti6
-rw-r--r--tests/fstar/betree/Primitives.fst6
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst2
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst2
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst20
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti6
-rw-r--r--tests/fstar/betree_back_stateful/Primitives.fst6
-rw-r--r--tests/fstar/demo/Primitives.fst6
-rw-r--r--tests/fstar/hashmap/Primitives.fst6
-rw-r--r--tests/fstar/hashmap_on_disk/Primitives.fst6
-rw-r--r--tests/fstar/misc/Primitives.fst6
-rw-r--r--tests/fstar/traits/Primitives.fst6
16 files changed, 72 insertions, 36 deletions
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/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/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.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 *)
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/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/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]