diff options
45 files changed, 846 insertions, 711 deletions
@@ -54,8 +54,8 @@ SUBDIR := build: format build-dev # Build the project, test it and verify the generated files -.PHONY: build-tests-verify -build-tests-verify: build tests verify +.PHONY: build-test-verify +build-test-verify: build test verify # Build the project, without formatting the code .PHONY: build-dev @@ -64,7 +64,7 @@ You can also use `make test` and `make verify` to run the tests, and check the generated files. As `make test` will run tests which use the Charon tests, you will need to regenerate the `.llbc` files. You have the following options: - run `make test` in the Charon repository -- run `REGEN_LLBC=1 make test` in the Aeneas repository +- run `make test` in the Aeneas repository ## Documentation diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 03b2b045..17810705 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -935,7 +935,11 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) (* Give back the value *) let ctx = give_back config l bc ctx in (* Do a sanity check and continue *) - cf_check cf ctx + let cc = cf_check in + (* Save a snapshot of the environment for the name generation *) + let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in + (* Compose *) + cc cf ctx and end_borrows_aux (config : config) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun = @@ -1041,6 +1045,9 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (* Sanity check: ending an abstraction must preserve the invariants *) let cc = comp cc Invariants.cf_check_invariants in + (* Save a snapshot of the environment for the name generation *) + let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in + (* Apply the continuation *) cc cf ctx diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 95a2956b..6b9f47ce 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -931,9 +931,11 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = ^ statement_to_string_with_tab ctx st ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n")); + (* Take a snapshot of the current context for the purpose of generating pretty names *) + let cc = S.cf_save_snapshot in (* Expand the symbolic values if necessary - we need to do that before * checking the invariants *) - let cc = greedy_expand_symbolic_values config in + let cc = comp cc (greedy_expand_symbolic_values config) in (* Sanity check *) let cc = comp cc Invariants.cf_check_invariants in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index a401594d..00a431a0 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -585,7 +585,7 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) let meta_s = emeta_to_string env meta in let e = texpression_to_string env inside indent indent_incr e in match meta with - | Assignment _ | SymbolicAssignment _ | Tag _ -> + | Assignment _ | SymbolicAssignments _ | SymbolicPlaces _ | Tag _ -> let e = meta_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") @@ -717,10 +717,25 @@ and emeta_to_string (env : fmt_env) (meta : emeta) : string = "@assign(" ^ mplace_to_string env lp ^ " := " ^ texpression_to_string env false "" "" rv ^ rp ^ ")" - | SymbolicAssignment (var_id, rv) -> - "@symb_assign(" ^ VarId.to_string var_id ^ " := " - ^ texpression_to_string env false "" "" rv - ^ ")" + | SymbolicAssignments info -> + let infos = + List.map + (fun (var_id, rv) -> + VarId.to_string var_id ^ " == " + ^ texpression_to_string env false "" "" rv) + info + in + let infos = String.concat ", " infos in + "@symb_assign(" ^ infos ^ ")" + | SymbolicPlaces info -> + let infos = + List.map + (fun (var_id, name) -> + VarId.to_string var_id ^ " == \"" ^ name ^ "\"") + info + in + let infos = String.concat ", " infos in + "@symb_places(" ^ infos ^ ")" | MPlace mp -> "@mplace=" ^ mplace_to_string env mp | Tag msg -> "@tag \"" ^ msg ^ "\"" in diff --git a/compiler/Pure.ml b/compiler/Pure.ml index cf6710aa..7de7e0f4 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -807,12 +807,18 @@ and emeta = The mvalue stores the value which is put in the destination The second (optional) mplace stores the origin. *) - | SymbolicAssignment of (var_id[@opaque]) * mvalue + | SymbolicAssignments of ((var_id[@opaque]) * mvalue) list (** Informationg linking a variable (from the pure AST) to an expression. We use this to guide the heuristics which derive pretty names. *) + | SymbolicPlaces of ((var_id[@opaque]) * string) list + (** Informationg linking a variable (from the pure AST) to a name. + + We generate this information by exploring the context, and use it + to derive pretty names. + *) | MPlace of mplace (** Meta-information about the origin of a value *) | Tag of string (** A tag - typically used for debugging *) [@@deriving diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 1820b86a..a1f6ce33 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -334,6 +334,15 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let ctx1 = obj#visit_typed_pattern () lv () in merge_ctxs ctx ctx1 in + (* If we have [x = y] where x and y are variables, add a constraint linking + the names of x and y *) + let add_eq_var_constraint (lv : typed_pattern) (re : texpression) + (ctx : pn_ctx) : pn_ctx = + match (lv.value, re.e) with + | PatVar (lv, _), Var rv when Option.is_some lv.basename -> + add_pure_var_constraint rv (Option.get lv.basename) ctx + | _ -> ctx + in (* This is used to propagate constraint information about places in case of * variable reassignments: we try to propagate the information from the @@ -428,6 +437,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let ctx, re = update_texpression re ctx in let ctx, e = update_texpression e ctx in let lv = update_typed_pattern ctx lv in + let ctx = add_eq_var_constraint lv re ctx in (ctx, Let (monadic, lv, re, e)) (* *) and update_switch_body (scrut : texpression) (body : switch_body) @@ -524,8 +534,15 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | _ -> ctx in ctx - | SymbolicAssignment (var_id, rvalue) -> - add_pure_var_value_constraint var_id rvalue ctx + | SymbolicAssignments infos -> + List.fold_left + (fun ctx (var_id, rvalue) -> + add_pure_var_value_constraint var_id rvalue ctx) + ctx infos + | SymbolicPlaces infos -> + List.fold_left + (fun ctx (var_id, name) -> add_pure_var_constraint var_id name ctx) + ctx infos | MPlace mp -> add_right_constraint mp e ctx | Tag _ -> ctx in @@ -1075,6 +1092,33 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl = ]} *) let simplify_let_then_return _ctx def = + (* Match a pattern and an expression: evaluates to [true] if the expression + is actually exactly the pattern *) + let rec match_pattern_and_expr (pat : typed_pattern) (e : texpression) : bool + = + match (pat.value, e.e) with + | PatConstant plit, Const lit -> plit = lit + | PatVar (pv, _), Var vid -> pv.id = vid + | PatDummy, _ -> + (* It is ok only if we ignore the unit value *) + pat.ty = mk_unit_ty && e = mk_unit_rvalue + | PatAdt padt, _ -> ( + let qualif, args = destruct_apps e in + match qualif.e with + | Qualif { id = AdtCons cons_id; generics = _ } -> + if + pat.ty = e.ty + && padt.variant_id = cons_id.variant_id + && List.length padt.field_values = List.length args + then + List.for_all + (fun (p, e) -> match_pattern_and_expr p e) + (List.combine padt.field_values args) + else false + | _ -> false) + | _ -> false + in + let expr_visitor = object (self) inherit [_] map_expression @@ -1090,13 +1134,24 @@ let simplify_let_then_return _ctx def = (* Small shortcut to avoid doing the check on every let-binding *) not_simpl_e | _ -> ( - match typed_pattern_to_texpression lv with - | None -> not_simpl_e - | Some lv_v -> - let lv_v = - if monadic then mk_result_return_texpression lv_v else lv_v - in - if lv_v = next_e then rv.e else not_simpl_e) + if (* Do the check *) + monadic then + (* The first let-binding is monadic *) + match opt_destruct_ret next_e with + | Some e -> + if match_pattern_and_expr lv e then rv.e else not_simpl_e + | None -> not_simpl_e + else + (* The first let-binding is not monadic *) + match opt_destruct_ret next_e with + | Some e -> + if match_pattern_and_expr lv e then + (* We need to wrap the right-value in a ret *) + (mk_result_return_texpression rv).e + else not_simpl_e + | None -> + if match_pattern_and_expr lv next_e then rv.e else not_simpl_e + ) end in @@ -1824,6 +1879,14 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl = ("inline_useless_var_assignments (pass 2):\n\n" ^ fun_decl_to_string ctx def ^ "\n")); + (* Simplify the let-then return again (the lambda simplification may have + unlocked more simplifications here) *) + let def = simplify_let_then_return ctx def in + log#ldebug + (lazy + ("simplify_let_then_return (pass 2):\n\n" ^ fun_decl_to_string ctx def + ^ "\n")); + (* Decompose the monadic let-bindings - used by Coq *) let def = if !Config.decompose_monadic_let_bindings then ( diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 80bf3c42..81e3fbe1 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -752,3 +752,21 @@ let opt_dest_struct_pattern (pat : typed_pattern) : typed_pattern list option = match pat.value with | PatAdt { variant_id = None; field_values } -> Some field_values | _ -> None + +(** Destruct a [ret ...] expression *) +let opt_destruct_ret (e : texpression) : texpression option = + match e.e with + | App + ( { + e = + Qualif + { + id = AdtCons { adt_id = TAssumed TResult; variant_id }; + generics = _; + }; + ty = _; + }, + arg ) + when variant_id = Some result_return_id -> + Some arg + | _ -> None diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index cc74a16b..e164fd49 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -65,6 +65,9 @@ type call = { type emeta = | Assignment of Contexts.eval_ctx * mplace * typed_value * mplace option (** We generated an assignment (destination, assigned value, src) *) + | Snapshot of Contexts.eval_ctx + (** Remember an environment snapshot - this is useful to check where the + symbolic values are, to compute proper names for instance *) [@@deriving show] type variant_id = VariantId.id [@@deriving show] diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 58fb6d04..3fa550cc 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1873,10 +1873,48 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) : (** Add meta-information to an expression *) let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list) (e : texpression) : texpression = - let var_values = List.combine vars values in - List.fold_right - (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e) - var_values e + let var_values = List.combine (List.map var_get_id vars) values in + if var_values <> [] then mk_emeta (SymbolicAssignments var_values) e else e + +(** Derive naming information from a context. + + We explore the context and look in which bindings the symbolic values appear: + we use this information to derive naming information. *) +let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) + (ectx : Contexts.eval_ctx) : (VarId.id * string) list = + let info : (VarId.id * string) list ref = ref [] in + let push_info name sv = info := (name, sv) :: !info in + let visitor = + object (self) + inherit [_] Contexts.iter_eval_ctx + + method! visit_env_elem _ ee = + match ee with + | EBinding (BVar { index = _; name = Some name }, v) -> + self#visit_typed_value name v + | _ -> () (* Ignore *) + + method! visit_value name v = + match v with + | VLiteral _ | VBottom -> () + | VBorrow (VMutBorrow (_, v)) | VLoan (VSharedLoan (_, v)) -> + self#visit_typed_value name v + | VSymbolic sv -> + (* Translate the type *) + let ty = ctx_translate_fwd_ty ctx sv.sv_ty in + (* If the type is unit, do nothing *) + if ty_is_unit ty then () + else + (* Otherwise lookup the variable *) + let var = lookup_var_for_symbolic_value sv ctx in + push_info var.id name + | _ -> () + end + in + (* Visit the context *) + visitor#visit_eval_ctx "x" ectx; + (* Return the computed information *) + !info let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with @@ -3528,11 +3566,23 @@ and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) : let lp = translate_mplace lp in let rv = typed_value_to_texpression ctx ectx rv in let rp = translate_opt_mplace rp in - Assignment (lp, rv, rp) - in - let e = Meta (meta, next_e) in - let ty = next_e.ty in - { e; ty } + Some (Assignment (lp, rv, rp)) + | S.Snapshot ectx -> + let infos = eval_ctx_to_symbolic_assignments_info ctx ectx in + if infos <> [] then + (* If often happens that the next expression contains exactly the + same meta information *) + match next_e.e with + | Meta (SymbolicPlaces infos1, _) when infos1 = infos -> None + | _ -> Some (SymbolicPlaces infos) + else None + in + match meta with + | Some meta -> + let e = Meta (meta, next_e) in + let ty = next_e.ty in + { e; ty } + | None -> next_e (** Wrap a function body in a match over the fuel to control termination. *) let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index a42c43ac..ad34c48e 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -189,3 +189,9 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) meta; }) | _ -> raise (Failure "Unreachable") + +let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) : + expression option = + match e with None -> None | Some e -> Some (Meta (Snapshot ctx, e)) + +let cf_save_snapshot : Cps.cm_fun = fun cf ctx -> save_snapshot ctx (cf ctx) @@ -8,11 +8,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1710741599, - "narHash": "sha256-/5o81Ifs6OGqNpxMklGCJ6w2CVQrQn+xMaC1VrC8pZE=", + "lastModified": 1710912772, + "narHash": "sha256-XUZ50NTvfsGoJAfFdjajHwXSIn4Rblutrdwn1y1dB7E=", "owner": "aeneasverif", "repo": "charon", - "rev": "f3faf02ec1dbd6645b816d54be39261dea6970c2", + "rev": "0db6709ef5b7952730ed3b0df3e79508b2cf33ad", "type": "github" }, "original": { @@ -83,11 +83,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1710514291, - "narHash": "sha256-eO3XmWazqfmSm91sQDk0HJNyLpsU5W6BgeftXoJSUl0=", + "lastModified": 1710871305, + "narHash": "sha256-4bqvrVXX8JVlvswJx9apdVJu/HvoAEVsYxGI8IZt14s=", "owner": "fstarlang", "repo": "fstar", - "rev": "704382c882f3b5b95f7987d3464f97020195319b", + "rev": "41299bb12072a7475c036262b9851f7cdc287387", "type": "github" }, "original": { @@ -116,11 +116,11 @@ ] }, "locked": { - "lastModified": 1710421079, - "narHash": "sha256-iXmFy2/JmS3khP4V3zIg1P4SROq0sPPuqOxRidJbfqQ=", + "lastModified": 1710781424, + "narHash": "sha256-hiS8rXXzF4N3QzopIYuiNR0F+eaajY7CV2xH6Ga23h4=", "owner": "hacl-star", "repo": "hacl-star", - "rev": "e5620ceb7c8a4996520d693f597872806dc0a1d3", + "rev": "3b0f36da380ce71f00d057432bbac6a58e60b329", "type": "github" }, "original": { @@ -146,11 +146,11 @@ ] }, "locked": { - "lastModified": 1710638129, - "narHash": "sha256-/SkIjiIg0MROfmYyA8XfWljRC4ehxDuZpE3tDQ07yYc=", + "lastModified": 1710897170, + "narHash": "sha256-b+/z6DJbLIHU4CzslZIQAzeMqxZUubhMrcur0J+rDL0=", "owner": "hacl-star", "repo": "hacl-nix", - "rev": "cc8c396d454e89c04012cf3b16eb6f64eb455bd6", + "rev": "8212076565dc408b564708df1872abdf1454f861", "type": "github" }, "original": { @@ -175,11 +175,11 @@ ] }, "locked": { - "lastModified": 1710613474, - "narHash": "sha256-C1y575wlUVaI3AlTMZvMYpie6mSLUmiQDXasaHqKo6o=", + "lastModified": 1710895334, + "narHash": "sha256-HZPu64k7e8Ah429ijQu306IwaN/yspRj6zxtzvYKGnU=", "owner": "fstarlang", "repo": "karamel", - "rev": "95968326f0ca1d6f9056347496482d285e6a9f1e", + "rev": "5a9cbe1d7d3f82760450b7a4bde8e4736b82d7ce", "type": "github" }, "original": { diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index 34d163b7..049d63cb 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -30,27 +30,25 @@ Definition array_to_mut_slice_ (T : Type) (s : array T 32%usize) : result ((slice T) * (slice T -> result (array T 32%usize))) := - p <- array_to_slice_mut T 32%usize s; - let (s1, to_slice_mut_back) := p in - Return (s1, to_slice_mut_back) + array_to_slice_mut T 32%usize s . (** [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 *) Definition array_len (T : Type) (s : array T 32%usize) : result usize := - s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i + s1 <- array_to_slice T 32%usize s; Return (slice_len T s1) . (** [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 *) Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize := - s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i + s1 <- array_to_slice T 32%usize s; Return (slice_len T s1) . (** [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 *) Definition shared_slice_len (T : Type) (s : slice T) : result usize := - let i := slice_len T s in Return i + Return (slice_len T s) . (** [arrays::index_array_shared]: @@ -78,9 +76,7 @@ Definition index_mut_array (T : Type) (s : array T 32%usize) (i : usize) : result (T * (T -> result (array T 32%usize))) := - p <- array_index_mut_usize T 32%usize s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) + array_index_mut_usize T 32%usize s i . (** [arrays::index_slice]: @@ -95,9 +91,7 @@ Definition index_mut_slice (T : Type) (s : slice T) (i : usize) : result (T * (T -> result (slice T))) := - p <- slice_index_mut_usize T s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) + slice_index_mut_usize T s i . (** [arrays::slice_subslice_shared_]: @@ -136,9 +130,7 @@ Definition array_to_slice_mut_ (x : array u32 32%usize) : result ((slice u32) * (slice u32 -> result (array u32 32%usize))) := - p <- array_to_slice_mut u32 32%usize x; - let (s, to_slice_mut_back) := p in - Return (s, to_slice_mut_back) + array_to_slice_mut u32 32%usize x . (** [arrays::array_subslice_shared_]: @@ -334,8 +326,8 @@ Definition update_mut_slice (x : slice u32) : result (slice u32) := Definition update_all : result unit := _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - a <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - p <- array_to_slice_mut u32 2%usize a; + x <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + p <- array_to_slice_mut u32 2%usize x; let (s, to_slice_mut_back) := p in s1 <- update_mut_slice s; _ <- to_slice_mut_back s1; @@ -381,7 +373,7 @@ Definition take_array_t (a : array AB_t 2%usize) : result unit := (** [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 *) Definition non_copyable_array : result unit := - _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt + take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]) . (** [arrays::sum]: loop 0: @@ -548,8 +540,7 @@ Fixpoint iter_mut_slice_loop | O => Fail_ OutOfFuel | S n1 => if i s< len - then ( - i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt) + then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1) else Return tt end . diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 3863a90f..c2cca26d 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -27,9 +27,7 @@ Definition betree_store_internal_node (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : result (state * unit) := - p <- betree_utils_store_internal_node id content st; - let (st1, _) := p in - Return (st1, tt) + betree_utils_store_internal_node id content st . (** [betree_main::betree::load_leaf_node]: @@ -45,9 +43,7 @@ Definition betree_store_leaf_node (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : result (state * unit) := - p <- betree_utils_store_leaf_node id content st; - let (st1, _) := p in - Return (st1, tt) + betree_utils_store_leaf_node id content st . (** [betree_main::betree::fresh_node_id]: @@ -205,9 +201,9 @@ Definition betree_Leaf_split p1 <- betree_List_hd (u64 * u64) content1; let (pivot, _) := p1 in p2 <- betree_NodeIdCounter_fresh_id node_id_cnt; - let (id0, nic) := p2 in - p3 <- betree_NodeIdCounter_fresh_id nic; - let (id1, nic1) := p3 in + let (id0, node_id_cnt1) := p2 in + p3 <- betree_NodeIdCounter_fresh_id node_id_cnt1; + let (id1, node_id_cnt2) := p3 in p4 <- betree_store_leaf_node id0 content0 st; let (st1, _) := p4 in p5 <- betree_store_leaf_node id1 content1 st1; @@ -222,7 +218,8 @@ Definition betree_Leaf_split betree_Leaf_id := id1; betree_Leaf_size := params.(betree_Params_split_size) |} in - Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, nic1)) + Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, + node_id_cnt2)) . (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: @@ -290,22 +287,22 @@ Fixpoint betree_Node_apply_upserts if b then ( p <- betree_List_pop_front (u64 * betree_Message_t) msgs; - let (msg, l) := p in + let (msg, msgs1) := p in let (_, m) := msg in match m with | Betree_Message_Insert _ => Fail_ Failure | Betree_Message_Delete => Fail_ Failure | Betree_Message_Upsert s => v <- betree_upsert_update prev s; - betree_Node_apply_upserts n1 l (Some v) key st + betree_Node_apply_upserts n1 msgs1 (Some v) key st end) else ( p <- core_option_Option_unwrap u64 prev st; let (st1, v) := p in - l <- + msgs1 <- betree_List_push_front (u64 * betree_Message_t) msgs (key, Betree_Message_Insert v); - Return (st1, (v, l))) + Return (st1, (v, msgs1))) end . @@ -355,9 +352,9 @@ with betree_Node_lookup then ( p3 <- betree_Internal_lookup_in_children n1 node key st1; let (st2, p4) := p3 in - let (o, i) := p4 in + let (o, node1) := p4 in _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l); - Return (st2, (o, Betree_Node_Internal i))) + Return (st2, (o, Betree_Node_Internal node1))) else match msg with | Betree_Message_Insert v => @@ -373,23 +370,24 @@ with betree_Node_lookup | Betree_Message_Upsert ufs => p3 <- betree_Internal_lookup_in_children n1 node key st1; let (st2, p4) := p3 in - let (v, i) := p4 in + let (v, node1) := p4 in p5 <- betree_Node_apply_upserts n1 (Betree_List_Cons (k, Betree_Message_Upsert ufs) l) v key st2; let (st3, p6) := p5 in - let (v1, l1) := p6 in - msgs1 <- lookup_first_message_for_key_back l1; - p7 <- betree_store_internal_node i.(betree_Internal_id) msgs1 st3; + let (v1, pending1) := p6 in + msgs1 <- lookup_first_message_for_key_back pending1; + p7 <- + betree_store_internal_node node1.(betree_Internal_id) msgs1 st3; let (st4, _) := p7 in - Return (st4, (Some v1, Betree_Node_Internal i)) + Return (st4, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil => p2 <- betree_Internal_lookup_in_children n1 node key st1; let (st2, p3) := p2 in - let (o, i) := p3 in + let (o, node1) := p3 in _ <- lookup_first_message_for_key_back Betree_List_Nil; - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) end | Betree_Node_Leaf node => p <- betree_load_leaf_node node.(betree_Leaf_id) st; @@ -417,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key p1 <- betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k, m) l); - let (_, l1) := p1 in - betree_Node_filter_messages_for_key n1 key l1) + let (_, msgs1) := p1 in + betree_Node_filter_messages_for_key n1 key msgs1) else Return (Betree_List_Cons (k, m) l) | Betree_List_Nil => Return Betree_List_Nil end @@ -467,17 +465,17 @@ Definition betree_Node_apply_to_internal then match new_msg with | Betree_Message_Insert i => - l <- betree_Node_filter_messages_for_key n key msgs1; - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + msgs2 <- betree_Node_filter_messages_for_key n key msgs1; + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Insert i); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete => - l <- betree_Node_filter_messages_for_key n key msgs1; - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + msgs2 <- betree_Node_filter_messages_for_key n key msgs1; + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Delete); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert s => p1 <- betree_List_hd (u64 * betree_Message_t) msgs1; let (_, m) := p1 in @@ -485,32 +483,33 @@ Definition betree_Node_apply_to_internal | Betree_Message_Insert prev => v <- betree_upsert_update (Some prev) s; p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; - let (_, l) := p2 in - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + let (_, msgs2) := p2 in + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Insert v); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete => p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; - let (_, l) := p2 in + let (_, msgs2) := p2 in v <- betree_upsert_update None s; - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Insert v); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert _ => p2 <- betree_Node_lookup_first_message_after_key n key msgs1; let (msgs2, lookup_first_message_after_key_back) := p2 in - l <- + msgs3 <- betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Upsert s); - msgs3 <- lookup_first_message_after_key_back l; - lookup_first_message_for_key_back msgs3 + msgs4 <- lookup_first_message_after_key_back msgs3; + lookup_first_message_for_key_back msgs4 end end else ( - l <- betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg); - lookup_first_message_for_key_back l) + msgs2 <- + betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg); + lookup_first_message_for_key_back msgs2) . (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: @@ -526,8 +525,8 @@ Fixpoint betree_Node_apply_messages_to_internal match new_msgs with | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in - l <- betree_Node_apply_to_internal n1 msgs i m; - betree_Node_apply_messages_to_internal n1 l new_msgs_tl + msgs1 <- betree_Node_apply_to_internal n1 msgs i m; + betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl | Betree_List_Nil => Return msgs end end @@ -574,28 +573,28 @@ Definition betree_Node_apply_to_leaf if b then ( p1 <- betree_List_pop_front (u64 * u64) bindings1; - let (hd, l) := p1 in + let (hd, bindings2) := p1 in match new_msg with | Betree_Message_Insert v => - l1 <- betree_List_push_front (u64 * u64) l (key, v); - lookup_mut_in_bindings_back l1 - | Betree_Message_Delete => lookup_mut_in_bindings_back l + bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete => lookup_mut_in_bindings_back bindings2 | Betree_Message_Upsert s => let (_, i) := hd in v <- betree_upsert_update (Some i) s; - l1 <- betree_List_push_front (u64 * u64) l (key, v); - lookup_mut_in_bindings_back l1 + bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); + lookup_mut_in_bindings_back bindings3 end) else match new_msg with | Betree_Message_Insert v => - l <- betree_List_push_front (u64 * u64) bindings1 (key, v); - lookup_mut_in_bindings_back l + bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back bindings2 | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1 | Betree_Message_Upsert s => v <- betree_upsert_update None s; - l <- betree_List_push_front (u64 * u64) bindings1 (key, v); - lookup_mut_in_bindings_back l + bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back bindings2 end . @@ -612,8 +611,8 @@ Fixpoint betree_Node_apply_messages_to_leaf match new_msgs with | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in - l <- betree_Node_apply_to_leaf n1 bindings i m; - betree_Node_apply_messages_to_leaf n1 l new_msgs_tl + bindings1 <- betree_Node_apply_to_leaf n1 bindings i m; + betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl | Betree_List_Nil => Return bindings end end @@ -684,38 +683,39 @@ with betree_Node_apply_messages | Betree_Node_Internal node => p <- betree_load_internal_node node.(betree_Internal_id) st; let (st1, content) := p in - l <- betree_Node_apply_messages_to_internal n1 content msgs; - num_msgs <- betree_List_len (u64 * betree_Message_t) n1 l; + content1 <- betree_Node_apply_messages_to_internal n1 content msgs; + num_msgs <- betree_List_len (u64 * betree_Message_t) n1 content1; if num_msgs s>= params.(betree_Params_min_flush_size) then ( - p1 <- betree_Internal_flush n1 node params node_id_cnt l st1; + p1 <- betree_Internal_flush n1 node params node_id_cnt content1 st1; let (st2, p2) := p1 in - let (content1, p3) := p2 in + let (content2, p3) := p2 in let (node1, node_id_cnt1) := p3 in p4 <- - betree_store_internal_node node1.(betree_Internal_id) content1 st2; + betree_store_internal_node node1.(betree_Internal_id) content2 st2; let (st3, _) := p4 in Return (st3, (Betree_Node_Internal node1, node_id_cnt1))) else ( - p1 <- betree_store_internal_node node.(betree_Internal_id) l st1; + p1 <- + betree_store_internal_node node.(betree_Internal_id) content1 st1; let (st2, _) := p1 in Return (st2, (Betree_Node_Internal node, node_id_cnt))) | Betree_Node_Leaf node => p <- betree_load_leaf_node node.(betree_Leaf_id) st; let (st1, content) := p in - l <- betree_Node_apply_messages_to_leaf n1 content msgs; - len <- betree_List_len (u64 * u64) n1 l; + content1 <- betree_Node_apply_messages_to_leaf n1 content msgs; + len <- betree_List_len (u64 * u64) n1 content1; i <- u64_mul 2%u64 params.(betree_Params_split_size); if len s>= i then ( - p1 <- betree_Leaf_split n1 node l params node_id_cnt st1; + p1 <- betree_Leaf_split n1 node content1 params node_id_cnt st1; let (st2, p2) := p1 in - let (new_node, nic) := p2 in + let (new_node, node_id_cnt1) := p2 in p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2; let (st3, _) := p3 in - Return (st3, (Betree_Node_Internal new_node, nic))) + Return (st3, (Betree_Node_Internal new_node, node_id_cnt1))) else ( - p1 <- betree_store_leaf_node node.(betree_Leaf_id) l st1; + p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1; let (st2, _) := p1 in Return (st2, (Betree_Node_Leaf {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len @@ -748,7 +748,7 @@ Definition betree_BeTree_new := node_id_cnt <- betree_NodeIdCounter_new; p <- betree_NodeIdCounter_fresh_id node_id_cnt; - let (id, nic) := p in + let (id, node_id_cnt1) := p in p1 <- betree_store_leaf_node id Betree_List_Nil st; let (st1, _) := p1 in Return (st1, @@ -758,7 +758,7 @@ Definition betree_BeTree_new betree_Params_min_flush_size := min_flush_size; betree_Params_split_size := split_size |}; - betree_BeTree_node_id_cnt := nic; + betree_BeTree_node_id_cnt := node_id_cnt1; betree_BeTree_root := (Betree_Node_Leaf {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |}) diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index 13e4b9c1..b14bed66 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -3,8 +3,8 @@ -arg -w -arg all -BetreeMain_Types.v BetreeMain_TypesExternal_Template.v +BetreeMain_Types.v Primitives.v BetreeMain_FunsExternal_Template.v BetreeMain_Funs.v diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index ec7ca29d..d5a6e535 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -34,8 +34,14 @@ Definition use_mul2_add1 (x : u32) (y : u32) : result u32 := Definition incr (x : u32) : result u32 := u32_add x 1%u32. +(** [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 *) +Definition use_incr : result unit := + x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt +. + (** [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 *) + Source: 'src/demo.rs', lines 34:0-34:17 *) Inductive CList_t (T : Type) := | CList_CCons : T -> CList_t T -> CList_t T | CList_CNil : CList_t T @@ -45,7 +51,7 @@ Arguments CList_CCons { _ }. Arguments CList_CNil { _ }. (** [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 *) + Source: 'src/demo.rs', lines 39:0-39:56 *) Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T := match n with | O => Fail_ OutOfFuel @@ -61,7 +67,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T := . (** [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 *) + Source: 'src/demo.rs', lines 54:0-54:68 *) Fixpoint list_nth_mut (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) @@ -89,7 +95,7 @@ Fixpoint list_nth_mut . (** [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 *) + Source: 'src/demo.rs', lines 69:0-78:1 *) Fixpoint list_nth_mut1_loop (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) @@ -116,16 +122,16 @@ Fixpoint list_nth_mut1_loop . (** [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 *) + Source: 'src/demo.rs', lines 69:0-69:77 *) Definition list_nth_mut1 (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) := - p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a) + list_nth_mut1_loop T n l i . (** [demo::i32_id]: - Source: 'src/demo.rs', lines 73:0-73:28 *) + Source: 'src/demo.rs', lines 80:0-80:28 *) Fixpoint i32_id (n : nat) (i : i32) : result i32 := match n with | O => Fail_ OutOfFuel @@ -136,8 +142,30 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 := end . +(** [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 *) +Fixpoint list_tail + (T : Type) (n : nat) (l : CList_t T) : + result ((CList_t T) * (CList_t T -> result (CList_t T))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match l with + | CList_CCons t tl => + p <- list_tail T n1 tl; + let (c, list_tail_back) := p in + let back_'a := + fun (ret : CList_t T) => + tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in + Return (c, back_'a) + | CList_CNil => Return (CList_CNil, Return) + end + end +. + (** Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 *) + Source: 'src/demo.rs', lines 97:0-97:17 *) Record Counter_t (Self : Type) := mkCounter_t { Counter_t_incr : Self -> result (usize * Self); }. @@ -146,19 +174,19 @@ Arguments mkCounter_t { _ }. Arguments Counter_t_incr { _ }. (** [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 *) + Source: 'src/demo.rs', lines 102:4-102:31 *) Definition counterUsize_incr (self : usize) : result (usize * usize) := self1 <- usize_add self 1%usize; Return (self, self1) . (** Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 *) + Source: 'src/demo.rs', lines 101:0-101:22 *) Definition CounterUsize : Counter_t usize := {| Counter_t_incr := counterUsize_incr; |}. (** [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 *) + Source: 'src/demo.rs', lines 109:0-109:59 *) Definition use_counter (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) := counterInst.(Counter_t_incr) cnt diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 0478edbe..d709a8d5 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -26,9 +26,9 @@ Fixpoint hashMap_allocate_slots_loop | S n2 => if n1 s> 0%usize then ( - v <- alloc_vec_Vec_push (List_t T) slots List_Nil; + slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil; n3 <- usize_sub n1 1%usize; - hashMap_allocate_slots_loop T n2 v n3) + hashMap_allocate_slots_loop T n2 slots1 n3) else Return slots end . @@ -190,8 +190,8 @@ Fixpoint hashMap_move_elements_from_list_loop | S n1 => match ls with | List_Cons k v tl => - hm <- hashMap_insert_no_resize T n1 ntable k v; - hashMap_move_elements_from_list_loop T n1 hm tl + ntable1 <- hashMap_insert_no_resize T n1 ntable k v; + hashMap_move_elements_from_list_loop T n1 ntable1 tl | List_Nil => Return ntable end end @@ -224,12 +224,10 @@ Fixpoint hashMap_move_elements_loop (core_slice_index_SliceIndexUsizeSliceTInst (List_t T)) slots i; let (l, index_mut_back) := p in let (ls, l1) := core_mem_replace (List_t T) l List_Nil in - hm <- hashMap_move_elements_from_list T n1 ntable ls; + ntable1 <- hashMap_move_elements_from_list T n1 ntable ls; i2 <- usize_add i 1%usize; slots1 <- index_mut_back l1; - back_'a <- hashMap_move_elements_loop T n1 hm slots1 i2; - let (hm1, v) := back_'a in - Return (hm1, v)) + hashMap_move_elements_loop T n1 ntable1 slots1 i2) else Return (ntable, slots) end . @@ -241,9 +239,7 @@ Definition hashMap_move_elements (slots : alloc_vec_Vec (List_t T)) (i : usize) : result ((HashMap_t T) * (alloc_vec_Vec (List_t T))) := - back_'a <- hashMap_move_elements_loop T n ntable slots i; - let (hm, v) := back_'a in - Return (hm, v) + hashMap_move_elements_loop T n ntable slots i . (** [hashmap::{hashmap::HashMap<T>}::try_resize]: @@ -284,9 +280,11 @@ Definition hashMap_insert (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) : result (HashMap_t T) := - hm <- hashMap_insert_no_resize T n self key value; - i <- hashMap_len T hm; - if i s> hm.(hashMap_max_load) then hashMap_try_resize T n hm else Return hm + self1 <- hashMap_insert_no_resize T n self key value; + i <- hashMap_len T self1; + if i s> self1.(hashMap_max_load) + then hashMap_try_resize T n self1 + else Return self1 . (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0: @@ -398,9 +396,7 @@ Definition hashMap_get_mut_in_list (T : Type) (n : nat) (ls : List_t T) (key : usize) : result (T * (T -> result (List_t T))) := - p <- hashMap_get_mut_in_list_loop T n ls key; - let (t, back_'a) := p in - Return (t, back_'a) + hashMap_get_mut_in_list_loop T n ls key . (** [hashmap::{hashmap::HashMap<T>}::get_mut]: diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 6a7eeb2d..9fb3c482 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -29,9 +29,9 @@ Fixpoint hashmap_HashMap_allocate_slots_loop | S n2 => if n1 s> 0%usize then ( - v <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil; + slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil; n3 <- usize_sub n1 1%usize; - hashmap_HashMap_allocate_slots_loop T n2 v n3) + hashmap_HashMap_allocate_slots_loop T n2 slots1 n3) else Return slots end . @@ -204,8 +204,8 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop | S n1 => match ls with | Hashmap_List_Cons k v tl => - hm <- hashmap_HashMap_insert_no_resize T n1 ntable k v; - hashmap_HashMap_move_elements_from_list_loop T n1 hm tl + ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v; + hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl | Hashmap_List_Nil => Return ntable end end @@ -239,12 +239,10 @@ Fixpoint hashmap_HashMap_move_elements_loop i; let (l, index_mut_back) := p in let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in - hm <- hashmap_HashMap_move_elements_from_list T n1 ntable ls; + ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls; i2 <- usize_add i 1%usize; slots1 <- index_mut_back l1; - back_'a <- hashmap_HashMap_move_elements_loop T n1 hm slots1 i2; - let (hm1, v) := back_'a in - Return (hm1, v)) + hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2) else Return (ntable, slots) end . @@ -256,9 +254,7 @@ Definition hashmap_HashMap_move_elements (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T))) := - back_'a <- hashmap_HashMap_move_elements_loop T n ntable slots i; - let (hm, v) := back_'a in - Return (hm, v) + hashmap_HashMap_move_elements_loop T n ntable slots i . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: @@ -304,11 +300,11 @@ Definition hashmap_HashMap_insert (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : result (hashmap_HashMap_t T) := - hm <- hashmap_HashMap_insert_no_resize T n self key value; - i <- hashmap_HashMap_len T hm; - if i s> hm.(hashmap_HashMap_max_load) - then hashmap_HashMap_try_resize T n hm - else Return hm + self1 <- hashmap_HashMap_insert_no_resize T n self key value; + i <- hashmap_HashMap_len T self1; + if i s> self1.(hashmap_HashMap_max_load) + then hashmap_HashMap_try_resize T n self1 + else Return self1 . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: @@ -423,9 +419,7 @@ Definition hashmap_HashMap_get_mut_in_list (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : result (T * (T -> result (hashmap_List_t T))) := - p <- hashmap_HashMap_get_mut_in_list_loop T n ls key; - let (t, back_'a) := p in - Return (t, back_'a) + hashmap_HashMap_get_mut_in_list_loop T n ls key . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: @@ -585,9 +579,7 @@ Definition insert_on_disk p <- hashmap_utils_deserialize st; let (st1, hm) := p in hm1 <- hashmap_HashMap_insert u64 n hm key value; - p1 <- hashmap_utils_serialize hm1 st1; - let (st2, _) := p1 in - Return (st2, tt) + hashmap_utils_serialize hm1 st1 . (** [hashmap_main::main]: diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject index 41945494..d73541d9 100644 --- a/tests/coq/hashmap_on_disk/_CoqProject +++ b/tests/coq/hashmap_on_disk/_CoqProject @@ -4,9 +4,9 @@ -arg all HashmapMain_Types.v +HashmapMain_FunsExternal_Template.v Primitives.v HashmapMain_Funs.v HashmapMain_TypesExternal.v -HashmapMain_FunsExternal_Template.v HashmapMain_FunsExternal.v HashmapMain_TypesExternal_Template.v diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 91ea88c9..faf91fef 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -45,9 +45,9 @@ Definition custom_swap := p <- core_mem_swap T x y st; let (st1, p1) := p in - let (t, t1) := p1 in - let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, t1)) in - Return (st1, (t, back_'a)) + let (x1, y1) := p1 in + let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in + Return (st1, (x1, back_'a)) . (** [external::test_custom_swap]: diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index e235b60d..7c83a014 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 := (** [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 *) Fixpoint sum_with_mut_borrows_loop - (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := + (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel | S n1 => - if mi s< max + if i s< max then ( - ms1 <- u32_add ms mi; - mi1 <- u32_add mi 1%u32; - sum_with_mut_borrows_loop n1 max mi1 ms1) - else u32_mul ms 2%u32 + ms <- u32_add s i; + mi <- u32_add i 1%u32; + sum_with_mut_borrows_loop n1 max mi ms) + else u32_mul s 2%u32 end . @@ -183,7 +183,7 @@ Definition list_nth_mut_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result (T * (T -> result (List_t T))) := - p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back) + list_nth_mut_loop_loop T n ls i . (** [loops::list_nth_shared_loop]: loop 0: @@ -245,10 +245,10 @@ Definition get_elem_mut p <- alloc_vec_Vec_index_mut (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - let (l, index_mut_back) := p in - p1 <- get_elem_mut_loop n x l; + let (ls, index_mut_back) := p in + p1 <- get_elem_mut_loop n x ls; let (i, back) := p1 in - let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in + let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in Return (i, back1) . @@ -273,10 +273,10 @@ Definition get_elem_shared (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) : result usize := - l <- + ls <- alloc_vec_Vec_index (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - get_elem_shared_loop n x l + get_elem_shared_loop n x ls . (** [loops::id_mut]: @@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T))) := - t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i; - let '(p, back_'a, back_'b) := t in - Return (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair]: loop 0: @@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T)))) := - p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair_merge]: loop 0: @@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: @@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair]: loop 0: @@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'b) := p in - Return (p1, back_'b) + list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: @@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::ignore_input_mut_borrow]: loop 0: @@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt) + then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; - _ <- incr_ignore_input_mut_borrow_loop n1 i1; - Return tt) + then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; - _ <- ignore_input_shared_borrow_loop n1 i1; - Return tt) + then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1) else Return tt end . diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 73c4ee58..76dc4cf6 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -475,9 +475,7 @@ Definition id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) := - let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1) - in - Return ((x, y), back_'a) + Return ((x, y), Return) . (** [no_nested_borrows::id_mut_pair2]: @@ -486,10 +484,7 @@ Definition id_mut_pair2 (T1 T2 : Type) (p : (T1 * T2)) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) := - let (t, t1) := p in - let back_'a := - fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in - Return ((t, t1), back_'a) + let (t, t1) := p in Return ((t, t1), Return) . (** [no_nested_borrows::id_mut_pair3]: diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 769cf34c..ad77fa2a 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 := (** [paper::test_incr]: Source: 'src/paper.rs', lines 8:0-8:18 *) Definition test_incr : result unit := - i <- ref_incr 0%i32; if negb (i s= 1%i32) then Fail_ Failure else Return tt + x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt . (** Unit test for [paper::test_incr] *) diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 869cdb4d..308de4f4 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -3,6 +3,7 @@ -arg -w -arg all +External_FunsExternal_Template.v Loops.v External_Types.v Primitives.v @@ -10,9 +11,8 @@ External_Funs.v External_TypesExternal.v Constants.v PoloniusList.v -Paper.v NoNestedBorrows.v External_FunsExternal.v Bitwise.v External_TypesExternal_Template.v -External_FunsExternal_Template.v +Paper.v diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst index cf0f4f8b..731c7290 100644 --- a/tests/fstar/arrays/Arrays.Funs.fst +++ b/tests/fstar/arrays/Arrays.Funs.fst @@ -23,23 +23,22 @@ let array_to_mut_slice_ (t : Type0) (s : array t 32) : result ((slice t) & (slice t -> result (array t 32))) = - let* (s1, to_slice_mut_back) = array_to_slice_mut t 32 s in - Return (s1, to_slice_mut_back) + array_to_slice_mut t 32 s (** [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 *) let array_len (t : Type0) (s : array t 32) : result usize = - let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i + let* s1 = array_to_slice t 32 s in Return (slice_len t s1) (** [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 *) let shared_array_len (t : Type0) (s : array t 32) : result usize = - let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i + let* s1 = array_to_slice t 32 s in Return (slice_len t s1) (** [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 *) let shared_slice_len (t : Type0) (s : slice t) : result usize = - let i = slice_len t s in Return i + Return (slice_len t s) (** [arrays::index_array_shared]: Source: 'src/arrays.rs', lines 37:0-37:57 *) @@ -62,8 +61,7 @@ let index_mut_array (t : Type0) (s : array t 32) (i : usize) : result (t & (t -> result (array t 32))) = - let* (x, index_mut_back) = array_index_mut_usize t 32 s i in - Return (x, index_mut_back) + array_index_mut_usize t 32 s i (** [arrays::index_slice]: Source: 'src/arrays.rs', lines 56:0-56:46 *) @@ -76,8 +74,7 @@ let index_mut_slice (t : Type0) (s : slice t) (i : usize) : result (t & (t -> result (slice t))) = - let* (x, index_mut_back) = slice_index_mut_usize t s i in - Return (x, index_mut_back) + slice_index_mut_usize t s i (** [arrays::slice_subslice_shared_]: Source: 'src/arrays.rs', lines 64:0-64:70 *) @@ -110,8 +107,7 @@ let array_to_slice_mut_ (x : array u32 32) : result ((slice u32) & (slice u32 -> result (array u32 32))) = - let* (s, to_slice_mut_back) = array_to_slice_mut u32 32 x in - Return (s, to_slice_mut_back) + array_to_slice_mut u32 32 x (** [arrays::array_subslice_shared_]: Source: 'src/arrays.rs', lines 80:0-80:74 *) @@ -272,8 +268,8 @@ let update_mut_slice (x : slice u32) : result (slice u32) = let update_all : result unit = let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in - let* a = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in - let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 a in + let* x = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in + let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 x in let* s1 = update_mut_slice s in let* _ = to_slice_mut_back s1 in Return () @@ -308,7 +304,7 @@ let take_array_t (a : array aB_t 2) : result unit = (** [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 *) let non_copyable_array : result unit = - let* _ = take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) in Return () + take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) (** [arrays::sum]: loop 0: Source: 'src/arrays.rs', lines 242:0-250:1 *) @@ -444,8 +440,7 @@ let rec iter_mut_slice_loop Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i)) = if i < len - then - let* i1 = usize_add i 1 in let* _ = iter_mut_slice_loop len i1 in Return () + then let* i1 = usize_add i 1 in iter_mut_slice_loop len i1 else Return () (** [arrays::iter_mut_slice]: diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index ec042fb3..2469f98c 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -22,8 +22,7 @@ let betree_store_internal_node (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_internal_node id content st in - Return (st1, ()) + betree_utils_store_internal_node id content st (** [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) @@ -37,8 +36,7 @@ let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_leaf_node id content st in - Return (st1, ()) + betree_utils_store_leaf_node id content st (** [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) @@ -172,13 +170,14 @@ let betree_Leaf_split let (content0, content1) = p in let* p1 = betree_List_hd (u64 & u64) content1 in let (pivot, _) = p1 in - let* (id0, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (id1, nic1) = betree_NodeIdCounter_fresh_id nic in + let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in let* (st1, _) = betree_store_leaf_node id0 content0 st in let* (st2, _) = betree_store_leaf_node id1 content1 st1 in let n = Betree_Node_Leaf { id = id0; size = params.split_size } in let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in - Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, nic1)) + Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, + node_id_cnt2)) (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 *) @@ -231,21 +230,21 @@ let rec betree_Node_apply_upserts let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b then - let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in + let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in let (_, m) = msg in begin match m with | Betree_Message_Insert _ -> Fail Failure | Betree_Message_Delete -> Fail Failure | Betree_Message_Upsert s -> let* v = betree_upsert_update prev s in - betree_Node_apply_upserts l (Some v) key st + betree_Node_apply_upserts msgs1 (Some v) key st end else let* (st1, v) = core_option_Option_unwrap u64 prev st in - let* l = + let* msgs1 = betree_List_push_front (u64 & betree_Message_t) msgs (key, Betree_Message_Insert v) in - Return (st1, (v, l)) + Return (st1, (v, msgs1)) (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) @@ -279,10 +278,11 @@ and betree_Node_lookup let (k, msg) = p in if k <> key then - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = + betree_Internal_lookup_in_children node key st1 in let* _ = lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) else begin match msg with | Betree_Message_Insert v -> @@ -296,19 +296,20 @@ and betree_Node_lookup Betree_Message_Delete) l) in Return (st1, (None, Betree_Node_Internal node)) | Betree_Message_Upsert ufs -> - let* (st2, (v, i)) = betree_Internal_lookup_in_children node key st1 - in - let* (st3, (v1, l1)) = + let* (st2, (v, node1)) = + betree_Internal_lookup_in_children node key st1 in + let* (st3, (v1, pending1)) = betree_Node_apply_upserts (Betree_List_Cons (k, Betree_Message_Upsert ufs) l) v key st2 in - let* msgs1 = lookup_first_message_for_key_back l1 in - let* (st4, _) = betree_store_internal_node i.id msgs1 st3 in - Return (st4, (Some v1, Betree_Node_Internal i)) + let* msgs1 = lookup_first_message_for_key_back pending1 in + let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in + Return (st4, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil -> - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 + in let* _ = lookup_first_message_for_key_back Betree_List_Nil in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) end | Betree_Node_Leaf node -> let* (st1, bindings) = betree_load_leaf_node node.id st in @@ -328,10 +329,10 @@ let rec betree_Node_filter_messages_for_key let (k, m) = p in if k = key then - let* (_, l1) = + let* (_, msgs1) = betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m) l) in - betree_Node_filter_messages_for_key key l1 + betree_Node_filter_messages_for_key key msgs1 else Return (Betree_List_Cons (k, m) l) | Betree_List_Nil -> Return Betree_List_Nil end @@ -374,49 +375,51 @@ let betree_Node_apply_to_internal then begin match new_msg with | Betree_Message_Insert i -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert i) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Delete) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert s -> let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in let (_, m) = p in begin match m with | Betree_Message_Insert prev -> let* v = betree_upsert_update (Some prev) s in - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in let* v = betree_upsert_update None s in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert _ -> let* (msgs2, lookup_first_message_after_key_back) = betree_Node_lookup_first_message_after_key key msgs1 in - let* l = + let* msgs3 = betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Upsert s) in - let* msgs3 = lookup_first_message_after_key_back l in - lookup_first_message_for_key_back msgs3 + let* msgs4 = lookup_first_message_after_key_back msgs3 in + lookup_first_message_for_key_back msgs4 end end else - let* l = + let* msgs2 = betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in - lookup_first_message_for_key_back l + lookup_first_message_for_key_back msgs2 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) @@ -429,8 +432,8 @@ let rec betree_Node_apply_messages_to_internal begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal l new_msgs_tl + let* msgs1 = betree_Node_apply_to_internal msgs i m in + betree_Node_apply_messages_to_internal msgs1 new_msgs_tl | Betree_List_Nil -> Return msgs end @@ -470,28 +473,28 @@ let betree_Node_apply_to_leaf let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in if b then - let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in + let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in begin match new_msg with | Betree_Message_Insert v -> - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 - | Betree_Message_Delete -> lookup_mut_in_bindings_back l + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2 | Betree_Message_Upsert s -> let (_, i) = hd in let* v = betree_upsert_update (Some i) s in - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 end else begin match new_msg with | Betree_Message_Insert v -> - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1 | Betree_Message_Upsert s -> let* v = betree_upsert_update None s in - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 end (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: @@ -505,8 +508,8 @@ let rec betree_Node_apply_messages_to_leaf begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf l new_msgs_tl + let* bindings1 = betree_Node_apply_to_leaf bindings i m in + betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl | Betree_List_Nil -> Return bindings end @@ -560,31 +563,31 @@ and betree_Node_apply_messages begin match self with | Betree_Node_Internal node -> let* (st1, content) = betree_load_internal_node node.id st in - let* l = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) l in + let* content1 = betree_Node_apply_messages_to_internal content msgs in + let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in if num_msgs >= params.min_flush_size then - let* (st2, (content1, p)) = - betree_Internal_flush node params node_id_cnt l st1 in + let* (st2, (content2, p)) = + betree_Internal_flush node params node_id_cnt content1 st1 in let (node1, node_id_cnt1) = p in - let* (st3, _) = betree_store_internal_node node1.id content1 st2 in + let* (st3, _) = betree_store_internal_node node1.id content2 st2 in Return (st3, (Betree_Node_Internal node1, node_id_cnt1)) else - let* (st2, _) = betree_store_internal_node node.id l st1 in + let* (st2, _) = betree_store_internal_node node.id content1 st1 in Return (st2, (Betree_Node_Internal node, node_id_cnt)) | Betree_Node_Leaf node -> let* (st1, content) = betree_load_leaf_node node.id st in - let* l = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) l in + let* content1 = betree_Node_apply_messages_to_leaf content msgs in + let* len = betree_List_len (u64 & u64) content1 in let* i = u64_mul 2 params.split_size in if len >= i then - let* (st2, (new_node, nic)) = - betree_Leaf_split node l params node_id_cnt st1 in + let* (st2, (new_node, node_id_cnt1)) = + betree_Leaf_split node content1 params node_id_cnt st1 in let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in - Return (st3, (Betree_Node_Internal new_node, nic)) + Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)) else - let* (st2, _) = betree_store_leaf_node node.id l st1 in + let* (st2, _) = betree_store_leaf_node node.id content1 st1 in Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) end @@ -609,12 +612,12 @@ let betree_BeTree_new result (state & betree_BeTree_t) = let* node_id_cnt = betree_NodeIdCounter_new in - let* (id, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in Return (st1, { params = { min_flush_size = min_flush_size; split_size = split_size }; - node_id_cnt = nic; + node_id_cnt = node_id_cnt1; root = (Betree_Node_Leaf { id = id; size = 0 }) }) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index ec042fb3..2469f98c 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -22,8 +22,7 @@ let betree_store_internal_node (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_internal_node id content st in - Return (st1, ()) + betree_utils_store_internal_node id content st (** [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) @@ -37,8 +36,7 @@ let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_leaf_node id content st in - Return (st1, ()) + betree_utils_store_leaf_node id content st (** [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) @@ -172,13 +170,14 @@ let betree_Leaf_split let (content0, content1) = p in let* p1 = betree_List_hd (u64 & u64) content1 in let (pivot, _) = p1 in - let* (id0, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (id1, nic1) = betree_NodeIdCounter_fresh_id nic in + let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in let* (st1, _) = betree_store_leaf_node id0 content0 st in let* (st2, _) = betree_store_leaf_node id1 content1 st1 in let n = Betree_Node_Leaf { id = id0; size = params.split_size } in let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in - Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, nic1)) + Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, + node_id_cnt2)) (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 *) @@ -231,21 +230,21 @@ let rec betree_Node_apply_upserts let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b then - let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in + let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in let (_, m) = msg in begin match m with | Betree_Message_Insert _ -> Fail Failure | Betree_Message_Delete -> Fail Failure | Betree_Message_Upsert s -> let* v = betree_upsert_update prev s in - betree_Node_apply_upserts l (Some v) key st + betree_Node_apply_upserts msgs1 (Some v) key st end else let* (st1, v) = core_option_Option_unwrap u64 prev st in - let* l = + let* msgs1 = betree_List_push_front (u64 & betree_Message_t) msgs (key, Betree_Message_Insert v) in - Return (st1, (v, l)) + Return (st1, (v, msgs1)) (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) @@ -279,10 +278,11 @@ and betree_Node_lookup let (k, msg) = p in if k <> key then - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = + betree_Internal_lookup_in_children node key st1 in let* _ = lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) else begin match msg with | Betree_Message_Insert v -> @@ -296,19 +296,20 @@ and betree_Node_lookup Betree_Message_Delete) l) in Return (st1, (None, Betree_Node_Internal node)) | Betree_Message_Upsert ufs -> - let* (st2, (v, i)) = betree_Internal_lookup_in_children node key st1 - in - let* (st3, (v1, l1)) = + let* (st2, (v, node1)) = + betree_Internal_lookup_in_children node key st1 in + let* (st3, (v1, pending1)) = betree_Node_apply_upserts (Betree_List_Cons (k, Betree_Message_Upsert ufs) l) v key st2 in - let* msgs1 = lookup_first_message_for_key_back l1 in - let* (st4, _) = betree_store_internal_node i.id msgs1 st3 in - Return (st4, (Some v1, Betree_Node_Internal i)) + let* msgs1 = lookup_first_message_for_key_back pending1 in + let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in + Return (st4, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil -> - let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in + let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 + in let* _ = lookup_first_message_for_key_back Betree_List_Nil in - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) end | Betree_Node_Leaf node -> let* (st1, bindings) = betree_load_leaf_node node.id st in @@ -328,10 +329,10 @@ let rec betree_Node_filter_messages_for_key let (k, m) = p in if k = key then - let* (_, l1) = + let* (_, msgs1) = betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m) l) in - betree_Node_filter_messages_for_key key l1 + betree_Node_filter_messages_for_key key msgs1 else Return (Betree_List_Cons (k, m) l) | Betree_List_Nil -> Return Betree_List_Nil end @@ -374,49 +375,51 @@ let betree_Node_apply_to_internal then begin match new_msg with | Betree_Message_Insert i -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert i) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* l = betree_Node_filter_messages_for_key key msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Delete) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert s -> let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in let (_, m) = p in begin match m with | Betree_Message_Insert prev -> let* v = betree_upsert_update (Some prev) s in - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete -> - let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in let* v = betree_upsert_update None s in - let* l1 = - betree_List_push_front (u64 & betree_Message_t) l (key, + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Insert v) in - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert _ -> let* (msgs2, lookup_first_message_after_key_back) = betree_Node_lookup_first_message_after_key key msgs1 in - let* l = + let* msgs3 = betree_List_push_front (u64 & betree_Message_t) msgs2 (key, Betree_Message_Upsert s) in - let* msgs3 = lookup_first_message_after_key_back l in - lookup_first_message_for_key_back msgs3 + let* msgs4 = lookup_first_message_after_key_back msgs3 in + lookup_first_message_for_key_back msgs4 end end else - let* l = + let* msgs2 = betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in - lookup_first_message_for_key_back l + lookup_first_message_for_key_back msgs2 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) @@ -429,8 +432,8 @@ let rec betree_Node_apply_messages_to_internal begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal l new_msgs_tl + let* msgs1 = betree_Node_apply_to_internal msgs i m in + betree_Node_apply_messages_to_internal msgs1 new_msgs_tl | Betree_List_Nil -> Return msgs end @@ -470,28 +473,28 @@ let betree_Node_apply_to_leaf let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in if b then - let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in + let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in begin match new_msg with | Betree_Message_Insert v -> - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 - | Betree_Message_Delete -> lookup_mut_in_bindings_back l + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2 | Betree_Message_Upsert s -> let (_, i) = hd in let* v = betree_upsert_update (Some i) s in - let* l1 = betree_List_push_front (u64 & u64) l (key, v) in - lookup_mut_in_bindings_back l1 + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 end else begin match new_msg with | Betree_Message_Insert v -> - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1 | Betree_Message_Upsert s -> let* v = betree_upsert_update None s in - let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back l + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 end (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: @@ -505,8 +508,8 @@ let rec betree_Node_apply_messages_to_leaf begin match new_msgs with | Betree_List_Cons new_msg new_msgs_tl -> let (i, m) = new_msg in - let* l = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf l new_msgs_tl + let* bindings1 = betree_Node_apply_to_leaf bindings i m in + betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl | Betree_List_Nil -> Return bindings end @@ -560,31 +563,31 @@ and betree_Node_apply_messages begin match self with | Betree_Node_Internal node -> let* (st1, content) = betree_load_internal_node node.id st in - let* l = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) l in + let* content1 = betree_Node_apply_messages_to_internal content msgs in + let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in if num_msgs >= params.min_flush_size then - let* (st2, (content1, p)) = - betree_Internal_flush node params node_id_cnt l st1 in + let* (st2, (content2, p)) = + betree_Internal_flush node params node_id_cnt content1 st1 in let (node1, node_id_cnt1) = p in - let* (st3, _) = betree_store_internal_node node1.id content1 st2 in + let* (st3, _) = betree_store_internal_node node1.id content2 st2 in Return (st3, (Betree_Node_Internal node1, node_id_cnt1)) else - let* (st2, _) = betree_store_internal_node node.id l st1 in + let* (st2, _) = betree_store_internal_node node.id content1 st1 in Return (st2, (Betree_Node_Internal node, node_id_cnt)) | Betree_Node_Leaf node -> let* (st1, content) = betree_load_leaf_node node.id st in - let* l = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) l in + let* content1 = betree_Node_apply_messages_to_leaf content msgs in + let* len = betree_List_len (u64 & u64) content1 in let* i = u64_mul 2 params.split_size in if len >= i then - let* (st2, (new_node, nic)) = - betree_Leaf_split node l params node_id_cnt st1 in + let* (st2, (new_node, node_id_cnt1)) = + betree_Leaf_split node content1 params node_id_cnt st1 in let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in - Return (st3, (Betree_Node_Internal new_node, nic)) + Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)) else - let* (st2, _) = betree_store_leaf_node node.id l st1 in + let* (st2, _) = betree_store_leaf_node node.id content1 st1 in Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) end @@ -609,12 +612,12 @@ let betree_BeTree_new result (state & betree_BeTree_t) = let* node_id_cnt = betree_NodeIdCounter_new in - let* (id, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in Return (st1, { params = { min_flush_size = min_flush_size; split_size = split_size }; - node_id_cnt = nic; + node_id_cnt = node_id_cnt1; root = (Betree_Node_Leaf { id = id; size = 0 }) }) diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index d13d2ba3..d93bc847 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -28,14 +28,19 @@ let use_mul2_add1 (x : u32) (y : u32) : result u32 = let incr (x : u32) : result u32 = u32_add x 1 +(** [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 *) +let use_incr : result unit = + let* x = incr 0 in let* x1 = incr x in let* _ = incr x1 in Return () + (** [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 *) + Source: 'src/demo.rs', lines 34:0-34:17 *) type cList_t (t : Type0) = | CList_CCons : t -> cList_t t -> cList_t t | CList_CNil : cList_t t (** [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 *) + Source: 'src/demo.rs', lines 39:0-39:56 *) let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t = if is_zero n then Fail OutOfFuel @@ -48,7 +53,7 @@ let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t = end (** [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 *) + Source: 'src/demo.rs', lines 54:0-54:68 *) let rec list_nth_mut (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -74,7 +79,7 @@ let rec list_nth_mut end (** [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 *) + Source: 'src/demo.rs', lines 69:0-78:1 *) let rec list_nth_mut1_loop (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -99,15 +104,15 @@ let rec list_nth_mut1_loop end (** [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 *) + Source: 'src/demo.rs', lines 69:0-69:77 *) let list_nth_mut1 (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) = - let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a) + list_nth_mut1_loop t n l i (** [demo::i32_id]: - Source: 'src/demo.rs', lines 73:0-73:28 *) + Source: 'src/demo.rs', lines 80:0-80:28 *) let rec i32_id (n : nat) (i : i32) : result i32 = if is_zero n then Fail OutOfFuel @@ -117,21 +122,41 @@ let rec i32_id (n : nat) (i : i32) : result i32 = then Return 0 else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1 +(** [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 *) +let rec list_tail + (t : Type0) (n : nat) (l : cList_t t) : + result ((cList_t t) & (cList_t t -> result (cList_t t))) + = + if is_zero n + then Fail OutOfFuel + else + let n1 = decrease n in + begin match l with + | CList_CCons x tl -> + let* (c, list_tail_back) = list_tail t n1 tl in + let back_'a = + fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1) + in + Return (c, back_'a) + | CList_CNil -> Return (CList_CNil, Return) + end + (** Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 *) + Source: 'src/demo.rs', lines 97:0-97:17 *) noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); } (** [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 *) + Source: 'src/demo.rs', lines 102:4-102:31 *) let counterUsize_incr (self : usize) : result (usize & usize) = let* self1 = usize_add self 1 in Return (self, self1) (** Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 *) + Source: 'src/demo.rs', lines 101:0-101:22 *) let counterUsize : counter_t usize = { incr = counterUsize_incr; } (** [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 *) + Source: 'src/demo.rs', lines 109:0-109:59 *) let use_counter (t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) = counterInst.incr cnt diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 447f9b49..fba711f1 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -21,9 +21,9 @@ let rec hashMap_allocate_slots_loop = if n > 0 then - let* v = alloc_vec_Vec_push (list_t t) slots List_Nil in + let* slots1 = alloc_vec_Vec_push (list_t t) slots List_Nil in let* n1 = usize_sub n 1 in - hashMap_allocate_slots_loop t v n1 + hashMap_allocate_slots_loop t slots1 n1 else Return slots (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: @@ -142,8 +142,8 @@ let rec hashMap_move_elements_from_list_loop = begin match ls with | List_Cons k v tl -> - let* hm = hashMap_insert_no_resize t ntable k v in - hashMap_move_elements_from_list_loop t hm tl + let* ntable1 = hashMap_insert_no_resize t ntable k v in + hashMap_move_elements_from_list_loop t ntable1 tl | List_Nil -> Return ntable end @@ -168,12 +168,10 @@ let rec hashMap_move_elements_loop alloc_vec_Vec_index_mut (list_t t) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) slots i in let (ls, l1) = core_mem_replace (list_t t) l List_Nil in - let* hm = hashMap_move_elements_from_list t ntable ls in + let* ntable1 = hashMap_move_elements_from_list t ntable ls in let* i2 = usize_add i 1 in let* slots1 = index_mut_back l1 in - let* back_'a = hashMap_move_elements_loop t hm slots1 i2 in - let (hm1, v) = back_'a in - Return (hm1, v) + hashMap_move_elements_loop t ntable1 slots1 i2 else Return (ntable, slots) (** [hashmap::{hashmap::HashMap<T>}::move_elements]: @@ -183,9 +181,7 @@ let hashMap_move_elements (i : usize) : result ((hashMap_t t) & (alloc_vec_Vec (list_t t))) = - let* back_'a = hashMap_move_elements_loop t ntable slots i in - let (hm, v) = back_'a in - Return (hm, v) + hashMap_move_elements_loop t ntable slots i (** [hashmap::{hashmap::HashMap<T>}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 *) @@ -213,9 +209,9 @@ let hashMap_insert (t : Type0) (self : hashMap_t t) (key : usize) (value : t) : result (hashMap_t t) = - let* hm = hashMap_insert_no_resize t self key value in - let* i = hashMap_len t hm in - if i > hm.max_load then hashMap_try_resize t hm else Return hm + let* self1 = hashMap_insert_no_resize t self key value in + let* i = hashMap_len t self1 in + if i > self1.max_load then hashMap_try_resize t self1 else Return self1 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 *) @@ -308,8 +304,7 @@ let hashMap_get_mut_in_list (t : Type0) (ls : list_t t) (key : usize) : result (t & (t -> result (list_t t))) = - let* (x, back_'a) = hashMap_get_mut_in_list_loop t ls key in - Return (x, back_'a) + hashMap_get_mut_in_list_loop t ls key (** [hashmap::{hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 *) diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index b16dcada..97f4151f 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -22,9 +22,10 @@ let rec hashmap_HashMap_allocate_slots_loop = if n > 0 then - let* v = alloc_vec_Vec_push (hashmap_List_t t) slots Hashmap_List_Nil in + let* slots1 = alloc_vec_Vec_push (hashmap_List_t t) slots Hashmap_List_Nil + in let* n1 = usize_sub n 1 in - hashmap_HashMap_allocate_slots_loop t v n1 + hashmap_HashMap_allocate_slots_loop t slots1 n1 else Return slots (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: @@ -149,8 +150,8 @@ let rec hashmap_HashMap_move_elements_from_list_loop = begin match ls with | Hashmap_List_Cons k v tl -> - let* hm = hashmap_HashMap_insert_no_resize t ntable k v in - hashmap_HashMap_move_elements_from_list_loop t hm tl + let* ntable1 = hashmap_HashMap_insert_no_resize t ntable k v in + hashmap_HashMap_move_elements_from_list_loop t ntable1 tl | Hashmap_List_Nil -> Return ntable end @@ -178,12 +179,10 @@ let rec hashmap_HashMap_move_elements_loop (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) slots i in let (ls, l1) = core_mem_replace (hashmap_List_t t) l Hashmap_List_Nil in - let* hm = hashmap_HashMap_move_elements_from_list t ntable ls in + let* ntable1 = hashmap_HashMap_move_elements_from_list t ntable ls in let* i2 = usize_add i 1 in let* slots1 = index_mut_back l1 in - let* back_'a = hashmap_HashMap_move_elements_loop t hm slots1 i2 in - let (hm1, v) = back_'a in - Return (hm1, v) + hashmap_HashMap_move_elements_loop t ntable1 slots1 i2 else Return (ntable, slots) (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: @@ -193,9 +192,7 @@ let hashmap_HashMap_move_elements (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : result ((hashmap_HashMap_t t) & (alloc_vec_Vec (hashmap_List_t t))) = - let* back_'a = hashmap_HashMap_move_elements_loop t ntable slots i in - let (hm, v) = back_'a in - Return (hm, v) + hashmap_HashMap_move_elements_loop t ntable slots i (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 *) @@ -223,9 +220,11 @@ let hashmap_HashMap_insert (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) : result (hashmap_HashMap_t t) = - let* hm = hashmap_HashMap_insert_no_resize t self key value in - let* i = hashmap_HashMap_len t hm in - if i > hm.max_load then hashmap_HashMap_try_resize t hm else Return hm + let* self1 = hashmap_HashMap_insert_no_resize t self key value in + let* i = hashmap_HashMap_len t self1 in + if i > self1.max_load + then hashmap_HashMap_try_resize t self1 + else Return self1 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 *) @@ -324,8 +323,7 @@ let hashmap_HashMap_get_mut_in_list (t : Type0) (ls : hashmap_List_t t) (key : usize) : result (t & (t -> result (hashmap_List_t t))) = - let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t ls key in - Return (x, back_'a) + hashmap_HashMap_get_mut_in_list_loop t ls key (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 *) @@ -446,8 +444,7 @@ let insert_on_disk (key : usize) (value : u64) (st : state) : result (state & unit) = let* (st1, hm) = hashmap_utils_deserialize st in let* hm1 = hashmap_HashMap_insert u64 hm key value in - let* (st2, _) = hashmap_utils_serialize hm1 st1 in - Return (st2, ()) + hashmap_utils_serialize hm1 st1 (** [hashmap_main::main]: Source: 'src/hashmap_main.rs', lines 16:0-16:13 *) diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 6672b523..3ba20022 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -33,8 +33,8 @@ let custom_swap (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & (t -> state -> result (state & (t & t))))) = - let* (st1, (x1, x2)) = core_mem_swap t x y st in - let back_'a = fun ret st2 -> Return (st2, (ret, x2)) in + let* (st1, (x1, y1)) = core_mem_swap t x y st in + let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in Return (st1, (x1, back_'a)) (** [external::test_custom_swap]: diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index c8ed16f4..e43f8170 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -13,8 +13,7 @@ unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_mut_borrows]: decreases clause Source: 'src/loops.rs', lines 19:0-31:1 *) unfold -let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat - = +let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_shared_borrows]: decreases clause diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 5f24fe7a..7c099da2 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -25,15 +25,15 @@ let sum (max : u32) : result u32 = (** [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 *) let rec sum_with_mut_borrows_loop - (max : u32) (mi : u32) (ms : u32) : - Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s)) = - if mi < max + if i < max then - let* ms1 = u32_add ms mi in - let* mi1 = u32_add mi 1 in - sum_with_mut_borrows_loop max mi1 ms1 - else u32_mul ms 2 + let* ms = u32_add s i in + let* mi = u32_add i 1 in + sum_with_mut_borrows_loop max mi ms + else u32_mul s 2 (** [loops::sum_with_mut_borrows]: Source: 'src/loops.rs', lines 19:0-19:44 *) @@ -140,7 +140,7 @@ let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result (t & (t -> result (list_t t))) = - let* (x, back) = list_nth_mut_loop_loop t ls i in Return (x, back) + list_nth_mut_loop_loop t ls i (** [loops::list_nth_shared_loop]: loop 0: Source: 'src/loops.rs', lines 101:0-111:1 *) @@ -185,11 +185,11 @@ let get_elem_mut (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result (usize & (usize -> result (alloc_vec_Vec (list_t usize)))) = - let* (l, index_mut_back) = + let* (ls, index_mut_back) = alloc_vec_Vec_index_mut (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - let* (i, back) = get_elem_mut_loop x l in - let back1 = fun ret -> let* l1 = back ret in index_mut_back l1 in + let* (i, back) = get_elem_mut_loop x ls in + let back1 = fun ret -> let* l = back ret in index_mut_back l in Return (i, back1) (** [loops::get_elem_shared]: loop 0: @@ -207,10 +207,10 @@ let rec get_elem_shared_loop Source: 'src/loops.rs', lines 129:0-129:68 *) let get_elem_shared (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = - let* l = + let* ls = alloc_vec_Vec_index (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - get_elem_shared_loop x l + get_elem_shared_loop x ls (** [loops::id_mut]: Source: 'src/loops.rs', lines 145:0-145:50 *) @@ -312,8 +312,7 @@ let list_nth_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t))) = - let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t ls0 ls1 i in - Return (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_shared_loop_pair]: loop 0: Source: 'src/loops.rs', lines 208:0-229:1 *) @@ -376,8 +375,7 @@ let list_nth_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t)))) = - let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 251:0-266:1 *) @@ -438,8 +436,7 @@ let list_nth_mut_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_shared_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 288:0-303:1 *) @@ -474,8 +471,7 @@ let list_nth_mut_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair]: loop 0: Source: 'src/loops.rs', lines 307:0-322:1 *) @@ -509,8 +505,7 @@ let list_nth_shared_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t ls0 ls1 i in - Return (p, back_'b) + list_nth_shared_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 326:0-341:1 *) @@ -545,8 +540,7 @@ let list_nth_shared_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::ignore_input_mut_borrow]: loop 0: Source: 'src/loops.rs', lines 345:0-349:1 *) @@ -555,10 +549,7 @@ let rec ignore_input_mut_borrow_loop Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = ignore_input_mut_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in ignore_input_mut_borrow_loop i1 else Return () (** [loops::ignore_input_mut_borrow]: @@ -573,10 +564,7 @@ let rec incr_ignore_input_mut_borrow_loop Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = incr_ignore_input_mut_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in incr_ignore_input_mut_borrow_loop i1 else Return () (** [loops::incr_ignore_input_mut_borrow]: @@ -593,10 +581,7 @@ let rec ignore_input_shared_borrow_loop Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = ignore_input_shared_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in ignore_input_shared_borrow_loop i1 else Return () (** [loops::ignore_input_shared_borrow]: diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index c71f8dbb..db63eb0d 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -425,8 +425,7 @@ let id_mut_pair1 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) = - let back_'a = fun ret -> let (x1, x2) = ret in Return (x1, x2) in - Return ((x, y), back_'a) + Return ((x, y), Return) (** [no_nested_borrows::id_mut_pair2]: Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 *) @@ -434,9 +433,7 @@ let id_mut_pair2 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) = - let (x, x1) = p in - let back_'a = fun ret -> let (x2, x3) = ret in Return (x2, x3) in - Return ((x, x1), back_'a) + let (x, x1) = p in Return ((x, x1), Return) (** [no_nested_borrows::id_mut_pair3]: Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 *) diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index cf4dc454..ddc5e7a8 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -13,7 +13,7 @@ let ref_incr (x : i32) : result i32 = (** [paper::test_incr]: Source: 'src/paper.rs', lines 8:0-8:18 *) let test_incr : result unit = - let* i = ref_incr 0 in if not (i = 1) then Fail Failure else Return () + let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Return () (** Unit test for [paper::test_incr] *) let _ = assert_norm (test_incr = Return ()) diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index d637ee13..207f31b9 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -28,31 +28,26 @@ def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result ((Slice T) × (Slice T → Result (Array T 32#usize))) := - do - let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s - Result.ret (s1, to_slice_mut_back) + Array.to_slice_mut T 32#usize s /- [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 -/ def array_len (T : Type) (s : Array T 32#usize) : Result Usize := do let s1 ← Array.to_slice T 32#usize s - let i := Slice.len T s1 - Result.ret i + Result.ret (Slice.len T s1) /- [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 -/ def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := do let s1 ← Array.to_slice T 32#usize s - let i := Slice.len T s1 - Result.ret i + Result.ret (Slice.len T s1) /- [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 -/ def shared_slice_len (T : Type) (s : Slice T) : Result Usize := - let i := Slice.len T s - Result.ret i + Result.ret (Slice.len T s) /- [arrays::index_array_shared]: Source: 'src/arrays.rs', lines 37:0-37:57 -/ @@ -76,9 +71,7 @@ def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result (T × (T → Result (Array T 32#usize))) := - do - let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i - Result.ret (t, index_mut_back) + Array.index_mut_usize T 32#usize s i /- [arrays::index_slice]: Source: 'src/arrays.rs', lines 56:0-56:46 -/ @@ -91,9 +84,7 @@ def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result (T × (T → Result (Slice T))) := - do - let (t, index_mut_back) ← Slice.index_mut_usize T s i - Result.ret (t, index_mut_back) + Slice.index_mut_usize T s i /- [arrays::slice_subslice_shared_]: Source: 'src/arrays.rs', lines 64:0-64:70 -/ @@ -127,9 +118,7 @@ def array_to_slice_mut_ (x : Array U32 32#usize) : Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) := - do - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x - Result.ret (s, to_slice_mut_back) + Array.to_slice_mut U32 32#usize x /- [arrays::array_subslice_shared_]: Source: 'src/arrays.rs', lines 80:0-80:74 -/ @@ -313,8 +302,8 @@ def update_all : Result Unit := do let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let a ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize a + let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x let s1 ← update_mut_slice s let _ ← to_slice_mut_back s1 Result.ret () @@ -354,9 +343,7 @@ def take_array_t (a : Array AB 2#usize) : Result Unit := /- [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 -/ def non_copyable_array : Result Unit := - do - let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) - Result.ret () + take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) /- [arrays::sum]: loop 0: Source: 'src/arrays.rs', lines 242:0-250:1 -/ @@ -496,11 +483,9 @@ def zero_slice (a : Slice U8) : Result (Slice U8) := Source: 'src/arrays.rs', lines 312:0-318:1 -/ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := if i < len - then - do - let i1 ← i + 1#usize - let _ ← iter_mut_slice_loop len i1 - Result.ret () + then do + let i1 ← i + 1#usize + iter_mut_slice_loop len i1 else Result.ret () /- [arrays::iter_mut_slice]: diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index d6449b37..ca9b48da 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -21,9 +21,7 @@ def betree.store_internal_node (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) : Result (State × Unit) := - do - let (st1, _) ← betree_utils.store_internal_node id content st - Result.ret (st1, ()) + betree_utils.store_internal_node id content st /- [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 -/ @@ -37,9 +35,7 @@ def betree.store_leaf_node (id : U64) (content : betree.List (U64 × U64)) (st : State) : Result (State × Unit) := - do - let (st1, _) ← betree_utils.store_leaf_node id content st - Result.ret (st1, ()) + betree_utils.store_leaf_node id content st /- [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 -/ @@ -172,13 +168,13 @@ def betree.Leaf.split let (content0, content1) := p let p1 ← betree.List.hd (U64 × U64) content1 let (pivot, _) := p1 - let (id0, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt - let (id1, nic1) ← betree.NodeIdCounter.fresh_id nic + let (id0, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1 let (st1, _) ← betree.store_leaf_node id0 content0 st let (st2, _) ← betree.store_leaf_node id1 content1 st1 let n := betree.Node.Leaf { id := id0, size := params.split_size } let n1 := betree.Node.Leaf { id := id1, size := params.split_size } - Result.ret (st2, (betree.Internal.mk self.id pivot n n1, nic1)) + Result.ret (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 -/ @@ -231,7 +227,7 @@ divergent def betree.Node.apply_upserts if b then do - let (msg, l) ← betree.List.pop_front (U64 × betree.Message) msgs + let (msg, msgs1) ← betree.List.pop_front (U64 × betree.Message) msgs let (_, m) := msg match m with | betree.Message.Insert _ => Result.fail .panic @@ -239,14 +235,14 @@ divergent def betree.Node.apply_upserts | betree.Message.Upsert s => do let v ← betree.upsert_update prev s - betree.Node.apply_upserts l (some v) key st + betree.Node.apply_upserts msgs1 (some v) key st else do let (st1, v) ← core.option.Option.unwrap U64 prev st - let l ← + let msgs1 ← betree.List.push_front (U64 × betree.Message) msgs (key, betree.Message.Insert v) - Result.ret (st1, (v, l)) + Result.ret (st1, (v, msgs1)) /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ @@ -284,12 +280,12 @@ divergent def betree.Node.lookup if k != key then do - let (st2, (o, i2)) ← + let (st2, (o, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 let _ ← lookup_first_message_for_key_back (betree.List.Cons (k, msg) l) - Result.ret (st2, (o, betree.Node.Internal i2)) + Result.ret (st2, (o, betree.Node.Internal node1)) else match msg with | betree.Message.Insert v => @@ -308,24 +304,24 @@ divergent def betree.Node.lookup n n1))) | betree.Message.Upsert ufs => do - let (st2, (v, i2)) ← + let (st2, (v, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 - let (st3, (v1, l1)) ← + let (st3, (v1, pending1)) ← betree.Node.apply_upserts (betree.List.Cons (k, betree.Message.Upsert ufs) l) v key st2 - let ⟨ i3, i4, n2, n3 ⟩ := i2 - let msgs1 ← lookup_first_message_for_key_back l1 - let (st4, _) ← betree.store_internal_node i3 msgs1 st3 + let ⟨ i2, i3, n2, n3 ⟩ := node1 + let msgs1 ← lookup_first_message_for_key_back pending1 + let (st4, _) ← betree.store_internal_node i2 msgs1 st3 Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk - i3 i4 n2 n3))) + i2 i3 n2 n3))) | betree.List.Nil => do - let (st2, (o, i2)) ← + let (st2, (o, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 let _ ← lookup_first_message_for_key_back betree.List.Nil - Result.ret (st2, (o, betree.Node.Internal i2)) + Result.ret (st2, (o, betree.Node.Internal node1)) | betree.Node.Leaf node => do let (st1, bindings) ← betree.load_leaf_node node.id st @@ -346,10 +342,10 @@ divergent def betree.Node.filter_messages_for_key if k = key then do - let (_, l1) ← + let (_, msgs1) ← betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) l) - betree.Node.filter_messages_for_key key l1 + betree.Node.filter_messages_for_key key msgs1 else Result.ret (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ret betree.List.Nil @@ -393,18 +389,18 @@ def betree.Node.apply_to_internal match new_msg with | betree.Message.Insert i => do - let l ← betree.Node.filter_messages_for_key key msgs1 - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Insert i) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Delete => do - let l ← betree.Node.filter_messages_for_key key msgs1 - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Delete) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Upsert s => do let p ← betree.List.hd (U64 × betree.Message) msgs1 @@ -413,33 +409,33 @@ def betree.Node.apply_to_internal | betree.Message.Insert prev => do let v ← betree.upsert_update (some prev) s - let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Insert v) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Delete => do - let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 let v ← betree.upsert_update none s - let l1 ← - betree.List.push_front (U64 × betree.Message) l (key, + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Insert v) - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | betree.Message.Upsert _ => do let (msgs2, lookup_first_message_after_key_back) ← betree.Node.lookup_first_message_after_key key msgs1 - let l ← + let msgs3 ← betree.List.push_front (U64 × betree.Message) msgs2 (key, betree.Message.Upsert s) - let msgs3 ← lookup_first_message_after_key_back l - lookup_first_message_for_key_back msgs3 + let msgs4 ← lookup_first_message_after_key_back msgs3 + lookup_first_message_for_key_back msgs4 else do - let l ← + let msgs2 ← betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) - lookup_first_message_for_key_back l + lookup_first_message_for_key_back msgs2 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 -/ @@ -452,8 +448,8 @@ divergent def betree.Node.apply_messages_to_internal | betree.List.Cons new_msg new_msgs_tl => do let (i, m) := new_msg - let l ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal l new_msgs_tl + let msgs1 ← betree.Node.apply_to_internal msgs i m + betree.Node.apply_messages_to_internal msgs1 new_msgs_tl | betree.List.Nil => Result.ret msgs /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: @@ -494,31 +490,31 @@ def betree.Node.apply_to_leaf if b then do - let (hd, l) ← betree.List.pop_front (U64 × U64) bindings1 + let (hd, bindings2) ← betree.List.pop_front (U64 × U64) bindings1 match new_msg with | betree.Message.Insert v => do - let l1 ← betree.List.push_front (U64 × U64) l (key, v) - lookup_mut_in_bindings_back l1 - | betree.Message.Delete => lookup_mut_in_bindings_back l + let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v) + lookup_mut_in_bindings_back bindings3 + | betree.Message.Delete => lookup_mut_in_bindings_back bindings2 | betree.Message.Upsert s => do let (_, i) := hd let v ← betree.upsert_update (some i) s - let l1 ← betree.List.push_front (U64 × U64) l (key, v) - lookup_mut_in_bindings_back l1 + let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v) + lookup_mut_in_bindings_back bindings3 else match new_msg with | betree.Message.Insert v => do - let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) - lookup_mut_in_bindings_back l + let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back bindings2 | betree.Message.Delete => lookup_mut_in_bindings_back bindings1 | betree.Message.Upsert s => do let v ← betree.upsert_update none s - let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) - lookup_mut_in_bindings_back l + let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back bindings2 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 -/ @@ -531,8 +527,8 @@ divergent def betree.Node.apply_messages_to_leaf | betree.List.Cons new_msg new_msgs_tl => do let (i, m) := new_msg - let l ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf l new_msgs_tl + let bindings1 ← betree.Node.apply_to_leaf bindings i m + betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl | betree.List.Nil => Result.ret bindings /- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: @@ -587,40 +583,40 @@ divergent def betree.Node.apply_messages do let ⟨ i, i1, n, n1 ⟩ := node let (st1, content) ← betree.load_internal_node i st - let l ← betree.Node.apply_messages_to_internal content msgs - let num_msgs ← betree.List.len (U64 × betree.Message) l + let content1 ← betree.Node.apply_messages_to_internal content msgs + let num_msgs ← betree.List.len (U64 × betree.Message) content1 if num_msgs >= params.min_flush_size then do - let (st2, (content1, p)) ← + let (st2, (content2, p)) ← betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt - l st1 + content1 st1 let (node1, node_id_cnt1) := p let ⟨ i2, i3, n2, n3 ⟩ := node1 - let (st3, _) ← betree.store_internal_node i2 content1 st2 + let (st3, _) ← betree.store_internal_node i2 content2 st2 Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3), node_id_cnt1)) else do - let (st2, _) ← betree.store_internal_node i l st1 + let (st2, _) ← betree.store_internal_node i content1 st1 Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1), node_id_cnt)) | betree.Node.Leaf node => do let (st1, content) ← betree.load_leaf_node node.id st - let l ← betree.Node.apply_messages_to_leaf content msgs - let len ← betree.List.len (U64 × U64) l + let content1 ← betree.Node.apply_messages_to_leaf content msgs + let len ← betree.List.len (U64 × U64) content1 let i ← 2#u64 * params.split_size if len >= i then do - let (st2, (new_node, nic)) ← - betree.Leaf.split node l params node_id_cnt st1 + let (st2, (new_node, node_id_cnt1)) ← + betree.Leaf.split node content1 params node_id_cnt st1 let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2 - Result.ret (st3, (betree.Node.Internal new_node, nic)) + Result.ret (st3, (betree.Node.Internal new_node, node_id_cnt1)) else do - let (st2, _) ← betree.store_leaf_node node.id l st1 + let (st2, _) ← betree.store_leaf_node node.id content1 st1 Result.ret (st2, (betree.Node.Leaf { node with size := len }, node_id_cnt)) @@ -649,12 +645,12 @@ def betree.BeTree.new := do let node_id_cnt ← betree.NodeIdCounter.new - let (id, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt let (st1, _) ← betree.store_leaf_node id betree.List.Nil st Result.ret (st1, { params := { min_flush_size := min_flush_size, split_size := split_size }, - node_id_cnt := nic, + node_id_cnt := node_id_cnt1, root := (betree.Node.Leaf { id := id, size := 0#u64 }) }) diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 854b4853..4acc69c8 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -36,14 +36,23 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := def incr (x : U32) : Result U32 := x + 1#u32 +/- [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 -/ +def use_incr : Result Unit := + do + let x ← incr 0#u32 + let x1 ← incr x + let _ ← incr x1 + Result.ret () + /- [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 -/ + Source: 'src/demo.rs', lines 34:0-34:17 -/ inductive CList (T : Type) := | CCons : T → CList T → CList T | CNil : CList T /- [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 -/ + Source: 'src/demo.rs', lines 39:0-39:56 -/ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CList.CCons x tl => @@ -55,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := | CList.CNil => Result.fail .panic /- [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 -/ + Source: 'src/demo.rs', lines 54:0-54:68 -/ divergent def list_nth_mut (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) @@ -79,7 +88,7 @@ divergent def list_nth_mut | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 -/ + Source: 'src/demo.rs', lines 69:0-78:1 -/ divergent def list_nth_mut1_loop (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) @@ -102,17 +111,15 @@ divergent def list_nth_mut1_loop | CList.CNil => Result.fail .panic /- [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 -/ + Source: 'src/demo.rs', lines 69:0-69:77 -/ def list_nth_mut1 (T : Type) (l : CList T) (i : U32) : Result (T × (T → Result (CList T))) := - do - let (t, back_'a) ← list_nth_mut1_loop T l i - Result.ret (t, back_'a) + list_nth_mut1_loop T l i /- [demo::i32_id]: - Source: 'src/demo.rs', lines 73:0-73:28 -/ + Source: 'src/demo.rs', lines 80:0-80:28 -/ divergent def i32_id (i : I32) : Result I32 := if i = 0#i32 then Result.ret 0#i32 @@ -121,26 +128,44 @@ divergent def i32_id (i : I32) : Result I32 := let i2 ← i32_id i1 i2 + 1#i32 +/- [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 -/ +divergent def list_tail + (T : Type) (l : CList T) : + Result ((CList T) × (CList T → Result (CList T))) + := + match l with + | CList.CCons t tl => + do + let (c, list_tail_back) ← list_tail T tl + let back_'a := + fun ret => + do + let tl1 ← list_tail_back ret + Result.ret (CList.CCons t tl1) + Result.ret (c, back_'a) + | CList.CNil => Result.ret (CList.CNil, Result.ret) + /- Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 -/ + Source: 'src/demo.rs', lines 97:0-97:17 -/ structure Counter (Self : Type) where incr : Self → Result (Usize × Self) /- [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 -/ + Source: 'src/demo.rs', lines 102:4-102:31 -/ def CounterUsize.incr (self : Usize) : Result (Usize × Usize) := do let self1 ← self + 1#usize Result.ret (self, self1) /- Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 -/ + Source: 'src/demo.rs', lines 101:0-101:22 -/ def CounterUsize : Counter Usize := { incr := CounterUsize.incr } /- [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 -/ + Source: 'src/demo.rs', lines 109:0-109:59 -/ def use_counter (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) := CounterInst.incr cnt diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index cdec7332..e514ac3e 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -65,4 +65,20 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : termination_by x.val.toNat decreasing_by scalar_decr_tac +theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) : + ∃ back, list_tail T l = ret (CList.CNil, back) ∧ + ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by + rw [list_tail] + match l with + | CNil => + simp_all + | CCons hd tl => + simp_all + progress as ⟨ back ⟩ + simp + -- Proving the backward function + intro tl' + progress + simp_all + end demo diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index db15aacc..8b645037 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -38,9 +38,9 @@ def custom_swap Result (State × (T × (T → State → Result (State × (T × T))))) := do - let (st1, (t, t1)) ← core.mem.swap T x y st - let back_'a := fun ret st2 => Result.ret (st2, (ret, t1)) - Result.ret (st1, (t, back_'a)) + let (st1, (x1, y1)) ← core.mem.swap T x y st + let back_'a := fun ret st2 => Result.ret (st2, (ret, y1)) + Result.ret (st1, (x1, back_'a)) /- [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 -/ diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index f0706725..1c95f7c9 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -20,9 +20,9 @@ divergent def HashMap.allocate_slots_loop if n > 0#usize then do - let v ← alloc.vec.Vec.push (List T) slots List.Nil + let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil let n1 ← n - 1#usize - HashMap.allocate_slots_loop T v n1 + HashMap.allocate_slots_loop T slots1 n1 else Result.ret slots /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: @@ -142,8 +142,8 @@ divergent def HashMap.move_elements_from_list_loop match ls with | List.Cons k v tl => do - let hm ← HashMap.insert_no_resize T ntable k v - HashMap.move_elements_from_list_loop T hm tl + let ntable1 ← HashMap.insert_no_resize T ntable k v + HashMap.move_elements_from_list_loop T ntable1 tl | List.Nil => Result.ret ntable /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: @@ -167,12 +167,10 @@ divergent def HashMap.move_elements_loop alloc.vec.Vec.index_mut (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i let (ls, l1) := core.mem.replace (List T) l List.Nil - let hm ← HashMap.move_elements_from_list T ntable ls + let ntable1 ← HashMap.move_elements_from_list T ntable ls let i2 ← i + 1#usize let slots1 ← index_mut_back l1 - let back_'a ← HashMap.move_elements_loop T hm slots1 i2 - let (hm1, v) := back_'a - Result.ret (hm1, v) + HashMap.move_elements_loop T ntable1 slots1 i2 else Result.ret (ntable, slots) /- [hashmap::{hashmap::HashMap<T>}::move_elements]: @@ -182,10 +180,7 @@ def HashMap.move_elements : Result ((HashMap T) × (alloc.vec.Vec (List T))) := - do - let back_'a ← HashMap.move_elements_loop T ntable slots i - let (hm, v) := back_'a - Result.ret (hm, v) + HashMap.move_elements_loop T ntable slots i /- [hashmap::{hashmap::HashMap<T>}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 -/ @@ -218,11 +213,11 @@ def HashMap.insert Result (HashMap T) := do - let hm ← HashMap.insert_no_resize T self key value - let i ← HashMap.len T hm - if i > hm.max_load - then HashMap.try_resize T hm - else Result.ret hm + let self1 ← HashMap.insert_no_resize T self key value + let i ← HashMap.len T self1 + if i > self1.max_load + then HashMap.try_resize T self1 + else Result.ret self1 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 -/ @@ -311,9 +306,7 @@ def HashMap.get_mut_in_list (T : Type) (ls : List T) (key : Usize) : Result (T × (T → Result (List T))) := - do - let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key - Result.ret (t, back_'a) + HashMap.get_mut_in_list_loop T ls key /- [hashmap::{hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 -/ diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 31441b4a..6a6934b8 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -21,9 +21,9 @@ divergent def hashmap.HashMap.allocate_slots_loop if n > 0#usize then do - let v ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil + let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil let n1 ← n - 1#usize - hashmap.HashMap.allocate_slots_loop T v n1 + hashmap.HashMap.allocate_slots_loop T slots1 n1 else Result.ret slots /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: @@ -150,8 +150,8 @@ divergent def hashmap.HashMap.move_elements_from_list_loop match ls with | hashmap.List.Cons k v tl => do - let hm ← hashmap.HashMap.insert_no_resize T ntable k v - hashmap.HashMap.move_elements_from_list_loop T hm tl + let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v + hashmap.HashMap.move_elements_from_list_loop T ntable1 tl | hashmap.List.Nil => Result.ret ntable /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: @@ -177,12 +177,10 @@ divergent def hashmap.HashMap.move_elements_loop alloc.vec.Vec.index_mut (hashmap.List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i let (ls, l1) := core.mem.replace (hashmap.List T) l hashmap.List.Nil - let hm ← hashmap.HashMap.move_elements_from_list T ntable ls + let ntable1 ← hashmap.HashMap.move_elements_from_list T ntable ls let i2 ← i + 1#usize let slots1 ← index_mut_back l1 - let back_'a ← hashmap.HashMap.move_elements_loop T hm slots1 i2 - let (hm1, v) := back_'a - Result.ret (hm1, v) + hashmap.HashMap.move_elements_loop T ntable1 slots1 i2 else Result.ret (ntable, slots) /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: @@ -192,10 +190,7 @@ def hashmap.HashMap.move_elements (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T))) := - do - let back_'a ← hashmap.HashMap.move_elements_loop T ntable slots i - let (hm, v) := back_'a - Result.ret (hm, v) + hashmap.HashMap.move_elements_loop T ntable slots i /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 -/ @@ -229,11 +224,11 @@ def hashmap.HashMap.insert Result (hashmap.HashMap T) := do - let hm ← hashmap.HashMap.insert_no_resize T self key value - let i ← hashmap.HashMap.len T hm - if i > hm.max_load - then hashmap.HashMap.try_resize T hm - else Result.ret hm + let self1 ← hashmap.HashMap.insert_no_resize T self key value + let i ← hashmap.HashMap.len T self1 + if i > self1.max_load + then hashmap.HashMap.try_resize T self1 + else Result.ret self1 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 -/ @@ -326,9 +321,7 @@ def hashmap.HashMap.get_mut_in_list (T : Type) (ls : hashmap.List T) (key : Usize) : Result (T × (T → Result (hashmap.List T))) := - do - let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key - Result.ret (t, back_'a) + hashmap.HashMap.get_mut_in_list_loop T ls key /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 -/ @@ -460,8 +453,7 @@ def insert_on_disk do let (st1, hm) ← hashmap_utils.deserialize st let hm1 ← hashmap.HashMap.insert U64 hm key value - let (st2, _) ← hashmap_utils.serialize hm1 st1 - Result.ret (st2, ()) + hashmap_utils.serialize hm1 st1 /- [hashmap_main::main]: Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/ diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 433ca8f0..0f3d77c2 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -23,14 +23,14 @@ def sum (max : U32) : Result U32 := /- [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 -/ divergent def sum_with_mut_borrows_loop - (max : U32) (mi : U32) (ms : U32) : Result U32 := - if mi < max + (max : U32) (i : U32) (s : U32) : Result U32 := + if i < max then do - let ms1 ← ms + mi - let mi1 ← mi + 1#u32 - sum_with_mut_borrows_loop max mi1 ms1 - else ms * 2#u32 + let ms ← s + i + let mi ← i + 1#u32 + sum_with_mut_borrows_loop max mi ms + else s * 2#u32 /- [loops::sum_with_mut_borrows]: Source: 'src/loops.rs', lines 19:0-19:44 -/ @@ -138,9 +138,7 @@ divergent def list_nth_mut_loop_loop Source: 'src/loops.rs', lines 88:0-88:71 -/ def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := - do - let (t, back) ← list_nth_mut_loop_loop T ls i - Result.ret (t, back) + list_nth_mut_loop_loop T ls i /- [loops::list_nth_shared_loop]: loop 0: Source: 'src/loops.rs', lines 101:0-111:1 -/ @@ -189,13 +187,13 @@ def get_elem_mut Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize)))) := do - let (l, index_mut_back) ← + let (ls, index_mut_back) ← alloc.vec.Vec.index_mut (List Usize) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - let (i, back) ← get_elem_mut_loop x l + let (i, back) ← get_elem_mut_loop x ls let back1 := fun ret => do - let l1 ← back ret - index_mut_back l1 + let l ← back ret + index_mut_back l Result.ret (i, back1) /- [loops::get_elem_shared]: loop 0: @@ -213,10 +211,10 @@ divergent def get_elem_shared_loop def get_elem_shared (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := do - let l ← + let ls ← alloc.vec.Vec.index (List Usize) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - get_elem_shared_loop x l + get_elem_shared_loop x ls /- [loops::id_mut]: Source: 'src/loops.rs', lines 145:0-145:50 -/ @@ -322,9 +320,7 @@ def list_nth_mut_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T)) × (T → Result (List T))) := - do - let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i - Result.ret (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop T ls0 ls1 i /- [loops::list_nth_shared_loop_pair]: loop 0: Source: 'src/loops.rs', lines 208:0-229:1 -/ @@ -384,9 +380,7 @@ def list_nth_mut_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × ((T × T) → Result ((List T) × (List T)))) := - do - let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_mut_loop_pair_merge_loop T ls0 ls1 i /- [loops::list_nth_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 251:0-266:1 -/ @@ -443,9 +437,7 @@ def list_nth_mut_shared_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_mut_shared_loop_pair_loop T ls0 ls1 i /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 288:0-303:1 -/ @@ -480,9 +472,7 @@ def list_nth_mut_shared_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i /- [loops::list_nth_shared_mut_loop_pair]: loop 0: Source: 'src/loops.rs', lines 307:0-322:1 -/ @@ -516,9 +506,7 @@ def list_nth_shared_mut_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i - Result.ret (p, back_'b) + list_nth_shared_mut_loop_pair_loop T ls0 ls1 i /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 326:0-341:1 -/ @@ -553,19 +541,15 @@ def list_nth_shared_mut_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result ((T × T) × (T → Result (List T))) := - do - let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i - Result.ret (p, back_'a) + list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i /- [loops::ignore_input_mut_borrow]: loop 0: Source: 'src/loops.rs', lines 345:0-349:1 -/ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit := if i > 0#u32 - then - do - let i1 ← i - 1#u32 - let _ ← ignore_input_mut_borrow_loop i1 - Result.ret () + then do + let i1 ← i - 1#u32 + ignore_input_mut_borrow_loop i1 else Result.ret () /- [loops::ignore_input_mut_borrow]: @@ -579,11 +563,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 := Source: 'src/loops.rs', lines 353:0-358:1 -/ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit := if i > 0#u32 - then - do - let i1 ← i - 1#u32 - let _ ← incr_ignore_input_mut_borrow_loop i1 - Result.ret () + then do + let i1 ← i - 1#u32 + incr_ignore_input_mut_borrow_loop i1 else Result.ret () /- [loops::incr_ignore_input_mut_borrow]: @@ -598,11 +580,9 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 := Source: 'src/loops.rs', lines 362:0-366:1 -/ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit := if i > 0#u32 - then - do - let i1 ← i - 1#u32 - let _ ← ignore_input_shared_borrow_loop i1 - Result.ret () + then do + let i1 ← i - 1#u32 + ignore_input_shared_borrow_loop i1 else Result.ret () /- [loops::ignore_input_shared_borrow]: diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 2112e282..5f9ec0f2 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -487,9 +487,7 @@ def id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) := - let back_'a := fun ret => let (t, t1) := ret - Result.ret (t, t1) - Result.ret ((x, y), back_'a) + Result.ret ((x, y), Result.ret) /- [no_nested_borrows::id_mut_pair2]: Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/ @@ -498,9 +496,7 @@ def id_mut_pair2 Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) := let (t, t1) := p - let back_'a := fun ret => let (t2, t3) := ret - Result.ret (t2, t3) - Result.ret ((t, t1), back_'a) + Result.ret ((t, t1), Result.ret) /- [no_nested_borrows::id_mut_pair3]: Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/ diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 4930a05c..924ff36c 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -14,8 +14,8 @@ def ref_incr (x : I32) : Result I32 := Source: 'src/paper.rs', lines 8:0-8:18 -/ def test_incr : Result Unit := do - let i ← ref_incr 0#i32 - if ¬ (i = 1#i32) + let x ← ref_incr 0#i32 + if ¬ (x = 1#i32) then Result.fail .panic else Result.ret () |