diff options
23 files changed, 1513 insertions, 1495 deletions
@@ -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 -/ |