summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--README.md41
-rw-r--r--compiler/Driver.ml8
-rw-r--r--compiler/Interpreter.ml16
-rw-r--r--compiler/PrePasses.ml4
-rw-r--r--compiler/Translate.ml11
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v516
-rw-r--r--tests/coq/betree/BetreeMain_Types.v12
-rw-r--r--tests/coq/misc/NoNestedBorrows.v18
-rw-r--r--tests/fstar/betree/BetreeMain.Clauses.Template.fst46
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst434
-rw-r--r--tests/fstar/betree/BetreeMain.Types.fsti12
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst46
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst556
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Types.fsti12
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst12
-rw-r--r--tests/hol4/betree/betreeMain_FunsScript.sml516
-rw-r--r--tests/hol4/betree/betreeMain_TypesScript.sml12
-rw-r--r--tests/hol4/betree/betreeMain_TypesTheory.sig140
-rw-r--r--tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml8
-rw-r--r--tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig158
-rw-r--r--tests/lean/BetreeMain/Funs.lean412
-rw-r--r--tests/lean/BetreeMain/Types.lean8
-rw-r--r--tests/lean/NoNestedBorrows.lean10
23 files changed, 1513 insertions, 1495 deletions
diff --git a/README.md b/README.md
index 3acba834..31dc74f4 100644
--- a/README.md
+++ b/README.md
@@ -13,24 +13,18 @@ Wall in Pompei, digital image from Michael Lahanis.
Aeneas is a verification toolchain for Rust programs. It relies on a translation from Rusts's MIR
internal language to a pure lamdba calculus. It is intended to be used in combination with
-[Charon](https://github.com/Kachoc/charon), which compiles Rust programs to an intermediate
-representation called LLBC. It currently has backends for the [F\*](https://www.fstar-lang.org)
-theorem prover and the [Coq](https://coq.inria.fr/) proof assistant, and we intend to add
-backends for other provers such as [HOL4](https://hol-theorem-prover.org/) or [LEAN](https://leanprover.github.io/).
+[Charon](https://github.com/AeneasVerif/charon), which compiles Rust programs to an intermediate
+representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org),
+[Coq](https://coq.inria.fr/), [HOL4](https://hol-theorem-prover.org/) and [LEAN](https://leanprover.github.io/).
## Project Structure
- `src`: the OCaml sources. Note that we rely on [Dune](https://github.com/ocaml/dune)
to build the project.
-- `fstar`: F\* files providing basic definitions and notations for the
- generated code (basic definitions for arithmetic types and operations,
- collections like vectors, etc.).
+- `backends`: standard libraries for the existing backends (definitions for
+ arithmetic operations, for standard collections like vectors, theorems, tactics, etc.)
- `tests`: files generated by applying Aeneas on some of the test files of Charon,
completed with hand-written files (proof scripts, mostly).
-- `rust-tests`: miscelleanous files, to test the semantics of Rust or generate
- code in a one-shot manner (mostly used for the arithmetic definitions, for
- instance to generate `MIN` and `MAX` constants for all the integer types
- supported by Rust).
## Installation & Build
@@ -83,27 +77,34 @@ to display a detailed documentation.
## Targeted Subset And Current Limitations
-We target **safe** Rust.
+We target **safe** Rust. This means we have no support for unsafe Rust, though we plan to
+design a mechanism to allow using Aeneas in combination with tools targeting unsafe Rust.
We have the following limitations, that we plan to address one by one:
-- **no loops**: ongoing work. We are currently working on a "join" operation on
- environments to address this issue.
-- **no functions pointers/closures/traits**: ongoing work.
+- **loops**: no nested loops for now. We are working on lifting this limitation.
+- **no functions pointers/closures/traits**: ongoing work. We are actively working on this
+ and plan to have support soon.
- **limited type parametricity**: it is not possible for now to instantiate a type
parameter with a type containing a borrow. This is mostly an engineering
issue. We intend to quickly address the issue for types (i.e., allow `Option<&mut T>`),
and later address it for functions (i.e., allow `f<&mut T>` - we consider this to
be less urgent).
- **no nested borrows in function signatures**: ongoing work.
-- **no interior mutability**: long-term effort. Interior mutability introduces
- true aliasing: we will probably have to use a low-level memory model to address
- this issue.
- Note that interior mutability is truely necessary for concurrent execution (it
- is exploited to implement the synchronisation primitives).
+- **interior mutability**: ongoing work. We are thinking of modeling the effects of
+ interior mutability by using ghost states.
- **no concurrent execution**: long-term effort. We plan to address coarse-grained
parallelism as a long-term goal.
+## Backend Support
+
+We currently support F\*, Coq, HOL4 and Lean. We would be interested in having an Isabelle
+backend. Our most mature backends are Lean and HOL4, for which we have in particular
+support for partial functions and extrinsic proofs of termination (see
+`./backends/lean/Base/Diverge/Elab.lean` and `./backends/hol4/divDefLib.sig` for instance)
+and tactics specialized for monadic programs (see
+`./backends/lean/Base/Progress/Progress.lean` and `./backends/hol4/primitivesLib.sml`).
+
## Formalization
The translation has been formalized and published at ICFP2022: [Aeneas: Rust
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index d819768b..b646a53d 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -214,7 +214,9 @@ let () =
(* Print a warning if the crate contains loops (loops are experimental for now) *)
let has_loops =
- List.exists Aeneas.LlbcAstUtils.fun_decl_has_loops m.functions
+ A.FunDeclId.Map.exists
+ (fun _ -> Aeneas.LlbcAstUtils.fun_decl_has_loops)
+ m.functions
in
if has_loops then log#lwarning (lazy "Support for loops is experimental");
@@ -222,7 +224,9 @@ let () =
whenever there are opaque functions *)
if
!backend = Lean
- && List.exists (fun (d : A.fun_decl) -> d.body = None) m.functions
+ && A.FunDeclId.Map.exists
+ (fun _ (d : A.fun_decl) -> d.body = None)
+ m.functions
&& not !split_files
then (
log#error
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 449463c8..154c5a21 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -15,7 +15,9 @@ let log = L.interpreter_log
let compute_type_fun_global_contexts (m : A.crate) :
C.type_context * C.fun_context * C.global_context =
let type_decls_list, _, _ = split_declarations m.declarations in
- let type_decls, fun_decls, global_decls = compute_defs_maps m in
+ let type_decls = m.types in
+ let fun_decls = m.functions in
+ let global_decls = m.globals in
let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
split_declarations_to_group_maps m.declarations
in
@@ -488,7 +490,7 @@ module Test = struct
*)
let test_unit_function (crate : A.crate) (fid : A.FunDeclId.id) : unit =
(* Retrieve the function declaration *)
- let fdef = A.FunDeclId.nth crate.functions fid in
+ let fdef = A.FunDeclId.Map.find fid crate.functions in
let body = Option.get fdef.body in
(* Debug *)
@@ -541,11 +543,15 @@ module Test = struct
(** Test all the unit functions in a list of function definitions *)
let test_unit_functions (crate : A.crate) : unit =
- let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
- let test_unit_fun (def : A.fun_decl) : unit =
+ let unit_funs =
+ A.FunDeclId.Map.filter
+ (fun _ -> fun_decl_is_transparent_unit)
+ crate.functions
+ in
+ let test_unit_fun _ (def : A.fun_decl) : unit =
test_unit_function crate def.A.def_id
in
- List.iter test_unit_fun unit_funs
+ A.FunDeclId.Map.iter test_unit_fun unit_funs
(** Execute the symbolic interpreter on a function. *)
let test_function_symbolic (synthesize : bool) (type_context : C.type_context)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 8b193ee2..b348ba1d 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -426,7 +426,9 @@ let remove_shallow_borrows (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
let apply_passes (crate : A.crate) : A.crate =
let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
let functions =
- List.fold_left (fun fl pass -> List.map pass fl) crate.functions passes
+ List.fold_left
+ (fun fl pass -> A.FunDeclId.Map.map pass fl)
+ crate.functions passes
in
let crate = { crate with functions } in
log#ldebug
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 6c6435c5..70ef5e3d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -291,7 +291,9 @@ let translate_crate_to_pure (crate : A.crate) :
let trans_ctx = { type_context; fun_context; global_context } in
(* Translate all the type definitions *)
- let type_decls = SymbolicToPure.translate_type_decls crate.types in
+ let type_decls =
+ SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types)
+ in
(* Compute the type definition map *)
let type_decls_map =
@@ -318,7 +320,7 @@ let translate_crate_to_pure (crate : A.crate) :
(LlbcAstUtils.fun_body_get_input_vars body)
in
(A.Regular fdef.def_id, input_names, fdef.signature))
- crate.functions
+ (A.FunDeclId.Map.values crate.functions)
in
let sigs = List.append assumed_sigs local_sigs in
let fun_sigs =
@@ -330,7 +332,7 @@ let translate_crate_to_pure (crate : A.crate) :
let pure_translations =
List.map
(translate_function_to_pure trans_ctx fun_sigs type_decls_map)
- crate.functions
+ (A.FunDeclId.Map.values crate.functions)
in
(* Apply the micro-passes *)
@@ -989,7 +991,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
in
let ctx =
- List.fold_left Extract.extract_global_decl_register_names ctx crate.globals
+ List.fold_left Extract.extract_global_decl_register_names ctx
+ (A.GlobalDeclId.Map.values crate.globals)
in
(* Open the output file *)
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 85aecfc8..e15085ff 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -260,28 +260,6 @@ Definition betree_leaf_split_back
betree_node_id_counter_fresh_id_back node_id_cnt0
.
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-Fixpoint betree_node_lookup_in_bindings_fwd
- (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
- result (option u64)
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match bindings with
- | BetreeListCons hd tl =>
- let (i, i0) := hd in
- if i s= key
- then Return (Some i0)
- else
- if i s> key
- then Return None
- else betree_node_lookup_in_bindings_fwd n0 key tl
- | BetreeListNil => Return None
- end
- end
-.
-
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
Fixpoint betree_node_lookup_first_message_for_key_fwd
(n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
@@ -386,8 +364,62 @@ Fixpoint betree_node_apply_upserts_back
end
.
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+Fixpoint betree_node_lookup_in_bindings_fwd
+ (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
+ result (option u64)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match bindings with
+ | BetreeListCons hd tl =>
+ let (i, i0) := hd in
+ if i s= key
+ then Return (Some i0)
+ else
+ if i s> key
+ then Return None
+ else betree_node_lookup_in_bindings_fwd n0 key tl
+ | BetreeListNil => Return None
+ end
+ end
+.
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+Fixpoint betree_internal_lookup_in_children_fwd
+ (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
+ result (state * (option u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ if key s< self.(Betree_internal_pivot)
+ then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
+ else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
+ end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+with betree_internal_lookup_in_children_back
+ (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
+ result Betree_internal_t
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ if key s< self.(Betree_internal_pivot)
+ then (
+ n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
+ else (
+ n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
+ end
+
(** [betree_main::betree::Node::{5}::lookup]: forward function *)
-Fixpoint betree_node_lookup_fwd
+with betree_node_lookup_fwd
(n : nat) (self : Betree_node_t) (key : u64) (st : state) :
result (state * (option u64))
:=
@@ -526,144 +558,6 @@ with betree_node_lookup_back
Return (BetreeNodeLeaf node)
end
end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-with betree_internal_lookup_in_children_fwd
- (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
- result (state * (option u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- if key s< self.(Betree_internal_pivot)
- then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
- else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
- end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-with betree_internal_lookup_in_children_back
- (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
- result Betree_internal_t
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- if key s< self.(Betree_internal_pivot)
- then (
- n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
- else (
- n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
- end
-.
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-Fixpoint betree_node_lookup_mut_in_bindings_fwd
- (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
- result (Betree_list_t (u64 * u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match bindings with
- | BetreeListCons hd tl =>
- let (i, i0) := hd in
- if i s>= key
- then Return (BetreeListCons (i, i0) tl)
- else betree_node_lookup_mut_in_bindings_fwd n0 key tl
- | BetreeListNil => Return BetreeListNil
- end
- end
-.
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-Fixpoint betree_node_lookup_mut_in_bindings_back
- (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64))
- (ret : Betree_list_t (u64 * u64)) :
- result (Betree_list_t (u64 * u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match bindings with
- | BetreeListCons hd tl =>
- let (i, i0) := hd in
- if i s>= key
- then Return ret
- else (
- tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
- Return (BetreeListCons (i, i0) tl0))
- | BetreeListNil => Return ret
- end
- end
-.
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
-Definition betree_node_apply_to_leaf_fwd_back
- (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64)
- (new_msg : Betree_message_t) :
- result (Betree_list_t (u64 * u64))
- :=
- bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
- b <- betree_list_head_has_key_fwd u64 bindings0 key;
- if b
- then (
- hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
- match new_msg with
- | BetreeMessageInsert v =>
- bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
- bindings2 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings2
- | BetreeMessageDelete =>
- bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1
- | BetreeMessageUpsert s =>
- let (_, i) := hd in
- v <- betree_upsert_update_fwd (Some i) s;
- bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
- bindings2 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings2
- end)
- else
- match new_msg with
- | BetreeMessageInsert v =>
- bindings1 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1
- | BetreeMessageDelete =>
- betree_node_lookup_mut_in_bindings_back n key bindings bindings0
- | BetreeMessageUpsert s =>
- v <- betree_upsert_update_fwd None s;
- bindings1 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1
- end
-.
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
-Fixpoint betree_node_apply_messages_to_leaf_fwd_back
- (n : nat) (bindings : Betree_list_t (u64 * u64))
- (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
- result (Betree_list_t (u64 * u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match new_msgs with
- | BetreeListCons new_msg new_msgs_tl =>
- let (i, m) := new_msg in
- bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
- betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
- | BetreeListNil => Return bindings
- end
- end
.
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
@@ -811,8 +705,210 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
end
.
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+Fixpoint betree_node_lookup_mut_in_bindings_fwd
+ (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match bindings with
+ | BetreeListCons hd tl =>
+ let (i, i0) := hd in
+ if i s>= key
+ then Return (BetreeListCons (i, i0) tl)
+ else betree_node_lookup_mut_in_bindings_fwd n0 key tl
+ | BetreeListNil => Return BetreeListNil
+ end
+ end
+.
+
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+Fixpoint betree_node_lookup_mut_in_bindings_back
+ (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64))
+ (ret : Betree_list_t (u64 * u64)) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match bindings with
+ | BetreeListCons hd tl =>
+ let (i, i0) := hd in
+ if i s>= key
+ then Return ret
+ else (
+ tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
+ Return (BetreeListCons (i, i0) tl0))
+ | BetreeListNil => Return ret
+ end
+ end
+.
+
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+Definition betree_node_apply_to_leaf_fwd_back
+ (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64)
+ (new_msg : Betree_message_t) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
+ b <- betree_list_head_has_key_fwd u64 bindings0 key;
+ if b
+ then (
+ hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
+ match new_msg with
+ | BetreeMessageInsert v =>
+ bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+ bindings2 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+ | BetreeMessageDelete =>
+ bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+ | BetreeMessageUpsert s =>
+ let (_, i) := hd in
+ v <- betree_upsert_update_fwd (Some i) s;
+ bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+ bindings2 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+ end)
+ else
+ match new_msg with
+ | BetreeMessageInsert v =>
+ bindings1 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+ | BetreeMessageDelete =>
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings0
+ | BetreeMessageUpsert s =>
+ v <- betree_upsert_update_fwd None s;
+ bindings1 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+ end
+.
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+Fixpoint betree_node_apply_messages_to_leaf_fwd_back
+ (n : nat) (bindings : Betree_list_t (u64 * u64))
+ (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match new_msgs with
+ | BetreeListCons new_msg new_msgs_tl =>
+ let (i, m) := new_msg in
+ bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
+ betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
+ | BetreeListNil => Return bindings
+ end
+ end
+.
+
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+Fixpoint betree_internal_flush_fwd
+ (n : nat) (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) :
+ result (state * (Betree_list_t (u64 * Betree_message_t)))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ p <-
+ betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+ self.(Betree_internal_pivot);
+ let (msgs_left, msgs_right) := p in
+ len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+ if len_left s>= params.(Betree_params_min_flush_size)
+ then (
+ p0 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (st0, _) := p0 in
+ p1 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (_, node_id_cnt0) := p1 in
+ len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+ if len_right s>= params.(Betree_params_min_flush_size)
+ then (
+ p2 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+ node_id_cnt0 msgs_right st0;
+ let (st1, _) := p2 in
+ _ <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right)
+ params node_id_cnt0 msgs_right st0;
+ Return (st1, BetreeListNil))
+ else Return (st0, msgs_right))
+ else (
+ p0 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+ node_id_cnt msgs_right st;
+ let (st0, _) := p0 in
+ _ <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+ node_id_cnt msgs_right st;
+ Return (st0, msgs_left))
+ end
+
+(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+with betree_internal_flush_back
+ (n : nat) (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) :
+ result (Betree_internal_t * Betree_node_id_counter_t)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ p <-
+ betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+ self.(Betree_internal_pivot);
+ let (msgs_left, msgs_right) := p in
+ len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+ if len_left s>= params.(Betree_params_min_flush_size)
+ then (
+ p0 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (st0, _) := p0 in
+ p1 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (n1, node_id_cnt0) := p1 in
+ len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+ if len_right s>= params.(Betree_params_min_flush_size)
+ then (
+ p2 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right)
+ params node_id_cnt0 msgs_right st0;
+ let (n2, node_id_cnt1) := p2 in
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
+ else
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
+ node_id_cnt0))
+ else (
+ p0 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+ node_id_cnt msgs_right st;
+ let (n1, node_id_cnt0) := p0 in
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
+ node_id_cnt0))
+ end
+
(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-Fixpoint betree_node_apply_messages_fwd
+with betree_node_apply_messages_fwd
(n : nat) (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) :
@@ -922,102 +1018,6 @@ with betree_node_apply_messages_back
|}, node_id_cnt))
end
end
-
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
-with betree_internal_flush_fwd
- (n : nat) (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) :
- result (state * (Betree_list_t (u64 * Betree_message_t)))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- p <-
- betree_list_partition_at_pivot_fwd Betree_message_t n0 content
- self.(Betree_internal_pivot);
- let (msgs_left, msgs_right) := p in
- len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
- if len_left s>= params.(Betree_params_min_flush_size)
- then (
- p0 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (st0, _) := p0 in
- p1 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (_, node_id_cnt0) := p1 in
- len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
- if len_right s>= params.(Betree_params_min_flush_size)
- then (
- p2 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
- node_id_cnt0 msgs_right st0;
- let (st1, _) := p2 in
- _ <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right)
- params node_id_cnt0 msgs_right st0;
- Return (st1, BetreeListNil))
- else Return (st0, msgs_right))
- else (
- p0 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
- node_id_cnt msgs_right st;
- let (st0, _) := p0 in
- _ <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right) params
- node_id_cnt msgs_right st;
- Return (st0, msgs_left))
- end
-
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
-with betree_internal_flush_back
- (n : nat) (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) :
- result (Betree_internal_t * Betree_node_id_counter_t)
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- p <-
- betree_list_partition_at_pivot_fwd Betree_message_t n0 content
- self.(Betree_internal_pivot);
- let (msgs_left, msgs_right) := p in
- len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
- if len_left s>= params.(Betree_params_min_flush_size)
- then (
- p0 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (st0, _) := p0 in
- p1 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (n1, node_id_cnt0) := p1 in
- len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
- if len_right s>= params.(Betree_params_min_flush_size)
- then (
- p2 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right)
- params node_id_cnt0 msgs_right st0;
- let (n2, node_id_cnt1) := p2 in
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
- else
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
- node_id_cnt0))
- else (
- p0 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right) params
- node_id_cnt msgs_right st;
- let (n1, node_id_cnt0) := p0 in
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
- node_id_cnt0))
- end
.
(** [betree_main::betree::Node::{5}::apply]: forward function *)
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index c8af54cd..4a4e75aa 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -37,19 +37,19 @@ mkBetree_leaf_t {
}
.
-(** [betree_main::betree::Node] *)
-Inductive Betree_node_t :=
-| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
-| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
-
(** [betree_main::betree::Internal] *)
-with Betree_internal_t :=
+Inductive Betree_internal_t :=
| mkBetree_internal_t :
u64 ->
u64 ->
Betree_node_t ->
Betree_node_t ->
Betree_internal_t
+
+(** [betree_main::betree::Node] *)
+with Betree_node_t :=
+| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
+| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
.
Definition Betree_internal_id (x : Betree_internal_t) :=
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index f93254e1..c1c24e00 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -238,23 +238,23 @@ Definition test_char_fwd : result char :=
Return (char_of_byte Coq.Init.Byte.x61)
.
-(** [no_nested_borrows::NodeElem] *)
-Inductive Node_elem_t (T : Type) :=
-| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
-| NodeElemNil : Node_elem_t T
-
(** [no_nested_borrows::Tree] *)
-with Tree_t (T : Type) :=
+Inductive Tree_t (T : Type) :=
| TreeLeaf : T -> Tree_t T
| TreeNode : T -> Node_elem_t T -> Tree_t T -> Tree_t T
-.
-Arguments NodeElemCons {T} _ _.
-Arguments NodeElemNil {T}.
+(** [no_nested_borrows::NodeElem] *)
+with Node_elem_t (T : Type) :=
+| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
+| NodeElemNil : Node_elem_t T
+.
Arguments TreeLeaf {T} _.
Arguments TreeNode {T} _ _ _.
+Arguments NodeElemCons {T} _ _.
+Arguments NodeElemNil {T}.
+
(** [no_nested_borrows::list_length]: forward function *)
Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
match l with
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 5a9776ab..823df03a 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -23,12 +23,6 @@ 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)
@@ -42,10 +36,10 @@ let betree_node_apply_upserts_decreases
(key : u64) (st : state) : nat =
admit ()
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
- (st : state) : nat =
+let betree_node_lookup_in_bindings_decreases (key : u64)
+ (bindings : betree_list_t (u64 & u64)) : nat =
admit ()
(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
@@ -54,17 +48,10 @@ 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 *)
+(** [betree_main::betree::Node::{5}::lookup]: 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 =
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
+ (st : state) : nat =
admit ()
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
@@ -86,11 +73,17 @@ let betree_node_apply_messages_to_internal_decreases
(new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
admit ()
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: 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 =
+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::Internal::{4}::flush]: decreases clause *)
@@ -100,3 +93,10 @@ let betree_internal_flush_decreases (self : betree_internal_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_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 ()
+
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index f1bc1191..bd4e37d4 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -222,24 +222,6 @@ let betree_leaf_split_back
let* _ = betree_store_leaf_node_fwd id1 content1 st0 in
betree_node_id_counter_fresh_id_back node_id_cnt0
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-let rec betree_node_lookup_in_bindings_fwd
- (key : u64) (bindings : betree_list_t (u64 & u64)) :
- Tot (result (option u64))
- (decreases (betree_node_lookup_in_bindings_decreases key bindings))
- =
- begin match bindings with
- | BetreeListCons hd tl ->
- let (i, i0) = hd in
- if i = key
- then Return (Some i0)
- else
- if i > key
- then Return None
- else betree_node_lookup_in_bindings_fwd key tl
- | BetreeListNil -> Return None
- end
-
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
let rec betree_node_lookup_first_message_for_key_fwd
(key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
@@ -326,8 +308,50 @@ let rec betree_node_apply_upserts_back
betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
BetreeMessageInsert v)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+let rec betree_node_lookup_in_bindings_fwd
+ (key : u64) (bindings : betree_list_t (u64 & u64)) :
+ Tot (result (option u64))
+ (decreases (betree_node_lookup_in_bindings_decreases key bindings))
+ =
+ begin match bindings with
+ | BetreeListCons hd tl ->
+ let (i, i0) = hd in
+ if i = key
+ then Return (Some i0)
+ else
+ if i > key
+ then Return None
+ else betree_node_lookup_in_bindings_fwd key tl
+ | BetreeListNil -> Return None
+ end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+let rec betree_internal_lookup_in_children_fwd
+ (self : betree_internal_t) (key : u64) (st : state) :
+ Tot (result (state & (option u64)))
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
+ =
+ if key < self.betree_internal_pivot
+ then betree_node_lookup_fwd self.betree_internal_left key st
+ else betree_node_lookup_fwd self.betree_internal_right key st
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+and betree_internal_lookup_in_children_back
+ (self : betree_internal_t) (key : u64) (st : state) :
+ Tot (result betree_internal_t)
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
+ =
+ if key < self.betree_internal_pivot
+ then
+ let* n = betree_node_lookup_back self.betree_internal_left key st in
+ Return { self with betree_internal_left = n }
+ else
+ let* n = betree_node_lookup_back self.betree_internal_right key st in
+ Return { self with betree_internal_right = n }
+
(** [betree_main::betree::Node::{5}::lookup]: forward function *)
-let rec betree_node_lookup_fwd
+and betree_node_lookup_fwd
(self : betree_node_t) (key : u64) (st : state) :
Tot (result (state & (option u64)))
(decreases (betree_node_lookup_decreases self key st))
@@ -451,123 +475,6 @@ and betree_node_lookup_back
Return (BetreeNodeLeaf node)
end
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-and betree_internal_lookup_in_children_fwd
- (self : betree_internal_t) (key : u64) (st : state) :
- Tot (result (state & (option u64)))
- (decreases (betree_internal_lookup_in_children_decreases self key st))
- =
- if key < self.betree_internal_pivot
- then betree_node_lookup_fwd self.betree_internal_left key st
- else betree_node_lookup_fwd self.betree_internal_right key st
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-and betree_internal_lookup_in_children_back
- (self : betree_internal_t) (key : u64) (st : state) :
- Tot (result betree_internal_t)
- (decreases (betree_internal_lookup_in_children_decreases self key st))
- =
- if key < self.betree_internal_pivot
- then
- let* n = betree_node_lookup_back self.betree_internal_left key st in
- Return { self with betree_internal_left = n }
- else
- let* n = betree_node_lookup_back self.betree_internal_right key st in
- Return { self with betree_internal_right = n }
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-let rec betree_node_lookup_mut_in_bindings_fwd
- (key : u64) (bindings : betree_list_t (u64 & u64)) :
- Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
- =
- begin match bindings with
- | BetreeListCons hd tl ->
- let (i, i0) = hd in
- if i >= key
- then Return (BetreeListCons (i, i0) tl)
- else betree_node_lookup_mut_in_bindings_fwd key tl
- | BetreeListNil -> Return BetreeListNil
- end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-let rec betree_node_lookup_mut_in_bindings_back
- (key : u64) (bindings : betree_list_t (u64 & u64))
- (ret : betree_list_t (u64 & u64)) :
- Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
- =
- begin match bindings with
- | BetreeListCons hd tl ->
- let (i, i0) = hd in
- if i >= key
- then Return ret
- else
- let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
- Return (BetreeListCons (i, i0) tl0)
- | BetreeListNil -> Return ret
- end
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
-let betree_node_apply_to_leaf_fwd_back
- (bindings : betree_list_t (u64 & u64)) (key : u64)
- (new_msg : betree_message_t) :
- result (betree_list_t (u64 & u64))
- =
- let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
- let* b = betree_list_head_has_key_fwd u64 bindings0 key in
- if b
- then
- let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
- begin match new_msg with
- | BetreeMessageInsert v ->
- let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
- let* bindings2 =
- betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings2
- | BetreeMessageDelete ->
- let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- | BetreeMessageUpsert s ->
- let (_, i) = hd in
- let* v = betree_upsert_update_fwd (Some i) s in
- let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
- let* bindings2 =
- betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings2
- end
- else
- begin match new_msg with
- | BetreeMessageInsert v ->
- let* bindings1 =
- betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- | BetreeMessageDelete ->
- betree_node_lookup_mut_in_bindings_back key bindings bindings0
- | BetreeMessageUpsert s ->
- let* v = betree_upsert_update_fwd None s in
- let* bindings1 =
- betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
-let rec betree_node_apply_messages_to_leaf_fwd_back
- (bindings : betree_list_t (u64 & u64))
- (new_msgs : betree_list_t (u64 & betree_message_t)) :
- Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
- =
- begin match new_msgs with
- | BetreeListCons new_msg new_msgs_tl ->
- let (i, m) = new_msg in
- let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
- betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
- | BetreeListNil -> Return bindings
- end
-
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
let rec betree_node_filter_messages_for_key_fwd_back
@@ -699,8 +606,181 @@ let rec betree_node_apply_messages_to_internal_fwd_back
| BetreeListNil -> Return msgs
end
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+let rec betree_node_lookup_mut_in_bindings_fwd
+ (key : u64) (bindings : betree_list_t (u64 & u64)) :
+ Tot (result (betree_list_t (u64 & u64)))
+ (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
+ =
+ begin match bindings with
+ | BetreeListCons hd tl ->
+ let (i, i0) = hd in
+ if i >= key
+ then Return (BetreeListCons (i, i0) tl)
+ else betree_node_lookup_mut_in_bindings_fwd key tl
+ | BetreeListNil -> Return BetreeListNil
+ end
+
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+let rec betree_node_lookup_mut_in_bindings_back
+ (key : u64) (bindings : betree_list_t (u64 & u64))
+ (ret : betree_list_t (u64 & u64)) :
+ Tot (result (betree_list_t (u64 & u64)))
+ (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
+ =
+ begin match bindings with
+ | BetreeListCons hd tl ->
+ let (i, i0) = hd in
+ if i >= key
+ then Return ret
+ else
+ let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
+ Return (BetreeListCons (i, i0) tl0)
+ | BetreeListNil -> Return ret
+ end
+
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+let betree_node_apply_to_leaf_fwd_back
+ (bindings : betree_list_t (u64 & u64)) (key : u64)
+ (new_msg : betree_message_t) :
+ result (betree_list_t (u64 & u64))
+ =
+ let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
+ let* b = betree_list_head_has_key_fwd u64 bindings0 key in
+ if b
+ then
+ let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
+ begin match new_msg with
+ | BetreeMessageInsert v ->
+ let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+ let* bindings2 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings2
+ | BetreeMessageDelete ->
+ let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ | BetreeMessageUpsert s ->
+ let (_, i) = hd in
+ let* v = betree_upsert_update_fwd (Some i) s in
+ let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+ let* bindings2 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings2
+ end
+ else
+ begin match new_msg with
+ | BetreeMessageInsert v ->
+ let* bindings1 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ | BetreeMessageDelete ->
+ betree_node_lookup_mut_in_bindings_back key bindings bindings0
+ | BetreeMessageUpsert s ->
+ let* v = betree_upsert_update_fwd None s in
+ let* bindings1 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ end
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+let rec betree_node_apply_messages_to_leaf_fwd_back
+ (bindings : betree_list_t (u64 & u64))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) :
+ Tot (result (betree_list_t (u64 & u64)))
+ (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
+ =
+ begin match new_msgs with
+ | BetreeListCons new_msg new_msgs_tl ->
+ let (i, m) = new_msg in
+ let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
+ betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+ | BetreeListNil -> Return bindings
+ end
+
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+let rec betree_internal_flush_fwd
+ (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) :
+ Tot (result (state & (betree_list_t (u64 & betree_message_t))))
+ (decreases (
+ betree_internal_flush_decreases self params node_id_cnt content st))
+ =
+ let* p =
+ betree_list_partition_at_pivot_fwd betree_message_t content
+ self.betree_internal_pivot in
+ let (msgs_left, msgs_right) = p in
+ let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
+ if len_left >= params.betree_params_min_flush_size
+ then
+ let* (st0, _) =
+ betree_node_apply_messages_fwd self.betree_internal_left params
+ node_id_cnt msgs_left st in
+ let* (_, node_id_cnt0) =
+ betree_node_apply_messages_back self.betree_internal_left params
+ node_id_cnt msgs_left st in
+ let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
+ if len_right >= params.betree_params_min_flush_size
+ then
+ let* (st1, _) =
+ betree_node_apply_messages_fwd self.betree_internal_right params
+ node_id_cnt0 msgs_right st0 in
+ let* _ =
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt0 msgs_right st0 in
+ Return (st1, BetreeListNil)
+ else Return (st0, msgs_right)
+ else
+ let* (st0, _) =
+ betree_node_apply_messages_fwd self.betree_internal_right params
+ node_id_cnt msgs_right st in
+ let* _ =
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt msgs_right st in
+ Return (st0, msgs_left)
+
+(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+and betree_internal_flush_back
+ (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) :
+ Tot (result (betree_internal_t & betree_node_id_counter_t))
+ (decreases (
+ betree_internal_flush_decreases self params node_id_cnt content st))
+ =
+ let* p =
+ betree_list_partition_at_pivot_fwd betree_message_t content
+ self.betree_internal_pivot in
+ let (msgs_left, msgs_right) = p in
+ let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
+ if len_left >= params.betree_params_min_flush_size
+ then
+ let* (st0, _) =
+ betree_node_apply_messages_fwd self.betree_internal_left params
+ node_id_cnt msgs_left st in
+ let* (n, node_id_cnt0) =
+ betree_node_apply_messages_back self.betree_internal_left params
+ node_id_cnt msgs_left st in
+ let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
+ if len_right >= params.betree_params_min_flush_size
+ then
+ let* (n0, node_id_cnt1) =
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt0 msgs_right st0 in
+ Return
+ ({ self with betree_internal_left = n; betree_internal_right = n0 },
+ node_id_cnt1)
+ else Return ({ self with betree_internal_left = n }, node_id_cnt0)
+ else
+ let* (n, node_id_cnt0) =
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt msgs_right st in
+ Return ({ self with betree_internal_right = n }, node_id_cnt0)
+
(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-let rec betree_node_apply_messages_fwd
+and betree_node_apply_messages_fwd
(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) :
@@ -794,86 +874,6 @@ and betree_node_apply_messages_back
Return (BetreeNodeLeaf { node with betree_leaf_size = len }, node_id_cnt)
end
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
-and betree_internal_flush_fwd
- (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) :
- Tot (result (state & (betree_list_t (u64 & betree_message_t))))
- (decreases (
- betree_internal_flush_decreases self params node_id_cnt content st))
- =
- let* p =
- betree_list_partition_at_pivot_fwd betree_message_t content
- self.betree_internal_pivot in
- let (msgs_left, msgs_right) = p in
- let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
- if len_left >= params.betree_params_min_flush_size
- then
- let* (st0, _) =
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st in
- let* (_, node_id_cnt0) =
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st in
- let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
- if len_right >= params.betree_params_min_flush_size
- then
- let* (st1, _) =
- betree_node_apply_messages_fwd self.betree_internal_right params
- node_id_cnt0 msgs_right st0 in
- let* _ =
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt0 msgs_right st0 in
- Return (st1, BetreeListNil)
- else Return (st0, msgs_right)
- else
- let* (st0, _) =
- betree_node_apply_messages_fwd self.betree_internal_right params
- node_id_cnt msgs_right st in
- let* _ =
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st in
- Return (st0, msgs_left)
-
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
-and betree_internal_flush_back
- (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) :
- Tot (result (betree_internal_t & betree_node_id_counter_t))
- (decreases (
- betree_internal_flush_decreases self params node_id_cnt content st))
- =
- let* p =
- betree_list_partition_at_pivot_fwd betree_message_t content
- self.betree_internal_pivot in
- let (msgs_left, msgs_right) = p in
- let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
- if len_left >= params.betree_params_min_flush_size
- then
- let* (st0, _) =
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st in
- let* (n, node_id_cnt0) =
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st in
- let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
- if len_right >= params.betree_params_min_flush_size
- then
- let* (n0, node_id_cnt1) =
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt0 msgs_right st0 in
- Return
- ({ self with betree_internal_left = n; betree_internal_right = n0 },
- node_id_cnt1)
- else Return ({ self with betree_internal_left = n }, node_id_cnt0)
- else
- let* (n, node_id_cnt0) =
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st in
- Return ({ self with betree_internal_right = n }, node_id_cnt0)
-
(** [betree_main::betree::Node::{5}::apply]: forward function *)
let betree_node_apply_fwd
(self : betree_node_t) (params : betree_params_t)
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti
index aad9cb43..a937c726 100644
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fsti
@@ -24,13 +24,8 @@ type betree_message_t =
(** [betree_main::betree::Leaf] *)
type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
-(** [betree_main::betree::Node] *)
-type betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
(** [betree_main::betree::Internal] *)
-and betree_internal_t =
+type betree_internal_t =
{
betree_internal_id : u64;
betree_internal_pivot : u64;
@@ -38,6 +33,11 @@ and betree_internal_t =
betree_internal_right : betree_node_t;
}
+(** [betree_main::betree::Node] *)
+and betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
(** [betree_main::betree::Params] *)
type betree_params_t =
{
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 5a9776ab..823df03a 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -23,12 +23,6 @@ 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)
@@ -42,10 +36,10 @@ let betree_node_apply_upserts_decreases
(key : u64) (st : state) : nat =
admit ()
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
- (st : state) : nat =
+let betree_node_lookup_in_bindings_decreases (key : u64)
+ (bindings : betree_list_t (u64 & u64)) : nat =
admit ()
(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
@@ -54,17 +48,10 @@ 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 *)
+(** [betree_main::betree::Node::{5}::lookup]: 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 =
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
+ (st : state) : nat =
admit ()
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
@@ -86,11 +73,17 @@ let betree_node_apply_messages_to_internal_decreases
(new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
admit ()
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: 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 =
+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::Internal::{4}::flush]: decreases clause *)
@@ -100,3 +93,10 @@ let betree_internal_flush_decreases (self : betree_internal_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_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 ()
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 12402fb4..be8ac438 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -261,24 +261,6 @@ let betree_leaf_split_back2
let* node_id_cnt1 = betree_node_id_counter_fresh_id_back node_id_cnt0 in
Return (st0, node_id_cnt1)
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-let rec betree_node_lookup_in_bindings_fwd
- (key : u64) (bindings : betree_list_t (u64 & u64)) :
- Tot (result (option u64))
- (decreases (betree_node_lookup_in_bindings_decreases key bindings))
- =
- begin match bindings with
- | BetreeListCons hd tl ->
- let (i, i0) = hd in
- if i = key
- then Return (Some i0)
- else
- if i > key
- then Return None
- else betree_node_lookup_in_bindings_fwd key tl
- | BetreeListNil -> Return None
- end
-
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
let rec betree_node_lookup_first_message_for_key_fwd
(key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
@@ -367,8 +349,52 @@ let rec betree_node_apply_upserts_back
BetreeMessageInsert v) in
Return (st0, msgs0)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+let rec betree_node_lookup_in_bindings_fwd
+ (key : u64) (bindings : betree_list_t (u64 & u64)) :
+ Tot (result (option u64))
+ (decreases (betree_node_lookup_in_bindings_decreases key bindings))
+ =
+ begin match bindings with
+ | BetreeListCons hd tl ->
+ let (i, i0) = hd in
+ if i = key
+ then Return (Some i0)
+ else
+ if i > key
+ then Return None
+ else betree_node_lookup_in_bindings_fwd key tl
+ | BetreeListNil -> Return None
+ end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+let rec betree_internal_lookup_in_children_fwd
+ (self : betree_internal_t) (key : u64) (st : state) :
+ Tot (result (state & (option u64)))
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
+ =
+ if key < self.betree_internal_pivot
+ then betree_node_lookup_fwd self.betree_internal_left key st
+ else betree_node_lookup_fwd self.betree_internal_right key st
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+and betree_internal_lookup_in_children_back
+ (self : betree_internal_t) (key : u64) (st : state) (st0 : state) :
+ Tot (result (state & betree_internal_t))
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
+ =
+ if key < self.betree_internal_pivot
+ then
+ let* (st1, n) =
+ betree_node_lookup_back self.betree_internal_left key st st0 in
+ Return (st1, { self with betree_internal_left = n })
+ else
+ let* (st1, n) =
+ betree_node_lookup_back self.betree_internal_right key st st0 in
+ Return (st1, { self with betree_internal_right = n })
+
(** [betree_main::betree::Node::{5}::lookup]: forward function *)
-let rec betree_node_lookup_fwd
+and betree_node_lookup_fwd
(self : betree_node_t) (key : u64) (st : state) :
Tot (result (state & (option u64)))
(decreases (betree_node_lookup_decreases self key st))
@@ -496,125 +522,6 @@ and betree_node_lookup_back
Return (st0, BetreeNodeLeaf node)
end
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-and betree_internal_lookup_in_children_fwd
- (self : betree_internal_t) (key : u64) (st : state) :
- Tot (result (state & (option u64)))
- (decreases (betree_internal_lookup_in_children_decreases self key st))
- =
- if key < self.betree_internal_pivot
- then betree_node_lookup_fwd self.betree_internal_left key st
- else betree_node_lookup_fwd self.betree_internal_right key st
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-and betree_internal_lookup_in_children_back
- (self : betree_internal_t) (key : u64) (st : state) (st0 : state) :
- Tot (result (state & betree_internal_t))
- (decreases (betree_internal_lookup_in_children_decreases self key st))
- =
- if key < self.betree_internal_pivot
- then
- let* (st1, n) =
- betree_node_lookup_back self.betree_internal_left key st st0 in
- Return (st1, { self with betree_internal_left = n })
- else
- let* (st1, n) =
- betree_node_lookup_back self.betree_internal_right key st st0 in
- Return (st1, { self with betree_internal_right = n })
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-let rec betree_node_lookup_mut_in_bindings_fwd
- (key : u64) (bindings : betree_list_t (u64 & u64)) :
- Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
- =
- begin match bindings with
- | BetreeListCons hd tl ->
- let (i, i0) = hd in
- if i >= key
- then Return (BetreeListCons (i, i0) tl)
- else betree_node_lookup_mut_in_bindings_fwd key tl
- | BetreeListNil -> Return BetreeListNil
- end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-let rec betree_node_lookup_mut_in_bindings_back
- (key : u64) (bindings : betree_list_t (u64 & u64))
- (ret : betree_list_t (u64 & u64)) :
- Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
- =
- begin match bindings with
- | BetreeListCons hd tl ->
- let (i, i0) = hd in
- if i >= key
- then Return ret
- else
- let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
- Return (BetreeListCons (i, i0) tl0)
- | BetreeListNil -> Return ret
- end
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
-let betree_node_apply_to_leaf_fwd_back
- (bindings : betree_list_t (u64 & u64)) (key : u64)
- (new_msg : betree_message_t) :
- result (betree_list_t (u64 & u64))
- =
- let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
- let* b = betree_list_head_has_key_fwd u64 bindings0 key in
- if b
- then
- let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
- begin match new_msg with
- | BetreeMessageInsert v ->
- let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
- let* bindings2 =
- betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings2
- | BetreeMessageDelete ->
- let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- | BetreeMessageUpsert s ->
- let (_, i) = hd in
- let* v = betree_upsert_update_fwd (Some i) s in
- let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
- let* bindings2 =
- betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings2
- end
- else
- begin match new_msg with
- | BetreeMessageInsert v ->
- let* bindings1 =
- betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- | BetreeMessageDelete ->
- betree_node_lookup_mut_in_bindings_back key bindings bindings0
- | BetreeMessageUpsert s ->
- let* v = betree_upsert_update_fwd None s in
- let* bindings1 =
- betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
-let rec betree_node_apply_messages_to_leaf_fwd_back
- (bindings : betree_list_t (u64 & u64))
- (new_msgs : betree_list_t (u64 & betree_message_t)) :
- Tot (result (betree_list_t (u64 & u64)))
- (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
- =
- begin match new_msgs with
- | BetreeListCons new_msg new_msgs_tl ->
- let (i, m) = new_msg in
- let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
- betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
- | BetreeListNil -> Return bindings
- end
-
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
let rec betree_node_filter_messages_for_key_fwd_back
@@ -746,157 +653,101 @@ let rec betree_node_apply_messages_to_internal_fwd_back
| BetreeListNil -> Return msgs
end
-(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-let rec betree_node_apply_messages_fwd
- (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) :
- Tot (result (state & unit))
- (decreases (
- betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+let rec betree_node_lookup_mut_in_bindings_fwd
+ (key : u64) (bindings : betree_list_t (u64 & u64)) :
+ Tot (result (betree_list_t (u64 & u64)))
+ (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
=
- begin match self with
- | BetreeNodeInternal node ->
- let* (st0, content) =
- betree_load_internal_node_fwd node.betree_internal_id st in
- let* content0 =
- betree_node_apply_messages_to_internal_fwd_back content msgs in
- let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
- if num_msgs >= params.betree_params_min_flush_size
- then
- let* (st1, content1) =
- betree_internal_flush_fwd node params node_id_cnt content0 st0 in
- let* (st2, (node0, _)) =
- betree_internal_flush_back'a node params node_id_cnt content0 st0 st1
- in
- let* (st3, _) =
- betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in
- Return (st3, ())
- else
- let* (st1, _) =
- betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
- Return (st1, ())
- | BetreeNodeLeaf node ->
- let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
- let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
- let* len = betree_list_len_fwd (u64 & u64) content0 in
- let* i = u64_mul 2 params.betree_params_split_size in
- if len >= i
- then
- let* (st1, _) =
- betree_leaf_split_fwd node content0 params node_id_cnt st0 in
- let* (st2, _) =
- betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
- betree_leaf_split_back0 node content0 params node_id_cnt st0 st2
- else
- let* (st1, _) =
- betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
- Return (st1, ())
+ begin match bindings with
+ | BetreeListCons hd tl ->
+ let (i, i0) = hd in
+ if i >= key
+ then Return (BetreeListCons (i, i0) tl)
+ else betree_node_lookup_mut_in_bindings_fwd key tl
+ | BetreeListNil -> Return BetreeListNil
end
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
-and betree_node_apply_messages_back'a
- (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) (st0 : state) :
- Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
- (decreases (
- betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+let rec betree_node_lookup_mut_in_bindings_back
+ (key : u64) (bindings : betree_list_t (u64 & u64))
+ (ret : betree_list_t (u64 & u64)) :
+ Tot (result (betree_list_t (u64 & u64)))
+ (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
=
- begin match self with
- | BetreeNodeInternal node ->
- let* (st1, content) =
- betree_load_internal_node_fwd node.betree_internal_id st in
- let* content0 =
- betree_node_apply_messages_to_internal_fwd_back content msgs in
- let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
- if num_msgs >= params.betree_params_min_flush_size
- then
- let* (st2, content1) =
- betree_internal_flush_fwd node params node_id_cnt content0 st1 in
- let* (st3, (node0, node_id_cnt0)) =
- betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
- in
- let* _ =
- betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
- Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
- else
- let* _ =
- betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
- Return (st0, (BetreeNodeInternal node, node_id_cnt))
- | BetreeNodeLeaf node ->
- let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
- let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
- let* len = betree_list_len_fwd (u64 & u64) content0 in
- let* i = u64_mul 2 params.betree_params_split_size in
- if len >= i
- then
- let* (st2, new_node) =
- betree_leaf_split_fwd node content0 params node_id_cnt st1 in
- let* (st3, _) =
- betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
- let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
- in
- let* (st4, node_id_cnt0) =
- betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in
- Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
+ begin match bindings with
+ | BetreeListCons hd tl ->
+ let (i, i0) = hd in
+ if i >= key
+ then Return ret
else
- let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
- Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len },
- node_id_cnt))
+ let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
+ Return (BetreeListCons (i, i0) tl0)
+ | BetreeListNil -> Return ret
end
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *)
-and betree_node_apply_messages_back1
- (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) (st0 : state) :
- Tot (result (state & unit))
- (decreases (
- betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+let betree_node_apply_to_leaf_fwd_back
+ (bindings : betree_list_t (u64 & u64)) (key : u64)
+ (new_msg : betree_message_t) :
+ result (betree_list_t (u64 & u64))
=
- begin match self with
- | BetreeNodeInternal node ->
- let* (st1, content) =
- betree_load_internal_node_fwd node.betree_internal_id st in
- let* content0 =
- betree_node_apply_messages_to_internal_fwd_back content msgs in
- let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
- if num_msgs >= params.betree_params_min_flush_size
- then
- let* (st2, content1) =
- betree_internal_flush_fwd node params node_id_cnt content0 st1 in
- let* (st3, (node0, _)) =
- betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
- in
- let* _ =
- betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
- betree_internal_flush_back1 node params node_id_cnt content0 st1 st0
- else
- let* _ =
- betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
- Return (st0, ())
- | BetreeNodeLeaf node ->
- let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
- let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
- let* len = betree_list_len_fwd (u64 & u64) content0 in
- let* i = u64_mul 2 params.betree_params_split_size in
- if len >= i
- then
- let* (st2, _) =
- betree_leaf_split_fwd node content0 params node_id_cnt st1 in
- let* (st3, _) =
- betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
- let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
- in
- betree_leaf_split_back1 node content0 params node_id_cnt st1 st0
- else
- let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
- Return (st0, ())
+ let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
+ let* b = betree_list_head_has_key_fwd u64 bindings0 key in
+ if b
+ then
+ let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
+ begin match new_msg with
+ | BetreeMessageInsert v ->
+ let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+ let* bindings2 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings2
+ | BetreeMessageDelete ->
+ let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ | BetreeMessageUpsert s ->
+ let (_, i) = hd in
+ let* v = betree_upsert_update_fwd (Some i) s in
+ let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+ let* bindings2 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings2
+ end
+ else
+ begin match new_msg with
+ | BetreeMessageInsert v ->
+ let* bindings1 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ | BetreeMessageDelete ->
+ betree_node_lookup_mut_in_bindings_back key bindings bindings0
+ | BetreeMessageUpsert s ->
+ let* v = betree_upsert_update_fwd None s in
+ let* bindings1 =
+ betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ end
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+let rec betree_node_apply_messages_to_leaf_fwd_back
+ (bindings : betree_list_t (u64 & u64))
+ (new_msgs : betree_list_t (u64 & betree_message_t)) :
+ Tot (result (betree_list_t (u64 & u64)))
+ (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
+ =
+ begin match new_msgs with
+ | BetreeListCons new_msg new_msgs_tl ->
+ let (i, m) = new_msg in
+ let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
+ betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+ | BetreeListNil -> Return bindings
end
(** [betree_main::betree::Internal::{4}::flush]: forward function *)
-and betree_internal_flush_fwd
+let rec betree_internal_flush_fwd
(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) :
@@ -1052,6 +903,155 @@ and betree_internal_flush_back1
node_id_cnt msgs_right st st2 in
Return (st0, ())
+(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+and betree_node_apply_messages_fwd
+ (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) :
+ Tot (result (state & unit))
+ (decreases (
+ betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+ =
+ begin match self with
+ | BetreeNodeInternal node ->
+ let* (st0, content) =
+ betree_load_internal_node_fwd node.betree_internal_id st in
+ let* content0 =
+ betree_node_apply_messages_to_internal_fwd_back content msgs in
+ let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+ if num_msgs >= params.betree_params_min_flush_size
+ then
+ let* (st1, content1) =
+ betree_internal_flush_fwd node params node_id_cnt content0 st0 in
+ let* (st2, (node0, _)) =
+ betree_internal_flush_back'a node params node_id_cnt content0 st0 st1
+ in
+ let* (st3, _) =
+ betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in
+ Return (st3, ())
+ else
+ let* (st1, _) =
+ betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
+ Return (st1, ())
+ | BetreeNodeLeaf node ->
+ let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+ let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+ let* len = betree_list_len_fwd (u64 & u64) content0 in
+ let* i = u64_mul 2 params.betree_params_split_size in
+ if len >= i
+ then
+ let* (st1, _) =
+ betree_leaf_split_fwd node content0 params node_id_cnt st0 in
+ let* (st2, _) =
+ betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
+ betree_leaf_split_back0 node content0 params node_id_cnt st0 st2
+ else
+ let* (st1, _) =
+ betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
+ Return (st1, ())
+ end
+
+(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+and betree_node_apply_messages_back'a
+ (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) (st0 : state) :
+ Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
+ (decreases (
+ betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+ =
+ begin match self with
+ | BetreeNodeInternal node ->
+ let* (st1, content) =
+ betree_load_internal_node_fwd node.betree_internal_id st in
+ let* content0 =
+ betree_node_apply_messages_to_internal_fwd_back content msgs in
+ let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+ if num_msgs >= params.betree_params_min_flush_size
+ then
+ let* (st2, content1) =
+ betree_internal_flush_fwd node params node_id_cnt content0 st1 in
+ let* (st3, (node0, node_id_cnt0)) =
+ betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
+ in
+ let* _ =
+ betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
+ Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
+ else
+ let* _ =
+ betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+ Return (st0, (BetreeNodeInternal node, node_id_cnt))
+ | BetreeNodeLeaf node ->
+ let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+ let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+ let* len = betree_list_len_fwd (u64 & u64) content0 in
+ let* i = u64_mul 2 params.betree_params_split_size in
+ if len >= i
+ then
+ let* (st2, new_node) =
+ betree_leaf_split_fwd node content0 params node_id_cnt st1 in
+ let* (st3, _) =
+ betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
+ let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
+ in
+ let* (st4, node_id_cnt0) =
+ betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in
+ Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
+ else
+ let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+ Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len },
+ node_id_cnt))
+ end
+
+(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *)
+and betree_node_apply_messages_back1
+ (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) (st0 : state) :
+ Tot (result (state & unit))
+ (decreases (
+ betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+ =
+ begin match self with
+ | BetreeNodeInternal node ->
+ let* (st1, content) =
+ betree_load_internal_node_fwd node.betree_internal_id st in
+ let* content0 =
+ betree_node_apply_messages_to_internal_fwd_back content msgs in
+ let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+ if num_msgs >= params.betree_params_min_flush_size
+ then
+ let* (st2, content1) =
+ betree_internal_flush_fwd node params node_id_cnt content0 st1 in
+ let* (st3, (node0, _)) =
+ betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
+ in
+ let* _ =
+ betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
+ betree_internal_flush_back1 node params node_id_cnt content0 st1 st0
+ else
+ let* _ =
+ betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+ Return (st0, ())
+ | BetreeNodeLeaf node ->
+ let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+ let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+ let* len = betree_list_len_fwd (u64 & u64) content0 in
+ let* i = u64_mul 2 params.betree_params_split_size in
+ if len >= i
+ then
+ let* (st2, _) =
+ betree_leaf_split_fwd node content0 params node_id_cnt st1 in
+ let* (st3, _) =
+ betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
+ let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
+ in
+ betree_leaf_split_back1 node content0 params node_id_cnt st1 st0
+ else
+ let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+ Return (st0, ())
+ end
+
(** [betree_main::betree::Node::{5}::apply]: forward function *)
let betree_node_apply_fwd
(self : betree_node_t) (params : betree_params_t)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
index aad9cb43..a937c726 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
@@ -24,13 +24,8 @@ type betree_message_t =
(** [betree_main::betree::Leaf] *)
type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
-(** [betree_main::betree::Node] *)
-type betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
(** [betree_main::betree::Internal] *)
-and betree_internal_t =
+type betree_internal_t =
{
betree_internal_id : u64;
betree_internal_pivot : u64;
@@ -38,6 +33,11 @@ and betree_internal_t =
betree_internal_right : betree_node_t;
}
+(** [betree_main::betree::Node] *)
+and betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
(** [betree_main::betree::Params] *)
type betree_params_t =
{
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index d790bfa9..2cdd6e21 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -202,16 +202,16 @@ let _ = assert_norm (choose_test_fwd = Return ())
let test_char_fwd : result char =
Return 'a'
-(** [no_nested_borrows::NodeElem] *)
-type node_elem_t (t : Type0) =
-| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
-| NodeElemNil : node_elem_t t
-
(** [no_nested_borrows::Tree] *)
-and tree_t (t : Type0) =
+type tree_t (t : Type0) =
| TreeLeaf : t -> tree_t t
| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
+(** [no_nested_borrows::NodeElem] *)
+and node_elem_t (t : Type0) =
+| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
+| NodeElemNil : node_elem_t t
+
(** [no_nested_borrows::list_length]: forward function *)
let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
begin match l with
diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml
index 03ff2671..b53c7b8d 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betreeMain_FunsScript.sml
@@ -279,22 +279,6 @@ val betree_leaf_split_back_def = Define ‘
od
-val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
- betree_node_lookup_in_bindings_fwd
- (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result =
- (case bindings of
- | BetreeListCons hd tl =>
- let (i, i0) = hd in
- if i = key
- then Return (SOME i0)
- else
- if u64_gt i key
- then Return NONE
- else betree_node_lookup_in_bindings_fwd key tl
- | BetreeListNil => Return NONE)
-’
-
val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
betree_node_lookup_first_message_for_key_fwd
@@ -396,7 +380,51 @@ val [betree_node_apply_upserts_back_def] = DefineDiv ‘
od
-val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def] = DefineDiv ‘
+val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘
+ (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+ betree_node_lookup_in_bindings_fwd
+ (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result =
+ (case bindings of
+ | BetreeListCons hd tl =>
+ let (i, i0) = hd in
+ if i = key
+ then Return (SOME i0)
+ else
+ if u64_gt i key
+ then Return NONE
+ else betree_node_lookup_in_bindings_fwd key tl
+ | BetreeListNil => Return NONE)
+’
+
+val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def, betree_node_lookup_fwd_def, betree_node_lookup_back_def] = DefineDiv ‘
+ (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+ (betree_internal_lookup_in_children_fwd
+ (self : betree_internal_t) (key : u64) (st : state) :
+ (state # u64 option) result
+ =
+ if u64_lt key self.betree_internal_pivot
+ then betree_node_lookup_fwd self.betree_internal_left key st
+ else betree_node_lookup_fwd self.betree_internal_right key st)
+ /\
+
+ (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+ (betree_internal_lookup_in_children_back
+ (self : betree_internal_t) (key : u64) (st : state) :
+ betree_internal_t result
+ =
+ if u64_lt key self.betree_internal_pivot
+ then (
+ do
+ n <- betree_node_lookup_back self.betree_internal_left key st;
+ Return (self with <| betree_internal_left := n |>)
+ od)
+ else (
+ do
+ n <- betree_node_lookup_back self.betree_internal_right key st;
+ Return (self with <| betree_internal_right := n |>)
+ od))
+ /\
+
(** [betree_main::betree::Node::{5}::lookup]: forward function *)
(betree_node_lookup_fwd
(self : betree_node_t) (key : u64) (st : state) :
@@ -468,8 +496,8 @@ val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lo
/\
(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
- (betree_node_lookup_back
- (self : betree_node_t) (key : u64) (st : state) : betree_node_t result =
+ betree_node_lookup_back
+ (self : betree_node_t) (key : u64) (st : state) : betree_node_t result =
(case self of
| BetreeNodeInternal node =>
do
@@ -532,142 +560,7 @@ val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lo
(_, bindings) <- betree_load_leaf_node_fwd node.betree_leaf_id st;
_ <- betree_node_lookup_in_bindings_fwd key bindings;
Return (BetreeNodeLeaf node)
- od))
- /\
-
- (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
- (betree_internal_lookup_in_children_fwd
- (self : betree_internal_t) (key : u64) (st : state) :
- (state # u64 option) result
- =
- if u64_lt key self.betree_internal_pivot
- then betree_node_lookup_fwd self.betree_internal_left key st
- else betree_node_lookup_fwd self.betree_internal_right key st)
- /\
-
- (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
- betree_internal_lookup_in_children_back
- (self : betree_internal_t) (key : u64) (st : state) :
- betree_internal_t result
- =
- if u64_lt key self.betree_internal_pivot
- then (
- do
- n <- betree_node_lookup_back self.betree_internal_left key st;
- Return (self with <| betree_internal_left := n |>)
od)
- else (
- do
- n <- betree_node_lookup_back self.betree_internal_right key st;
- Return (self with <| betree_internal_right := n |>)
- od)
-’
-
-val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
- betree_node_lookup_mut_in_bindings_fwd
- (key : u64) (bindings : (u64 # u64) betree_list_t) :
- (u64 # u64) betree_list_t result
- =
- (case bindings of
- | BetreeListCons hd tl =>
- let (i, i0) = hd in
- if u64_ge i key
- then Return (BetreeListCons (i, i0) tl)
- else betree_node_lookup_mut_in_bindings_fwd key tl
- | BetreeListNil => Return BetreeListNil)
-’
-
-val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
- betree_node_lookup_mut_in_bindings_back
- (key : u64) (bindings : (u64 # u64) betree_list_t)
- (ret : (u64 # u64) betree_list_t) :
- (u64 # u64) betree_list_t result
- =
- (case bindings of
- | BetreeListCons hd tl =>
- let (i, i0) = hd in
- if u64_ge i key
- then Return ret
- else (
- do
- tl0 <- betree_node_lookup_mut_in_bindings_back key tl ret;
- Return (BetreeListCons (i, i0) tl0)
- od)
- | BetreeListNil => Return ret)
-’
-
-val betree_node_apply_to_leaf_fwd_back_def = Define ‘
- (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
- betree_node_apply_to_leaf_fwd_back
- (bindings : (u64 # u64) betree_list_t) (key : u64)
- (new_msg : betree_message_t) :
- (u64 # u64) betree_list_t result
- =
- do
- bindings0 <- betree_node_lookup_mut_in_bindings_fwd key bindings;
- b <- betree_list_head_has_key_fwd bindings0 key;
- if b
- then (
- do
- hd <- betree_list_pop_front_fwd bindings0;
- (case new_msg of
- | BetreeMessageInsert v =>
- do
- bindings1 <- betree_list_pop_front_back bindings0;
- bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
- betree_node_lookup_mut_in_bindings_back key bindings bindings2
- od
- | BetreeMessageDelete =>
- do
- bindings1 <- betree_list_pop_front_back bindings0;
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- od
- | BetreeMessageUpsert s =>
- let (_, i) = hd in
- do
- v <- betree_upsert_update_fwd (SOME i) s;
- bindings1 <- betree_list_pop_front_back bindings0;
- bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
- betree_node_lookup_mut_in_bindings_back key bindings bindings2
- od)
- od)
- else
- (case new_msg of
- | BetreeMessageInsert v =>
- do
- bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- od
- | BetreeMessageDelete =>
- betree_node_lookup_mut_in_bindings_back key bindings bindings0
- | BetreeMessageUpsert s =>
- do
- v <- betree_upsert_update_fwd NONE s;
- bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
- betree_node_lookup_mut_in_bindings_back key bindings bindings1
- od)
- od
-’
-
-val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
- betree_node_apply_messages_to_leaf_fwd_back
- (bindings : (u64 # u64) betree_list_t)
- (new_msgs : (u64 # betree_message_t) betree_list_t) :
- (u64 # u64) betree_list_t result
- =
- (case new_msgs of
- | BetreeListCons new_msg new_msgs_tl =>
- let (i, m) = new_msg in
- do
- bindings0 <- betree_node_apply_to_leaf_fwd_back bindings i m;
- betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
- od
- | BetreeListNil => Return bindings)
val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘
@@ -811,7 +704,211 @@ val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘
| BetreeListNil => Return msgs)
-val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, betree_internal_flush_fwd_def, betree_internal_flush_back_def] = DefineDiv ‘
+val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘
+ (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+ betree_node_lookup_mut_in_bindings_fwd
+ (key : u64) (bindings : (u64 # u64) betree_list_t) :
+ (u64 # u64) betree_list_t result
+ =
+ (case bindings of
+ | BetreeListCons hd tl =>
+ let (i, i0) = hd in
+ if u64_ge i key
+ then Return (BetreeListCons (i, i0) tl)
+ else betree_node_lookup_mut_in_bindings_fwd key tl
+ | BetreeListNil => Return BetreeListNil)
+’
+
+val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘
+ (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+ betree_node_lookup_mut_in_bindings_back
+ (key : u64) (bindings : (u64 # u64) betree_list_t)
+ (ret : (u64 # u64) betree_list_t) :
+ (u64 # u64) betree_list_t result
+ =
+ (case bindings of
+ | BetreeListCons hd tl =>
+ let (i, i0) = hd in
+ if u64_ge i key
+ then Return ret
+ else (
+ do
+ tl0 <- betree_node_lookup_mut_in_bindings_back key tl ret;
+ Return (BetreeListCons (i, i0) tl0)
+ od)
+ | BetreeListNil => Return ret)
+’
+
+val betree_node_apply_to_leaf_fwd_back_def = Define ‘
+ (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+ betree_node_apply_to_leaf_fwd_back
+ (bindings : (u64 # u64) betree_list_t) (key : u64)
+ (new_msg : betree_message_t) :
+ (u64 # u64) betree_list_t result
+ =
+ do
+ bindings0 <- betree_node_lookup_mut_in_bindings_fwd key bindings;
+ b <- betree_list_head_has_key_fwd bindings0 key;
+ if b
+ then (
+ do
+ hd <- betree_list_pop_front_fwd bindings0;
+ (case new_msg of
+ | BetreeMessageInsert v =>
+ do
+ bindings1 <- betree_list_pop_front_back bindings0;
+ bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
+ betree_node_lookup_mut_in_bindings_back key bindings bindings2
+ od
+ | BetreeMessageDelete =>
+ do
+ bindings1 <- betree_list_pop_front_back bindings0;
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ od
+ | BetreeMessageUpsert s =>
+ let (_, i) = hd in
+ do
+ v <- betree_upsert_update_fwd (SOME i) s;
+ bindings1 <- betree_list_pop_front_back bindings0;
+ bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
+ betree_node_lookup_mut_in_bindings_back key bindings bindings2
+ od)
+ od)
+ else
+ (case new_msg of
+ | BetreeMessageInsert v =>
+ do
+ bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ od
+ | BetreeMessageDelete =>
+ betree_node_lookup_mut_in_bindings_back key bindings bindings0
+ | BetreeMessageUpsert s =>
+ do
+ v <- betree_upsert_update_fwd NONE s;
+ bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
+ betree_node_lookup_mut_in_bindings_back key bindings bindings1
+ od)
+ od
+’
+
+val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘
+ (** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
+ betree_node_apply_messages_to_leaf_fwd_back
+ (bindings : (u64 # u64) betree_list_t)
+ (new_msgs : (u64 # betree_message_t) betree_list_t) :
+ (u64 # u64) betree_list_t result
+ =
+ (case new_msgs of
+ | BetreeListCons new_msg new_msgs_tl =>
+ let (i, m) = new_msg in
+ do
+ bindings0 <- betree_node_apply_to_leaf_fwd_back bindings i m;
+ betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+ od
+ | BetreeListNil => Return bindings)
+’
+
+val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def] = DefineDiv ‘
+ (** [betree_main::betree::Internal::{4}::flush]: forward function *)
+ (betree_internal_flush_fwd
+ (self : betree_internal_t) (params : betree_params_t)
+ (node_id_cnt : betree_node_id_counter_t)
+ (content : (u64 # betree_message_t) betree_list_t) (st : state) :
+ (state # (u64 # betree_message_t) betree_list_t) result
+ =
+ do
+ p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
+ let (msgs_left, msgs_right) = p in
+ do
+ len_left <- betree_list_len_fwd msgs_left;
+ if u64_ge len_left params.betree_params_min_flush_size
+ then (
+ do
+ (st0, _) <-
+ betree_node_apply_messages_fwd self.betree_internal_left params
+ node_id_cnt msgs_left st;
+ (_, node_id_cnt0) <-
+ betree_node_apply_messages_back self.betree_internal_left params
+ node_id_cnt msgs_left st;
+ len_right <- betree_list_len_fwd msgs_right;
+ if u64_ge len_right params.betree_params_min_flush_size
+ then (
+ do
+ (st1, _) <-
+ betree_node_apply_messages_fwd self.betree_internal_right params
+ node_id_cnt0 msgs_right st0;
+ _ <-
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt0 msgs_right st0;
+ Return (st1, BetreeListNil)
+ od)
+ else Return (st0, msgs_right)
+ od)
+ else (
+ do
+ (st0, _) <-
+ betree_node_apply_messages_fwd self.betree_internal_right params
+ node_id_cnt msgs_right st;
+ _ <-
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt msgs_right st;
+ Return (st0, msgs_left)
+ od)
+ od
+ od)
+ /\
+
+ (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+ (betree_internal_flush_back
+ (self : betree_internal_t) (params : betree_params_t)
+ (node_id_cnt : betree_node_id_counter_t)
+ (content : (u64 # betree_message_t) betree_list_t) (st : state) :
+ (betree_internal_t # betree_node_id_counter_t) result
+ =
+ do
+ p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
+ let (msgs_left, msgs_right) = p in
+ do
+ len_left <- betree_list_len_fwd msgs_left;
+ if u64_ge len_left params.betree_params_min_flush_size
+ then (
+ do
+ (st0, _) <-
+ betree_node_apply_messages_fwd self.betree_internal_left params
+ node_id_cnt msgs_left st;
+ (n, node_id_cnt0) <-
+ betree_node_apply_messages_back self.betree_internal_left params
+ node_id_cnt msgs_left st;
+ len_right <- betree_list_len_fwd msgs_right;
+ if u64_ge len_right params.betree_params_min_flush_size
+ then (
+ do
+ (n0, node_id_cnt1) <-
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt0 msgs_right st0;
+ Return
+ (self
+ with
+ <|
+ betree_internal_left := n; betree_internal_right := n0
+ |>, node_id_cnt1)
+ od)
+ else Return (self with <| betree_internal_left := n |>, node_id_cnt0)
+ od)
+ else (
+ do
+ (n, node_id_cnt0) <-
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt msgs_right st;
+ Return (self with <| betree_internal_right := n |>, node_id_cnt0)
+ od)
+ od
+ od)
+ /\
+
(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
(betree_node_apply_messages_fwd
(self : betree_node_t) (params : betree_params_t)
@@ -868,12 +965,12 @@ val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, be
/\
(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
- (betree_node_apply_messages_back
- (self : betree_node_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t)
- (msgs : (u64 # betree_message_t) betree_list_t) (st : state) :
- (betree_node_t # betree_node_id_counter_t) result
- =
+ betree_node_apply_messages_back
+ (self : betree_node_t) (params : betree_params_t)
+ (node_id_cnt : betree_node_id_counter_t)
+ (msgs : (u64 # betree_message_t) betree_list_t) (st : state) :
+ (betree_node_t # betree_node_id_counter_t) result
+ =
(case self of
| BetreeNodeInternal node =>
do
@@ -921,104 +1018,7 @@ val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, be
Return (BetreeNodeLeaf (node with <| betree_leaf_size := len |>),
node_id_cnt)
od)
- od))
- /\
-
- (** [betree_main::betree::Internal::{4}::flush]: forward function *)
- (betree_internal_flush_fwd
- (self : betree_internal_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t)
- (content : (u64 # betree_message_t) betree_list_t) (st : state) :
- (state # (u64 # betree_message_t) betree_list_t) result
- =
- do
- p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
- let (msgs_left, msgs_right) = p in
- do
- len_left <- betree_list_len_fwd msgs_left;
- if u64_ge len_left params.betree_params_min_flush_size
- then (
- do
- (st0, _) <-
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st;
- (_, node_id_cnt0) <-
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st;
- len_right <- betree_list_len_fwd msgs_right;
- if u64_ge len_right params.betree_params_min_flush_size
- then (
- do
- (st1, _) <-
- betree_node_apply_messages_fwd self.betree_internal_right params
- node_id_cnt0 msgs_right st0;
- _ <-
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt0 msgs_right st0;
- Return (st1, BetreeListNil)
- od)
- else Return (st0, msgs_right)
- od)
- else (
- do
- (st0, _) <-
- betree_node_apply_messages_fwd self.betree_internal_right params
- node_id_cnt msgs_right st;
- _ <-
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st;
- Return (st0, msgs_left)
od)
- od
- od)
- /\
-
- (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
- betree_internal_flush_back
- (self : betree_internal_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t)
- (content : (u64 # betree_message_t) betree_list_t) (st : state) :
- (betree_internal_t # betree_node_id_counter_t) result
- =
- do
- p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
- let (msgs_left, msgs_right) = p in
- do
- len_left <- betree_list_len_fwd msgs_left;
- if u64_ge len_left params.betree_params_min_flush_size
- then (
- do
- (st0, _) <-
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st;
- (n, node_id_cnt0) <-
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st;
- len_right <- betree_list_len_fwd msgs_right;
- if u64_ge len_right params.betree_params_min_flush_size
- then (
- do
- (n0, node_id_cnt1) <-
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt0 msgs_right st0;
- Return
- (self
- with
- <|
- betree_internal_left := n; betree_internal_right := n0
- |>, node_id_cnt1)
- od)
- else Return (self with <| betree_internal_left := n |>, node_id_cnt0)
- od)
- else (
- do
- (n, node_id_cnt0) <-
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st;
- Return (self with <| betree_internal_right := n |>, node_id_cnt0)
- od)
- od
- od
val betree_node_apply_fwd_def = Define ‘
diff --git a/tests/hol4/betree/betreeMain_TypesScript.sml b/tests/hol4/betree/betreeMain_TypesScript.sml
index c43421c2..779f6abb 100644
--- a/tests/hol4/betree/betreeMain_TypesScript.sml
+++ b/tests/hol4/betree/betreeMain_TypesScript.sml
@@ -31,12 +31,6 @@ Datatype:
End
Datatype:
- (** [betree_main::betree::Node] *)
- betree_node_t =
- | BetreeNodeInternal betree_internal_t
- | BetreeNodeLeaf betree_leaf_t
- ;
-
(** [betree_main::betree::Internal] *)
betree_internal_t =
<|
@@ -45,6 +39,12 @@ Datatype:
betree_internal_left : betree_node_t;
betree_internal_right : betree_node_t;
|>
+ ;
+
+ (** [betree_main::betree::Node] *)
+ betree_node_t =
+ | BetreeNodeInternal betree_internal_t
+ | BetreeNodeLeaf betree_leaf_t
End
Datatype:
diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betreeMain_TypesTheory.sig
index a451eae9..cffe6afb 100644
--- a/tests/hol4/betree/betreeMain_TypesTheory.sig
+++ b/tests/hol4/betree/betreeMain_TypesTheory.sig
@@ -22,6 +22,7 @@ sig
val betree_internal_t_betree_internal_right : thm
val betree_internal_t_betree_internal_right_fupd : thm
val betree_internal_t_case_def : thm
+ val betree_internal_t_size_def : thm
val betree_leaf_t_TY_DEF : thm
val betree_leaf_t_betree_leaf_id : thm
val betree_leaf_t_betree_leaf_id_fupd : thm
@@ -42,7 +43,6 @@ sig
val betree_node_id_counter_t_size_def : thm
val betree_node_t_TY_DEF : thm
val betree_node_t_case_def : thm
- val betree_node_t_size_def : thm
val betree_params_t_TY_DEF : thm
val betree_params_t_betree_params_min_flush_size : thm
val betree_params_t_betree_params_min_flush_size_fupd : thm
@@ -177,11 +177,11 @@ sig
val betree_upsert_fun_state_t_induction : thm
val betree_upsert_fun_state_t_nchotomy : thm
val datatype_betree_be_tree_t : thm
+ val datatype_betree_internal_t : thm
val datatype_betree_leaf_t : thm
val datatype_betree_list_t : thm
val datatype_betree_message_t : thm
val datatype_betree_node_id_counter_t : thm
- val datatype_betree_node_t : thm
val datatype_betree_params_t : thm
val datatype_betree_upsert_fun_state_t : thm
@@ -253,30 +253,30 @@ sig
⊢ ∃rep.
TYPE_DEFINITION
- (λa1'.
- ∀ $var$('betree_node_t') $var$('betree_internal_t').
+ (λa0'.
+ ∀ $var$('betree_internal_t') $var$('betree_node_t').
(∀a0'.
- (∃a. a0' =
- (λa.
- ind_type$CONSTR 0 (ARB,ARB,ARB)
- (ind_type$FCONS a (λn. ind_type$BOTTOM)))
- a ∧ $var$('betree_internal_t') a) ∨
- (∃a. a0' =
- (λa.
- ind_type$CONSTR (SUC 0) (a,ARB,ARB)
- (λn. ind_type$BOTTOM)) a) ⇒
- $var$('betree_node_t') a0') ∧
- (∀a1'.
(∃a0 a1 a2 a3.
- a1' =
+ a0' =
(λa0 a1 a2 a3.
- ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1)
+ ind_type$CONSTR 0 (a0,a1,ARB)
(ind_type$FCONS a2
(ind_type$FCONS a3 (λn. ind_type$BOTTOM))))
a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧
$var$('betree_node_t') a3) ⇒
- $var$('betree_internal_t') a1') ⇒
- $var$('betree_internal_t') a1') rep
+ $var$('betree_internal_t') a0') ∧
+ (∀a1'.
+ (∃a. a1' =
+ (λa.
+ ind_type$CONSTR (SUC 0) (ARB,ARB,ARB)
+ (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+ a ∧ $var$('betree_internal_t') a) ∨
+ (∃a. a1' =
+ (λa.
+ ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB,a)
+ (λn. ind_type$BOTTOM)) a) ⇒
+ $var$('betree_node_t') a1') ⇒
+ $var$('betree_internal_t') a0') rep
[betree_internal_t_betree_internal_id] Definition
@@ -329,6 +329,16 @@ sig
betree_internal_t_CASE (betree_internal_t a0 a1 a2 a3) f =
f a0 a1 a2 a3
+ [betree_internal_t_size_def] Definition
+
+ ⊢ (∀a0 a1 a2 a3.
+ betree_internal_t_size (betree_internal_t a0 a1 a2 a3) =
+ 1 + (betree_node_t_size a2 + betree_node_t_size a3)) ∧
+ (∀a. betree_node_t_size (BetreeNodeInternal a) =
+ 1 + betree_internal_t_size a) ∧
+ ∀a. betree_node_t_size (BetreeNodeLeaf a) =
+ 1 + betree_leaf_t_size a
+
[betree_leaf_t_TY_DEF] Definition
⊢ ∃rep.
@@ -479,46 +489,36 @@ sig
⊢ ∃rep.
TYPE_DEFINITION
- (λa0'.
- ∀ $var$('betree_node_t') $var$('betree_internal_t').
+ (λa1'.
+ ∀ $var$('betree_internal_t') $var$('betree_node_t').
(∀a0'.
- (∃a. a0' =
- (λa.
- ind_type$CONSTR 0 (ARB,ARB,ARB)
- (ind_type$FCONS a (λn. ind_type$BOTTOM)))
- a ∧ $var$('betree_internal_t') a) ∨
- (∃a. a0' =
- (λa.
- ind_type$CONSTR (SUC 0) (a,ARB,ARB)
- (λn. ind_type$BOTTOM)) a) ⇒
- $var$('betree_node_t') a0') ∧
- (∀a1'.
(∃a0 a1 a2 a3.
- a1' =
+ a0' =
(λa0 a1 a2 a3.
- ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1)
+ ind_type$CONSTR 0 (a0,a1,ARB)
(ind_type$FCONS a2
(ind_type$FCONS a3 (λn. ind_type$BOTTOM))))
a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧
$var$('betree_node_t') a3) ⇒
- $var$('betree_internal_t') a1') ⇒
- $var$('betree_node_t') a0') rep
+ $var$('betree_internal_t') a0') ∧
+ (∀a1'.
+ (∃a. a1' =
+ (λa.
+ ind_type$CONSTR (SUC 0) (ARB,ARB,ARB)
+ (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+ a ∧ $var$('betree_internal_t') a) ∨
+ (∃a. a1' =
+ (λa.
+ ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB,a)
+ (λn. ind_type$BOTTOM)) a) ⇒
+ $var$('betree_node_t') a1') ⇒
+ $var$('betree_node_t') a1') rep
[betree_node_t_case_def] Definition
⊢ (∀a f f1. betree_node_t_CASE (BetreeNodeInternal a) f f1 = f a) ∧
∀a f f1. betree_node_t_CASE (BetreeNodeLeaf a) f f1 = f1 a
- [betree_node_t_size_def] Definition
-
- ⊢ (∀a. betree_node_t_size (BetreeNodeInternal a) =
- 1 + betree_internal_t_size a) ∧
- (∀a. betree_node_t_size (BetreeNodeLeaf a) =
- 1 + betree_leaf_t_size a) ∧
- ∀a0 a1 a2 a3.
- betree_internal_t_size (betree_internal_t a0 a1 a2 a3) =
- 1 + (betree_node_t_size a2 + betree_node_t_size a3)
-
[betree_params_t_TY_DEF] Definition
⊢ ∃rep.
@@ -883,11 +883,11 @@ sig
[betree_internal_t_Axiom] Theorem
⊢ ∀f0 f1 f2. ∃fn0 fn1.
- (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧
- (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧
- ∀a0 a1 a2 a3.
- fn1 (betree_internal_t a0 a1 a2 a3) =
- f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3)
+ (∀a0 a1 a2 a3.
+ fn0 (betree_internal_t a0 a1 a2 a3) =
+ f0 a0 a1 a2 a3 (fn1 a2) (fn1 a3)) ∧
+ (∀a. fn1 (BetreeNodeInternal a) = f1 a (fn0 a)) ∧
+ ∀a. fn1 (BetreeNodeLeaf a) = f2 a
[betree_internal_t_accessors] Theorem
@@ -1130,9 +1130,9 @@ sig
[betree_internal_t_induction] Theorem
⊢ ∀P0 P1.
- (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧
- (∀b. P0 (BetreeNodeLeaf b)) ∧
- (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒
+ (∀b b0. P1 b ∧ P1 b0 ⇒ ∀u u0. P0 (betree_internal_t u0 u b b0)) ∧
+ (∀b. P0 b ⇒ P1 (BetreeNodeInternal b)) ∧
+ (∀b. P1 (BetreeNodeLeaf b)) ⇒
(∀b. P0 b) ∧ ∀b. P1 b
[betree_internal_t_literal_11] Theorem
@@ -1472,11 +1472,11 @@ sig
[betree_node_t_Axiom] Theorem
⊢ ∀f0 f1 f2. ∃fn0 fn1.
- (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧
- (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧
- ∀a0 a1 a2 a3.
- fn1 (betree_internal_t a0 a1 a2 a3) =
- f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3)
+ (∀a0 a1 a2 a3.
+ fn0 (betree_internal_t a0 a1 a2 a3) =
+ f0 a0 a1 a2 a3 (fn1 a2) (fn1 a3)) ∧
+ (∀a. fn1 (BetreeNodeInternal a) = f1 a (fn0 a)) ∧
+ ∀a. fn1 (BetreeNodeLeaf a) = f2 a
[betree_node_t_case_cong] Theorem
@@ -1498,9 +1498,9 @@ sig
[betree_node_t_induction] Theorem
⊢ ∀P0 P1.
- (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧
- (∀b. P0 (BetreeNodeLeaf b)) ∧
- (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒
+ (∀b b0. P1 b ∧ P1 b0 ⇒ ∀u u0. P0 (betree_internal_t u0 u b b0)) ∧
+ (∀b. P0 b ⇒ P1 (BetreeNodeInternal b)) ∧
+ (∀b. P1 (BetreeNodeLeaf b)) ⇒
(∀b. P0 b) ∧ ∀b. P1 b
[betree_node_t_nchotomy] Theorem
@@ -1706,6 +1706,14 @@ sig
(record betree_be_tree_t betree_be_tree_params
betree_be_tree_node_id_cnt betree_be_tree_root)
+ [datatype_betree_internal_t] Theorem
+
+ ⊢ DATATYPE
+ (record betree_internal_t betree_internal_id
+ betree_internal_pivot betree_internal_left
+ betree_internal_right ∧
+ betree_node_t BetreeNodeInternal BetreeNodeLeaf)
+
[datatype_betree_leaf_t] Theorem
⊢ DATATYPE (record betree_leaf_t betree_leaf_id betree_leaf_size)
@@ -1726,14 +1734,6 @@ sig
(record betree_node_id_counter_t
betree_node_id_counter_next_node_id)
- [datatype_betree_node_t] Theorem
-
- ⊢ DATATYPE
- (betree_node_t BetreeNodeInternal BetreeNodeLeaf ∧
- record betree_internal_t betree_internal_id
- betree_internal_pivot betree_internal_left
- betree_internal_right)
-
[datatype_betree_params_t] Theorem
⊢ DATATYPE
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
index 66614c3f..1b2d6121 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
+++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
@@ -279,11 +279,11 @@ val test_char_fwd_def = Define ‘
Datatype:
- (** [no_nested_borrows::NodeElem] *)
- node_elem_t = | NodeElemCons tree_t node_elem_t | NodeElemNil ;
-
(** [no_nested_borrows::Tree] *)
- tree_t = | TreeLeaf 't | TreeNode 't node_elem_t tree_t
+ tree_t = | TreeLeaf 't | TreeNode 't node_elem_t tree_t ;
+
+ (** [no_nested_borrows::NodeElem] *)
+ node_elem_t = | NodeElemCons tree_t node_elem_t | NodeElemNil
End
val [list_length_fwd_def] = DefineDiv ‘
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
index c0ff4e09..67368e38 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
+++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
@@ -47,7 +47,6 @@ sig
val new_tuple3_fwd_def : thm
val node_elem_t_TY_DEF : thm
val node_elem_t_case_def : thm
- val node_elem_t_size_def : thm
val one_t_TY_DEF : thm
val one_t_case_def : thm
val one_t_size_def : thm
@@ -97,6 +96,7 @@ sig
val test_weird_borrows1_fwd_def : thm
val tree_t_TY_DEF : thm
val tree_t_case_def : thm
+ val tree_t_size_def : thm
(* Theorems *)
val EXISTS_pair_t : thm
@@ -108,12 +108,12 @@ sig
val datatype_empty_enum_t : thm
val datatype_enum_t : thm
val datatype_list_t : thm
- val datatype_node_elem_t : thm
val datatype_one_t : thm
val datatype_pair_t : thm
val datatype_struct_with_pair_t : thm
val datatype_struct_with_tuple_t : thm
val datatype_sum_t : thm
+ val datatype_tree_t : thm
val empty_enum_t2num_11 : thm
val empty_enum_t2num_ONTO : thm
val empty_enum_t2num_num2empty_enum_t : thm
@@ -491,52 +491,41 @@ sig
⊢ ∃rep.
TYPE_DEFINITION
- (λa0'.
- ∀ $var$('node_elem_t') $var$('tree_t').
+ (λa1'.
+ ∀ $var$('tree_t') $var$('node_elem_t').
(∀a0'.
- (∃a0 a1.
- a0' =
- (λa0 a1.
- ind_type$CONSTR 0 ARB
- (ind_type$FCONS a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
- a0 a1 ∧ $var$('tree_t') a0 ∧
- $var$('node_elem_t') a1) ∨
- a0' =
- ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
- $var$('node_elem_t') a0') ∧
- (∀a1'.
- (∃a. a1' =
- (λa.
- ind_type$CONSTR (SUC (SUC 0)) a
- (λn. ind_type$BOTTOM)) a) ∨
+ (∃a. a0' =
+ (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+ a) ∨
(∃a0 a1 a2.
- a1' =
+ a0' =
(λa0 a1 a2.
- ind_type$CONSTR (SUC (SUC (SUC 0))) a0
+ ind_type$CONSTR (SUC 0) a0
(ind_type$FCONS a1
(ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
$var$('tree_t') a2) ⇒
- $var$('tree_t') a1') ⇒
- $var$('node_elem_t') a0') rep
+ $var$('tree_t') a0') ∧
+ (∀a1'.
+ (∃a0 a1.
+ a1' =
+ (λa0 a1.
+ ind_type$CONSTR (SUC (SUC 0)) ARB
+ (ind_type$FCONS a0
+ (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+ a0 a1 ∧ $var$('tree_t') a0 ∧
+ $var$('node_elem_t') a1) ∨
+ a1' =
+ ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+ (λn. ind_type$BOTTOM) ⇒
+ $var$('node_elem_t') a1') ⇒
+ $var$('node_elem_t') a1') rep
[node_elem_t_case_def] Definition
⊢ (∀a0 a1 f v. node_elem_t_CASE (NodeElemCons a0 a1) f v = f a0 a1) ∧
∀f v. node_elem_t_CASE NodeElemNil f v = v
- [node_elem_t_size_def] Definition
-
- ⊢ (∀f a0 a1.
- node_elem_t_size f (NodeElemCons a0 a1) =
- 1 + (tree_t_size f a0 + node_elem_t_size f a1)) ∧
- (∀f. node_elem_t_size f NodeElemNil = 0) ∧
- (∀f a. tree_t_size f (TreeLeaf a) = 1 + f a) ∧
- ∀f a0 a1 a2.
- tree_t_size f (TreeNode a0 a1 a2) =
- 1 + (f a0 + (node_elem_t_size f a1 + tree_t_size f a2))
-
[one_t_TY_DEF] Definition
⊢ ∃rep.
@@ -923,41 +912,52 @@ sig
⊢ ∃rep.
TYPE_DEFINITION
- (λa1'.
- ∀ $var$('node_elem_t') $var$('tree_t').
+ (λa0'.
+ ∀ $var$('tree_t') $var$('node_elem_t').
(∀a0'.
- (∃a0 a1.
- a0' =
- (λa0 a1.
- ind_type$CONSTR 0 ARB
- (ind_type$FCONS a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
- a0 a1 ∧ $var$('tree_t') a0 ∧
- $var$('node_elem_t') a1) ∨
- a0' =
- ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
- $var$('node_elem_t') a0') ∧
- (∀a1'.
- (∃a. a1' =
- (λa.
- ind_type$CONSTR (SUC (SUC 0)) a
- (λn. ind_type$BOTTOM)) a) ∨
+ (∃a. a0' =
+ (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+ a) ∨
(∃a0 a1 a2.
- a1' =
+ a0' =
(λa0 a1 a2.
- ind_type$CONSTR (SUC (SUC (SUC 0))) a0
+ ind_type$CONSTR (SUC 0) a0
(ind_type$FCONS a1
(ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
$var$('tree_t') a2) ⇒
- $var$('tree_t') a1') ⇒
- $var$('tree_t') a1') rep
+ $var$('tree_t') a0') ∧
+ (∀a1'.
+ (∃a0 a1.
+ a1' =
+ (λa0 a1.
+ ind_type$CONSTR (SUC (SUC 0)) ARB
+ (ind_type$FCONS a0
+ (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+ a0 a1 ∧ $var$('tree_t') a0 ∧
+ $var$('node_elem_t') a1) ∨
+ a1' =
+ ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+ (λn. ind_type$BOTTOM) ⇒
+ $var$('node_elem_t') a1') ⇒
+ $var$('tree_t') a0') rep
[tree_t_case_def] Definition
⊢ (∀a f f1. tree_t_CASE (TreeLeaf a) f f1 = f a) ∧
∀a0 a1 a2 f f1. tree_t_CASE (TreeNode a0 a1 a2) f f1 = f1 a0 a1 a2
+ [tree_t_size_def] Definition
+
+ ⊢ (∀f a. tree_t_size f (TreeLeaf a) = 1 + f a) ∧
+ (∀f a0 a1 a2.
+ tree_t_size f (TreeNode a0 a1 a2) =
+ 1 + (f a0 + (node_elem_t_size f a1 + tree_t_size f a2))) ∧
+ (∀f a0 a1.
+ node_elem_t_size f (NodeElemCons a0 a1) =
+ 1 + (tree_t_size f a0 + node_elem_t_size f a1)) ∧
+ ∀f. node_elem_t_size f NodeElemNil = 0
+
[EXISTS_pair_t] Theorem
⊢ ∀P. (∃p. P p) ⇔ ∃t0 t. P <|pair_x := t0; pair_y := t|>
@@ -994,11 +994,6 @@ sig
⊢ DATATYPE (list_t ListCons ListNil)
- [datatype_node_elem_t] Theorem
-
- ⊢ DATATYPE
- (node_elem_t NodeElemCons NodeElemNil ∧ tree_t TreeLeaf TreeNode)
-
[datatype_one_t] Theorem
⊢ DATATYPE (one_t OneOne)
@@ -1019,6 +1014,11 @@ sig
⊢ DATATYPE (sum_t SumLeft SumRight)
+ [datatype_tree_t] Theorem
+
+ ⊢ DATATYPE
+ (tree_t TreeLeaf TreeNode ∧ node_elem_t NodeElemCons NodeElemNil)
+
[empty_enum_t2num_11] Theorem
⊢ ∀a a'. empty_enum_t2num a = empty_enum_t2num a' ⇔ a = a'
@@ -1167,10 +1167,11 @@ sig
[node_elem_t_Axiom] Theorem
⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
- (∀a0 a1. fn0 (NodeElemCons a0 a1) = f0 a0 a1 (fn1 a0) (fn0 a1)) ∧
- fn0 NodeElemNil = f1 ∧ (∀a. fn1 (TreeLeaf a) = f2 a) ∧
- ∀a0 a1 a2.
- fn1 (TreeNode a0 a1 a2) = f3 a0 a1 a2 (fn0 a1) (fn1 a2)
+ (∀a. fn0 (TreeLeaf a) = f0 a) ∧
+ (∀a0 a1 a2.
+ fn0 (TreeNode a0 a1 a2) = f1 a0 a1 a2 (fn1 a1) (fn0 a2)) ∧
+ (∀a0 a1. fn1 (NodeElemCons a0 a1) = f2 a0 a1 (fn0 a0) (fn1 a1)) ∧
+ fn1 NodeElemNil = f3
[node_elem_t_case_cong] Theorem
@@ -1192,10 +1193,10 @@ sig
[node_elem_t_induction] Theorem
⊢ ∀P0 P1.
- (∀t n. P1 t ∧ P0 n ⇒ P0 (NodeElemCons t n)) ∧ P0 NodeElemNil ∧
- (∀t. P1 (TreeLeaf t)) ∧
- (∀n t. P0 n ∧ P1 t ⇒ ∀t0. P1 (TreeNode t0 n t)) ⇒
- (∀n. P0 n) ∧ ∀t. P1 t
+ (∀t. P0 (TreeLeaf t)) ∧
+ (∀n t. P1 n ∧ P0 t ⇒ ∀t0. P0 (TreeNode t0 n t)) ∧
+ (∀t n. P0 t ∧ P1 n ⇒ P1 (NodeElemCons t n)) ∧ P1 NodeElemNil ⇒
+ (∀t. P0 t) ∧ ∀n. P1 n
[node_elem_t_nchotomy] Theorem
@@ -1557,10 +1558,11 @@ sig
[tree_t_Axiom] Theorem
⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
- (∀a0 a1. fn0 (NodeElemCons a0 a1) = f0 a0 a1 (fn1 a0) (fn0 a1)) ∧
- fn0 NodeElemNil = f1 ∧ (∀a. fn1 (TreeLeaf a) = f2 a) ∧
- ∀a0 a1 a2.
- fn1 (TreeNode a0 a1 a2) = f3 a0 a1 a2 (fn0 a1) (fn1 a2)
+ (∀a. fn0 (TreeLeaf a) = f0 a) ∧
+ (∀a0 a1 a2.
+ fn0 (TreeNode a0 a1 a2) = f1 a0 a1 a2 (fn1 a1) (fn0 a2)) ∧
+ (∀a0 a1. fn1 (NodeElemCons a0 a1) = f2 a0 a1 (fn0 a0) (fn1 a1)) ∧
+ fn1 NodeElemNil = f3
[tree_t_case_cong] Theorem
@@ -1582,10 +1584,10 @@ sig
[tree_t_induction] Theorem
⊢ ∀P0 P1.
- (∀t n. P1 t ∧ P0 n ⇒ P0 (NodeElemCons t n)) ∧ P0 NodeElemNil ∧
- (∀t. P1 (TreeLeaf t)) ∧
- (∀n t. P0 n ∧ P1 t ⇒ ∀t0. P1 (TreeNode t0 n t)) ⇒
- (∀n. P0 n) ∧ ∀t. P1 t
+ (∀t. P0 (TreeLeaf t)) ∧
+ (∀n t. P1 n ∧ P0 t ⇒ ∀t0. P0 (TreeNode t0 n t)) ∧
+ (∀t n. P0 t ∧ P1 n ⇒ P1 (NodeElemCons t n)) ∧ P1 NodeElemNil ⇒
+ (∀t. P0 t) ∧ ∀n. P1 n
[tree_t_nchotomy] Theorem
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index a6c6f496..933aac88 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -209,20 +209,6 @@ def betree.Leaf.split_back
let _ ← betree.store_leaf_node id1 content1 st0
betree.NodeIdCounter.fresh_id_back node_id_cnt0
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
-divergent def betree.Node.lookup_in_bindings
- (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
- match bindings with
- | betree.List.Cons hd tl =>
- let (i, i0) := hd
- if i = key
- then Result.ret (Option.some i0)
- else
- if i > key
- then Result.ret Option.none
- else betree.Node.lookup_in_bindings key tl
- | betree.List.Nil => Result.ret Option.none
-
/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function -/
divergent def betree.Node.lookup_first_message_for_key
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -312,8 +298,46 @@ divergent def betree.Node.apply_upserts_back
betree.List.push_front (U64 × betree.Message) msgs (key,
betree.Message.Insert v)
+/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
+divergent def betree.Node.lookup_in_bindings
+ (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+ match bindings with
+ | betree.List.Cons hd tl =>
+ let (i, i0) := hd
+ if i = key
+ then Result.ret (Option.some i0)
+ else
+ if i > key
+ then Result.ret Option.none
+ else betree.Node.lookup_in_bindings key tl
+ | betree.List.Nil => Result.ret Option.none
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
+mutual divergent def betree.Internal.lookup_in_children
+ (self : betree.Internal) (key : U64) (st : State) :
+ Result (State × (Option U64))
+ :=
+ let ⟨ _, i, n, n0 ⟩ := self
+ if key < i
+ then betree.Node.lookup n key st
+ else betree.Node.lookup n0 key st
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
+divergent def betree.Internal.lookup_in_children_back
+ (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
+ let ⟨ i, i0, n, n0 ⟩ := self
+ if key < i0
+ then
+ do
+ let n1 ← betree.Node.lookup_back n key st
+ Result.ret (betree.Internal.mk i i0 n1 n0)
+ else
+ do
+ let n1 ← betree.Node.lookup_back n0 key st
+ Result.ret (betree.Internal.mk i i0 n n1)
+
/- [betree_main::betree::Node::{5}::lookup]: forward function -/
-mutual divergent def betree.Node.lookup
+divergent def betree.Node.lookup
(self : betree.Node) (key : U64) (st : State) :
Result (State × (Option U64))
:=
@@ -455,126 +479,8 @@ divergent def betree.Node.lookup_back
let _ ← betree.Node.lookup_in_bindings key bindings
Result.ret (betree.Node.Leaf node)
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
-divergent def betree.Internal.lookup_in_children
- (self : betree.Internal) (key : U64) (st : State) :
- Result (State × (Option U64))
- :=
- let ⟨ _, i, n, n0 ⟩ := self
- if key < i
- then betree.Node.lookup n key st
- else betree.Node.lookup n0 key st
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
-divergent def betree.Internal.lookup_in_children_back
- (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
- let ⟨ i, i0, n, n0 ⟩ := self
- if key < i0
- then
- do
- let n1 ← betree.Node.lookup_back n key st
- Result.ret (betree.Internal.mk i i0 n1 n0)
- else
- do
- let n1 ← betree.Node.lookup_back n0 key st
- Result.ret (betree.Internal.mk i i0 n n1)
-
end
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
-divergent def betree.Node.lookup_mut_in_bindings
- (key : U64) (bindings : betree.List (U64 × U64)) :
- Result (betree.List (U64 × U64))
- :=
- match bindings with
- | betree.List.Cons hd tl =>
- let (i, i0) := hd
- if i >= key
- then Result.ret (betree.List.Cons (i, i0) tl)
- else betree.Node.lookup_mut_in_bindings key tl
- | betree.List.Nil => Result.ret betree.List.Nil
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
-divergent def betree.Node.lookup_mut_in_bindings_back
- (key : U64) (bindings : betree.List (U64 × U64))
- (ret0 : betree.List (U64 × U64)) :
- Result (betree.List (U64 × U64))
- :=
- match bindings with
- | betree.List.Cons hd tl =>
- let (i, i0) := hd
- if i >= key
- then Result.ret ret0
- else
- do
- let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
- Result.ret (betree.List.Cons (i, i0) tl0)
- | betree.List.Nil => Result.ret ret0
-
-/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
-def betree.Node.apply_to_leaf
- (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
- :
- Result (betree.List (U64 × U64))
- :=
- do
- let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
- let b ← betree.List.head_has_key U64 bindings0 key
- if b
- then
- do
- let hd ← betree.List.pop_front (U64 × U64) bindings0
- match new_msg with
- | betree.Message.Insert v =>
- do
- let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
- let bindings2 ←
- betree.List.push_front (U64 × U64) bindings1 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings2
- | betree.Message.Delete =>
- do
- let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
- betree.Node.lookup_mut_in_bindings_back key bindings bindings1
- | betree.Message.Upsert s =>
- do
- let (_, i) := hd
- let v ← betree.upsert_update (Option.some i) s
- let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
- let bindings2 ←
- betree.List.push_front (U64 × U64) bindings1 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings2
- else
- match new_msg with
- | betree.Message.Insert v =>
- do
- let bindings1 ←
- betree.List.push_front (U64 × U64) bindings0 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings1
- | betree.Message.Delete =>
- betree.Node.lookup_mut_in_bindings_back key bindings bindings0
- | betree.Message.Upsert s =>
- do
- let v ← betree.upsert_update Option.none s
- let bindings1 ←
- betree.List.push_front (U64 × U64) bindings0 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings1
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
-divergent def betree.Node.apply_messages_to_leaf
- (bindings : betree.List (U64 × U64))
- (new_msgs : betree.List (U64 × betree.Message)) :
- Result (betree.List (U64 × U64))
- :=
- match new_msgs with
- | betree.List.Cons new_msg new_msgs_tl =>
- do
- let (i, m) := new_msg
- let bindings0 ← betree.Node.apply_to_leaf bindings i m
- betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
- | betree.List.Nil => Result.ret bindings
-
/- [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
divergent def betree.Node.filter_messages_for_key
@@ -706,8 +612,174 @@ divergent def betree.Node.apply_messages_to_internal
betree.Node.apply_messages_to_internal msgs0 new_msgs_tl
| betree.List.Nil => Result.ret msgs
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
+divergent def betree.Node.lookup_mut_in_bindings
+ (key : U64) (bindings : betree.List (U64 × U64)) :
+ Result (betree.List (U64 × U64))
+ :=
+ match bindings with
+ | betree.List.Cons hd tl =>
+ let (i, i0) := hd
+ if i >= key
+ then Result.ret (betree.List.Cons (i, i0) tl)
+ else betree.Node.lookup_mut_in_bindings key tl
+ | betree.List.Nil => Result.ret betree.List.Nil
+
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
+divergent def betree.Node.lookup_mut_in_bindings_back
+ (key : U64) (bindings : betree.List (U64 × U64))
+ (ret0 : betree.List (U64 × U64)) :
+ Result (betree.List (U64 × U64))
+ :=
+ match bindings with
+ | betree.List.Cons hd tl =>
+ let (i, i0) := hd
+ if i >= key
+ then Result.ret ret0
+ else
+ do
+ let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
+ Result.ret (betree.List.Cons (i, i0) tl0)
+ | betree.List.Nil => Result.ret ret0
+
+/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) -/
+def betree.Node.apply_to_leaf
+ (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
+ :
+ Result (betree.List (U64 × U64))
+ :=
+ do
+ let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
+ let b ← betree.List.head_has_key U64 bindings0 key
+ if b
+ then
+ do
+ let hd ← betree.List.pop_front (U64 × U64) bindings0
+ match new_msg with
+ | betree.Message.Insert v =>
+ do
+ let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+ let bindings2 ←
+ betree.List.push_front (U64 × U64) bindings1 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings2
+ | betree.Message.Delete =>
+ do
+ let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+ | betree.Message.Upsert s =>
+ do
+ let (_, i) := hd
+ let v ← betree.upsert_update (Option.some i) s
+ let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+ let bindings2 ←
+ betree.List.push_front (U64 × U64) bindings1 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings2
+ else
+ match new_msg with
+ | betree.Message.Insert v =>
+ do
+ let bindings1 ←
+ betree.List.push_front (U64 × U64) bindings0 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+ | betree.Message.Delete =>
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings0
+ | betree.Message.Upsert s =>
+ do
+ let v ← betree.upsert_update Option.none s
+ let bindings1 ←
+ betree.List.push_front (U64 × U64) bindings0 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+
+/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) -/
+divergent def betree.Node.apply_messages_to_leaf
+ (bindings : betree.List (U64 × U64))
+ (new_msgs : betree.List (U64 × betree.Message)) :
+ Result (betree.List (U64 × U64))
+ :=
+ match new_msgs with
+ | betree.List.Cons new_msg new_msgs_tl =>
+ do
+ let (i, m) := new_msg
+ let bindings0 ← betree.Node.apply_to_leaf bindings i m
+ betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
+ | betree.List.Nil => Result.ret bindings
+
+/- [betree_main::betree::Internal::{4}::flush]: forward function -/
+mutual divergent def betree.Internal.flush
+ (self : betree.Internal) (params : betree.Params)
+ (node_id_cnt : betree.NodeIdCounter)
+ (content : betree.List (U64 × betree.Message)) (st : State) :
+ Result (State × (betree.List (U64 × betree.Message)))
+ :=
+ do
+ let ⟨ _, i, n, n0 ⟩ := self
+ let p ← betree.List.partition_at_pivot betree.Message content i
+ let (msgs_left, msgs_right) := p
+ let len_left ← betree.List.len (U64 × betree.Message) msgs_left
+ if len_left >= params.min_flush_size
+ then
+ do
+ let (st0, _) ←
+ betree.Node.apply_messages n params node_id_cnt msgs_left st
+ let (_, node_id_cnt0) ←
+ betree.Node.apply_messages_back n params node_id_cnt msgs_left st
+ let len_right ← betree.List.len (U64 × betree.Message) msgs_right
+ if len_right >= params.min_flush_size
+ then
+ do
+ let (st1, _) ←
+ betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0
+ let _ ←
+ betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
+ st0
+ Result.ret (st1, betree.List.Nil)
+ else Result.ret (st0, msgs_right)
+ else
+ do
+ let (st0, _) ←
+ betree.Node.apply_messages n0 params node_id_cnt msgs_right st
+ let _ ←
+ betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
+ Result.ret (st0, msgs_left)
+
+/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
+divergent def betree.Internal.flush_back
+ (self : betree.Internal) (params : betree.Params)
+ (node_id_cnt : betree.NodeIdCounter)
+ (content : betree.List (U64 × betree.Message)) (st : State) :
+ Result (betree.Internal × betree.NodeIdCounter)
+ :=
+ do
+ let ⟨ i, i0, n, n0 ⟩ := self
+ let p ← betree.List.partition_at_pivot betree.Message content i0
+ let (msgs_left, msgs_right) := p
+ let len_left ← betree.List.len (U64 × betree.Message) msgs_left
+ if len_left >= params.min_flush_size
+ then
+ do
+ let (st0, _) ←
+ betree.Node.apply_messages n params node_id_cnt msgs_left st
+ let (n1, node_id_cnt0) ←
+ betree.Node.apply_messages_back n params node_id_cnt msgs_left st
+ let len_right ← betree.List.len (U64 × betree.Message) msgs_right
+ if len_right >= params.min_flush_size
+ then
+ do
+ let (n2, node_id_cnt1) ←
+ betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
+ st0
+ Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1)
+ else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0)
+ else
+ do
+ let (n1, node_id_cnt0) ←
+ betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
+ Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
+
/- [betree_main::betree::Node::{5}::apply_messages]: forward function -/
-mutual divergent def betree.Node.apply_messages
+divergent def betree.Node.apply_messages
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
(msgs : betree.List (U64 × betree.Message)) (st : State) :
@@ -806,78 +878,6 @@ divergent def betree.Node.apply_messages_back
let _ ← betree.store_leaf_node node.id content0 st0
Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt)
-/- [betree_main::betree::Internal::{4}::flush]: forward function -/
-divergent def betree.Internal.flush
- (self : betree.Internal) (params : betree.Params)
- (node_id_cnt : betree.NodeIdCounter)
- (content : betree.List (U64 × betree.Message)) (st : State) :
- Result (State × (betree.List (U64 × betree.Message)))
- :=
- do
- let ⟨ _, i, n, n0 ⟩ := self
- let p ← betree.List.partition_at_pivot betree.Message content i
- let (msgs_left, msgs_right) := p
- let len_left ← betree.List.len (U64 × betree.Message) msgs_left
- if len_left >= params.min_flush_size
- then
- do
- let (st0, _) ←
- betree.Node.apply_messages n params node_id_cnt msgs_left st
- let (_, node_id_cnt0) ←
- betree.Node.apply_messages_back n params node_id_cnt msgs_left st
- let len_right ← betree.List.len (U64 × betree.Message) msgs_right
- if len_right >= params.min_flush_size
- then
- do
- let (st1, _) ←
- betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0
- let _ ←
- betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
- st0
- Result.ret (st1, betree.List.Nil)
- else Result.ret (st0, msgs_right)
- else
- do
- let (st0, _) ←
- betree.Node.apply_messages n0 params node_id_cnt msgs_right st
- let _ ←
- betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
- Result.ret (st0, msgs_left)
-
-/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
-divergent def betree.Internal.flush_back
- (self : betree.Internal) (params : betree.Params)
- (node_id_cnt : betree.NodeIdCounter)
- (content : betree.List (U64 × betree.Message)) (st : State) :
- Result (betree.Internal × betree.NodeIdCounter)
- :=
- do
- let ⟨ i, i0, n, n0 ⟩ := self
- let p ← betree.List.partition_at_pivot betree.Message content i0
- let (msgs_left, msgs_right) := p
- let len_left ← betree.List.len (U64 × betree.Message) msgs_left
- if len_left >= params.min_flush_size
- then
- do
- let (st0, _) ←
- betree.Node.apply_messages n params node_id_cnt msgs_left st
- let (n1, node_id_cnt0) ←
- betree.Node.apply_messages_back n params node_id_cnt msgs_left st
- let len_right ← betree.List.len (U64 × betree.Message) msgs_right
- if len_right >= params.min_flush_size
- then
- do
- let (n2, node_id_cnt1) ←
- betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
- st0
- Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1)
- else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0)
- else
- do
- let (n1, node_id_cnt0) ←
- betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
- Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
-
end
/- [betree_main::betree::Node::{5}::apply]: forward function -/
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index c02c148a..2f5de6a0 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -28,15 +28,15 @@ structure betree.Leaf where
mutual
+/- [betree_main::betree::Internal] -/
+inductive betree.Internal :=
+| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
+
/- [betree_main::betree::Node] -/
inductive betree.Node :=
| Internal : betree.Internal → betree.Node
| Leaf : betree.Leaf → betree.Node
-/- [betree_main::betree::Internal] -/
-inductive betree.Internal :=
-| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
-
end
/- [betree_main::betree::Params] -/
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 1a180c60..884e62c4 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -251,16 +251,16 @@ def test_char : Result Char :=
mutual
-/- [no_nested_borrows::NodeElem] -/
-inductive NodeElem (T : Type) :=
-| Cons : Tree T → NodeElem T → NodeElem T
-| Nil : NodeElem T
-
/- [no_nested_borrows::Tree] -/
inductive Tree (T : Type) :=
| Leaf : T → Tree T
| Node : T → NodeElem T → Tree T → Tree T
+/- [no_nested_borrows::NodeElem] -/
+inductive NodeElem (T : Type) :=
+| Cons : Tree T → NodeElem T → NodeElem T
+| Nil : NodeElem T
+
end
/- [no_nested_borrows::list_length]: forward function -/