diff --git a/ocaml/fstar-lib/FStar_Tactics_Load.ml b/ocaml/fstar-lib/FStar_Tactics_Load.ml index daa12c507e9..ed563d54aa9 100644 --- a/ocaml/fstar-lib/FStar_Tactics_Load.ml +++ b/ocaml/fstar-lib/FStar_Tactics_Load.ml @@ -21,7 +21,9 @@ let dynlink (fname:string) : unit = [EM.text (U.format1 "Failed to load plugin file %s" fname); EM.text (U.format1 "Reason: `%s`" (Dynlink.error_message e)); EM.text (U.format1 "Remove the `--load` option or use `--warn_error -%s` to ignore and continue." - (string_of_int (Z.to_int (E.errno EC.Error_PluginDynlink))))]) + (string_of_int (Z.to_int (E.errno EC.Error_PluginDynlink))))]); + (* If we weren't ignoring this error, just stop now *) + E.stop_if_err () let load_tactic tac = dynlink tac; diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml index 38a5671a6f9..c1031bd7741 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml @@ -1739,6 +1739,33 @@ let (ask_solver_quake : query_settings Prims.list -> answer) = total_ran; tried_recovery = false })) +type recovery_hammer = + | IncreaseRLimit of Prims.int + | RestartAnd of recovery_hammer +let (uu___is_IncreaseRLimit : recovery_hammer -> Prims.bool) = + fun projectee -> + match projectee with | IncreaseRLimit _0 -> true | uu___ -> false +let (__proj__IncreaseRLimit__item___0 : recovery_hammer -> Prims.int) = + fun projectee -> match projectee with | IncreaseRLimit _0 -> _0 +let (uu___is_RestartAnd : recovery_hammer -> Prims.bool) = + fun projectee -> + match projectee with | RestartAnd _0 -> true | uu___ -> false +let (__proj__RestartAnd__item___0 : recovery_hammer -> recovery_hammer) = + fun projectee -> match projectee with | RestartAnd _0 -> _0 +let rec (pp_hammer : recovery_hammer -> FStar_Pprint.document) = + fun h -> + match h with + | IncreaseRLimit factor -> + let uu___ = FStar_Errors_Msg.text "increasing its rlimit by" in + let uu___1 = + let uu___2 = FStar_Class_PP.pp FStar_Class_PP.pp_int factor in + let uu___3 = FStar_Pprint.doc_of_string "x" in + FStar_Pprint.op_Hat_Hat uu___2 uu___3 in + FStar_Pprint.op_Hat_Slash_Hat uu___ uu___1 + | RestartAnd h1 -> + let uu___ = FStar_Errors_Msg.text "restarting the solver and" in + let uu___1 = pp_hammer h1 in + FStar_Pprint.op_Hat_Slash_Hat uu___ uu___1 let (ask_solver_recover : query_settings Prims.list -> answer) = fun configs -> let uu___ = FStar_Options.proof_recovery () in @@ -1748,13 +1775,14 @@ let (ask_solver_recover : query_settings Prims.list -> answer) = (if r.ok then r else - (let last_cfg = FStar_Compiler_List.last configs in + (let restarted = FStar_Compiler_Util.mk_ref false in + let cfg = FStar_Compiler_List.last configs in (let uu___3 = let uu___4 = FStar_Errors_Msg.text "This query failed to be solved. Will now retry with higher rlimits due to --proof_recovery." in [uu___4] in - FStar_Errors.diag_doc last_cfg.query_range uu___3); + FStar_Errors.diag_doc cfg.query_range uu___3); (let try_factor n = (let uu___4 = let uu___5 = @@ -1763,29 +1791,41 @@ let (ask_solver_recover : query_settings Prims.list -> answer) = let uu___7 = FStar_Class_PP.pp FStar_Class_PP.pp_int n in FStar_Pprint.op_Hat_Slash_Hat uu___6 uu___7 in [uu___5] in - FStar_Errors.diag_doc last_cfg.query_range uu___4); - (let cfg = + FStar_Errors.diag_doc cfg.query_range uu___4); + (let cfg1 = { - query_env = (last_cfg.query_env); - query_decl = (last_cfg.query_decl); - query_name = (last_cfg.query_name); - query_index = (last_cfg.query_index); - query_range = (last_cfg.query_range); - query_fuel = (last_cfg.query_fuel); - query_ifuel = (last_cfg.query_ifuel); - query_rlimit = (FStar_Mul.op_Star n last_cfg.query_rlimit); - query_hint = (last_cfg.query_hint); - query_errors = (last_cfg.query_errors); - query_all_labels = (last_cfg.query_all_labels); - query_suffix = (last_cfg.query_suffix); - query_hash = (last_cfg.query_hash); + query_env = (cfg.query_env); + query_decl = (cfg.query_decl); + query_name = (cfg.query_name); + query_index = (cfg.query_index); + query_range = (cfg.query_range); + query_fuel = (cfg.query_fuel); + query_ifuel = (cfg.query_ifuel); + query_rlimit = (FStar_Mul.op_Star n cfg.query_rlimit); + query_hint = (cfg.query_hint); + query_errors = (cfg.query_errors); + query_all_labels = (cfg.query_all_labels); + query_suffix = (cfg.query_suffix); + query_hash = (cfg.query_hash); query_can_be_split_and_retried = - (last_cfg.query_can_be_split_and_retried); - query_term = (last_cfg.query_term) + (cfg.query_can_be_split_and_retried); + query_term = (cfg.query_term) } in - ask_solver_quake [cfg]) in - let rec aux factors = - match factors with + ask_solver_quake [cfg1]) in + let rec try_hammer h = + match h with + | IncreaseRLimit factor -> try_factor factor + | RestartAnd h1 -> + ((let uu___4 = + let uu___5 = + FStar_Errors_Msg.text "Trying a solver restart" in + [uu___5] in + FStar_Errors.diag_doc cfg.query_range uu___4); + ((cfg.query_env).FStar_TypeChecker_Env.solver).FStar_TypeChecker_Env.refresh + (); + try_hammer h1) in + let rec aux hammers = + match hammers with | [] -> { ok = (r.ok); @@ -1798,8 +1838,8 @@ let (ask_solver_recover : query_settings Prims.list -> answer) = total_ran = (r.total_ran); tried_recovery = true } - | n::ns -> - let r1 = try_factor n in + | h::hs -> + let r1 = try_hammer h in if r1.ok then ((let uu___4 = @@ -1807,12 +1847,8 @@ let (ask_solver_recover : query_settings Prims.list -> answer) = let uu___6 = let uu___7 = FStar_Errors_Msg.text - "This query succeeded after increasing its rlimit by" in - let uu___8 = - let uu___9 = - FStar_Class_PP.pp FStar_Class_PP.pp_int n in - let uu___10 = FStar_Pprint.doc_of_string "x" in - FStar_Pprint.op_Hat_Hat uu___9 uu___10 in + "This query succeeded after " in + let uu___8 = pp_hammer h in FStar_Pprint.op_Hat_Slash_Hat uu___7 uu___8 in let uu___7 = let uu___8 = @@ -1821,11 +1857,54 @@ let (ask_solver_recover : query_settings Prims.list -> answer) = [uu___8] in uu___6 :: uu___7 in (FStar_Errors_Codes.Warning_ProofRecovery, uu___5) in - FStar_Errors.log_issue_doc last_cfg.query_range uu___4); + FStar_Errors.log_issue_doc cfg.query_range uu___4); r1) - else aux ns in - aux [(Prims.of_int (2)); (Prims.of_int (4)); (Prims.of_int (8))]))) + else aux hs in + aux + [IncreaseRLimit (Prims.of_int (2)); + IncreaseRLimit (Prims.of_int (4)); + IncreaseRLimit (Prims.of_int (8)); + RestartAnd (IncreaseRLimit (Prims.of_int (8)))]))) else ask_solver_quake configs +let (failing_query_ctr : Prims.int FStar_Compiler_Effect.ref) = + FStar_Compiler_Util.mk_ref Prims.int_zero +let (maybe_save_failing_query : + FStar_TypeChecker_Env.env_t -> + FStar_SMTEncoding_Term.decl Prims.list -> query_settings -> unit) + = + fun env -> + fun prefix -> + fun qs -> + let uu___ = FStar_Options.proof_recovery () in + if uu___ + then + let mod1 = + let uu___1 = FStar_TypeChecker_Env.current_module env in + FStar_Class_Show.show FStar_Ident.showable_lident uu___1 in + let n = + (let uu___2 = + let uu___3 = FStar_Compiler_Effect.op_Bang failing_query_ctr in + uu___3 + Prims.int_one in + FStar_Compiler_Effect.op_Colon_Equals failing_query_ctr uu___2); + FStar_Compiler_Effect.op_Bang failing_query_ctr in + let file_name = + let uu___1 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) n in + FStar_Compiler_Util.format2 "failedQueries-%s-%s.smt2" mod1 + uu___1 in + let query_str = + let uu___1 = with_fuel_and_diagnostics qs [] in + let uu___2 = + let uu___3 = FStar_Compiler_Util.string_of_int qs.query_index in + FStar_Compiler_Util.format2 "(%s, %s)" qs.query_name uu___3 in + FStar_SMTEncoding_Z3.ask_text qs.query_range + (filter_assertions qs.query_env FStar_Pervasives_Native.None + qs.query_hint) qs.query_hash qs.query_all_labels uu___1 + uu___2 in + FStar_Compiler_Util.write_file file_name query_str + else () let (ask_solver : Prims.bool -> Prims.bool -> @@ -1882,7 +1961,13 @@ let (ask_solver : ans_ok) else (FStar_SMTEncoding_Z3.giveZ3 prefix; - ask_solver_recover configs) in + (let ans1 = ask_solver_recover configs in + if Prims.op_Negation ans1.ok + then + (let uu___4 = FStar_Compiler_List.last configs in + maybe_save_failing_query env prefix uu___4) + else (); + ans1)) in (configs, ans) let (report : FStar_TypeChecker_Env.env -> query_settings -> answer -> unit) = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml index 1f26e4885e8..3fd0648d59e 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml @@ -369,17 +369,47 @@ let (check_z3version : FStar_Compiler_Util.proc -> unit) = then ((let uu___4 = let uu___5 = - let uu___6 = FStar_Compiler_Util.proc_prog p in + let uu___6 = + let uu___7 = + let uu___8 = FStar_Compiler_Util.proc_prog p in + FStar_Compiler_Util.format3 + "Unexpected Z3 version for '%s': expected '%s', got '%s'." + uu___8 ver_conf ver_found in + FStar_Errors_Msg.text uu___7 in let uu___7 = let uu___8 = - let uu___9 = FStar_Options.z3_version () in - Prims.op_Hat "z3-" uu___9 in - FStar_Platform.exe uu___8 in - FStar_Compiler_Util.format5 - "Unexpected Z3 version for `%s': expected `%s', got `%s'.\nPlease download the correct version of Z3 from %s\nand install it into your $PATH as `%s'." - uu___6 ver_conf ver_found z3url uu___7 in + let uu___9 = + let uu___10 = + FStar_Errors_Msg.text + "Please download the correct version of Z3 from" in + let uu___11 = FStar_Pprint.url z3url in + FStar_Pprint.prefix (Prims.of_int (4)) Prims.int_one + uu___10 uu___11 in + let uu___10 = + let uu___11 = + let uu___12 = + FStar_Errors_Msg.text + "and install it into your $PATH as" in + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 = FStar_Options.z3_version () in + Prims.op_Hat "z3-" uu___18 in + FStar_Platform.exe uu___17 in + FStar_Pprint.doc_of_string uu___16 in + FStar_Pprint.squotes uu___15 in + FStar_Pprint.op_Hat_Hat uu___14 FStar_Pprint.dot in + FStar_Pprint.op_Hat_Slash_Hat uu___12 uu___13 in + FStar_Pprint.group uu___11 in + FStar_Pprint.op_Hat_Slash_Hat uu___9 uu___10 in + [uu___8] in + uu___6 :: uu___7 in (FStar_Errors_Codes.Warning_SolverMismatch, uu___5) in - FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange uu___4); + FStar_Errors.log_issue_doc FStar_Compiler_Range_Type.dummyRange + uu___4); + FStar_Errors.stop_if_err (); FStar_Compiler_Effect.op_Colon_Equals _already_warned_version_mismatch true) else ()) @@ -1006,13 +1036,35 @@ let (mk_input : fun fresh -> fun theory -> let ver = FStar_Options.z3_version () in - let options = z3_options ver in + let options = "; Z3 invocation started by F*\n" in let options1 = + let uu___ = + let uu___1 = + let uu___2 = FStar_Compiler_Effect.op_Bang FStar_Options._version in + let uu___3 = + let uu___4 = + let uu___5 = + FStar_Compiler_Effect.op_Bang FStar_Options._commit in + Prims.op_Hat uu___5 "\n" in + Prims.op_Hat " -- hash: " uu___4 in + Prims.op_Hat uu___2 uu___3 in + Prims.op_Hat "; F* version: " uu___1 in + Prims.op_Hat options uu___ in + let options2 = + let uu___ = + let uu___1 = + let uu___2 = FStar_Options.z3_version () in + Prims.op_Hat uu___2 "\n" in + Prims.op_Hat "; Z3 version (according to F*): " uu___1 in + Prims.op_Hat options1 uu___ in + let options3 = + let uu___ = z3_options ver in Prims.op_Hat options2 uu___ in + let options4 = let uu___ = let uu___1 = FStar_Options.z3_smtopt () in FStar_Compiler_Effect.op_Bar_Greater uu___1 (FStar_Compiler_String.concat "\n") in - Prims.op_Hat options uu___ in + Prims.op_Hat options3 uu___ in (let uu___1 = FStar_Options.print_z3_statistics () in if uu___1 then context_profile theory else ()); (let uu___1 = @@ -1036,7 +1088,7 @@ let (mk_input : | (prefix, check_sat, suffix) -> let pp = FStar_Compiler_List.map - (FStar_SMTEncoding_Term.declToSmt options1) in + (FStar_SMTEncoding_Term.declToSmt options4) in let suffix1 = check_sat :: suffix in let ps_lines = pp prefix in let ss_lines = pp suffix1 in @@ -1049,7 +1101,7 @@ let (mk_input : let uu___5 = FStar_Compiler_Effect.op_Bar_Greater prefix (FStar_Compiler_List.map - (FStar_SMTEncoding_Term.declToSmt_no_caps options1)) in + (FStar_SMTEncoding_Term.declToSmt_no_caps options4)) in FStar_Compiler_Effect.op_Bar_Greater uu___5 (FStar_Compiler_String.concat "\n") else ps in @@ -1062,7 +1114,7 @@ let (mk_input : (let uu___4 = let uu___5 = FStar_Compiler_List.map - (FStar_SMTEncoding_Term.declToSmt options1) theory in + (FStar_SMTEncoding_Term.declToSmt options4) theory in FStar_Compiler_Effect.op_Bar_Greater uu___5 (FStar_Compiler_String.concat "\n") in (uu___4, FStar_Pervasives_Native.None)) in @@ -1148,6 +1200,33 @@ let (z3_job : z3result_query_hash = qhash; z3result_log_file = log_file } +let (ask_text : + FStar_Compiler_Range_Type.range -> + (FStar_SMTEncoding_Term.decl Prims.list -> + (FStar_SMTEncoding_Term.decl Prims.list * Prims.bool)) + -> + Prims.string FStar_Pervasives_Native.option -> + FStar_SMTEncoding_Term.error_labels -> + FStar_SMTEncoding_Term.decl Prims.list -> + Prims.string -> Prims.string) + = + fun r -> + fun filter_theory -> + fun cache -> + fun label_messages -> + fun qry -> + fun queryid -> + let theory = flatten_fresh_scope () in + let theory1 = + FStar_Compiler_List.op_At theory + (FStar_Compiler_List.op_At [FStar_SMTEncoding_Term.Push] + (FStar_Compiler_List.op_At qry + [FStar_SMTEncoding_Term.Pop])) in + let uu___ = filter_theory theory1 in + match uu___ with + | (theory2, _used_unsat_core) -> + let uu___1 = mk_input true theory2 in + (match uu___1 with | (input, qhash, log_file_name) -> input) let (ask : FStar_Compiler_Range_Type.range -> (FStar_SMTEncoding_Term.decl Prims.list -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml index cb7d3fb6742..fdef1b52b72 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml @@ -3455,138 +3455,144 @@ let run_tactic_on_ps' : else ()); (match res with | FStar_Tactics_Result.Success (ret, ps3) -> - let remaining_smt_goals = - FStar_Compiler_List.op_At - ps3.FStar_Tactics_Types.goals - ps3.FStar_Tactics_Types.smt_goals in - (FStar_Compiler_List.iter - (fun g1 -> - FStar_Tactics_V2_Basic.mark_goal_implicit_already_checked - g1; - (let uu___7 = - FStar_Tactics_V2_Basic.is_irrelevant g1 in - if uu___7 - then - ((let uu___9 = - FStar_Compiler_Effect.op_Bang tacdbg in - if uu___9 - then - let uu___10 = - let uu___11 = - FStar_Tactics_Types.goal_witness - g1 in - FStar_Class_Show.show - FStar_Syntax_Print.showable_term - uu___11 in - FStar_Compiler_Util.print1 - "Assigning irrelevant goal %s\n" - uu___10 - else ()); - (let uu___9 = - let uu___10 = - FStar_Tactics_Types.goal_env g1 in - let uu___11 = - FStar_Tactics_Types.goal_witness g1 in - FStar_TypeChecker_Rel.teq_nosmt_force - uu___10 uu___11 - FStar_Syntax_Util.exp_unit in - if uu___9 - then () - else - (let uu___11 = - let uu___12 = - let uu___13 = - FStar_Tactics_Types.goal_witness - g1 in - FStar_Class_Show.show - FStar_Syntax_Print.showable_term - uu___13 in - FStar_Compiler_Util.format1 - "Irrelevant tactic witness does not unify with (): %s" - uu___12 in - failwith uu___11))) - else ())) remaining_smt_goals; - (let uu___7 = + ((let uu___6 = FStar_Compiler_Effect.op_Bang tacdbg in - if uu___7 + if uu___6 then - let uu___8 = - (FStar_Common.string_of_list ()) - (fun imp -> - FStar_Class_Show.show - FStar_Syntax_Print.showable_ctxu - imp.FStar_TypeChecker_Common.imp_uvar) - ps3.FStar_Tactics_Types.all_implicits in - FStar_Compiler_Util.print1 - "About to check tactic implicits: %s\n" - uu___8 + FStar_Tactics_Printing.do_dump_proofstate ps3 + "at the finish line" else ()); - (let g1 = - { - FStar_TypeChecker_Common.guard_f = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.guard_f); - FStar_TypeChecker_Common.deferred_to_tac = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = - (ps3.FStar_Tactics_Types.all_implicits) - } in - let g2 = - FStar_TypeChecker_Rel.solve_deferred_constraints - env g1 in - (let uu___8 = - FStar_Compiler_Effect.op_Bang tacdbg in - if uu___8 - then - let uu___9 = - FStar_Class_Show.show - (FStar_Class_Show.printableshow - FStar_Class_Printable.printable_nat) - (FStar_Compiler_List.length - ps3.FStar_Tactics_Types.all_implicits) in - let uu___10 = - FStar_Class_Show.show - (FStar_Class_Show.show_list - FStar_TypeChecker_Common.show_implicit) - ps3.FStar_Tactics_Types.all_implicits in - FStar_Compiler_Util.print2 - "Checked %s implicits (1): %s\n" uu___9 - uu___10 - else ()); - (let tagged_implicits = - FStar_TypeChecker_Rel.resolve_implicits_tac - env g2 in - (let uu___9 = - FStar_Compiler_Effect.op_Bang tacdbg in - if uu___9 - then - let uu___10 = - FStar_Class_Show.show - (FStar_Class_Show.printableshow - FStar_Class_Printable.printable_nat) - (FStar_Compiler_List.length - ps3.FStar_Tactics_Types.all_implicits) in - let uu___11 = - FStar_Class_Show.show - (FStar_Class_Show.show_list - FStar_TypeChecker_Common.show_implicit) - ps3.FStar_Tactics_Types.all_implicits in - FStar_Compiler_Util.print2 - "Checked %s implicits (2): %s\n" uu___10 - uu___11 - else ()); - report_implicits rng_goal tagged_implicits; - (let uu___11 = - FStar_Compiler_Effect.op_Bang tacdbg in - if uu___11 - then - FStar_Tactics_Printing.do_dump_proofstate - ps3 "at the finish line" - else ()); - (remaining_smt_goals, ret)))) + (let remaining_smt_goals = + FStar_Compiler_List.op_At + ps3.FStar_Tactics_Types.goals + ps3.FStar_Tactics_Types.smt_goals in + FStar_Compiler_List.iter + (fun g1 -> + FStar_Tactics_V2_Basic.mark_goal_implicit_already_checked + g1; + (let uu___8 = + FStar_Tactics_V2_Basic.is_irrelevant g1 in + if uu___8 + then + ((let uu___10 = + FStar_Compiler_Effect.op_Bang tacdbg in + if uu___10 + then + let uu___11 = + let uu___12 = + FStar_Tactics_Types.goal_witness + g1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + uu___12 in + FStar_Compiler_Util.print1 + "Assigning irrelevant goal %s\n" + uu___11 + else ()); + (let uu___10 = + let uu___11 = + FStar_Tactics_Types.goal_env g1 in + let uu___12 = + FStar_Tactics_Types.goal_witness + g1 in + FStar_TypeChecker_Rel.teq_nosmt_force + uu___11 uu___12 + FStar_Syntax_Util.exp_unit in + if uu___10 + then () + else + (let uu___12 = + let uu___13 = + let uu___14 = + FStar_Tactics_Types.goal_witness + g1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + uu___14 in + FStar_Compiler_Util.format1 + "Irrelevant tactic witness does not unify with (): %s" + uu___13 in + failwith uu___12))) + else ())) remaining_smt_goals; + FStar_Errors.with_ctx + "While checking implicits left by a tactic" + (fun uu___8 -> + (let uu___10 = + FStar_Compiler_Effect.op_Bang tacdbg in + if uu___10 + then + let uu___11 = + (FStar_Common.string_of_list ()) + (fun imp -> + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu + imp.FStar_TypeChecker_Common.imp_uvar) + ps3.FStar_Tactics_Types.all_implicits in + FStar_Compiler_Util.print1 + "About to check tactic implicits: %s\n" + uu___11 + else ()); + (let g1 = + { + FStar_TypeChecker_Common.guard_f = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.guard_f); + FStar_TypeChecker_Common.deferred_to_tac + = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); + FStar_TypeChecker_Common.deferred = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); + FStar_TypeChecker_Common.univ_ineqs = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); + FStar_TypeChecker_Common.implicits = + (ps3.FStar_Tactics_Types.all_implicits) + } in + let g2 = + FStar_TypeChecker_Rel.solve_deferred_constraints + env g1 in + (let uu___11 = + FStar_Compiler_Effect.op_Bang tacdbg in + if uu___11 + then + let uu___12 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat) + (FStar_Compiler_List.length + ps3.FStar_Tactics_Types.all_implicits) in + let uu___13 = + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_TypeChecker_Common.show_implicit) + ps3.FStar_Tactics_Types.all_implicits in + FStar_Compiler_Util.print2 + "Checked %s implicits (1): %s\n" + uu___12 uu___13 + else ()); + (let tagged_implicits = + FStar_TypeChecker_Rel.resolve_implicits_tac + env g2 in + (let uu___12 = + FStar_Compiler_Effect.op_Bang tacdbg in + if uu___12 + then + let uu___13 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat) + (FStar_Compiler_List.length + ps3.FStar_Tactics_Types.all_implicits) in + let uu___14 = + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_TypeChecker_Common.show_implicit) + ps3.FStar_Tactics_Types.all_implicits in + FStar_Compiler_Util.print2 + "Checked %s implicits (2): %s\n" + uu___13 uu___14 + else ()); + report_implicits rng_goal + tagged_implicits))); + (remaining_smt_goals, ret))) | FStar_Tactics_Result.Failed (FStar_Errors.Error (code, msg, rng, ctx), ps3) -> let msg1 = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml index 1b72abd28a0..9bade554374 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml @@ -126,6 +126,68 @@ let (uu___is_NonTrivial : guard_formula -> Prims.bool) = let (__proj__NonTrivial__item___0 : guard_formula -> FStar_Syntax_Syntax.formula) = fun projectee -> match projectee with | NonTrivial _0 -> _0 +let (mk_by_tactic : + FStar_Syntax_Syntax.term -> + FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) + = + fun tac -> + fun f -> + let t_by_tactic = + let uu___ = + FStar_Syntax_Syntax.tabbrev FStar_Parser_Const.by_tactic_lid in + FStar_Syntax_Syntax.mk_Tm_uinst uu___ [FStar_Syntax_Syntax.U_zero] in + let uu___ = + let uu___1 = FStar_Syntax_Syntax.as_arg tac in + let uu___2 = let uu___3 = FStar_Syntax_Syntax.as_arg f in [uu___3] in + uu___1 :: uu___2 in + FStar_Syntax_Syntax.mk_Tm_app t_by_tactic uu___ + FStar_Compiler_Range_Type.dummyRange +let rec (delta_depth_greater_than : + FStar_Syntax_Syntax.delta_depth -> + FStar_Syntax_Syntax.delta_depth -> Prims.bool) + = + fun l -> + fun m -> + match (l, m) with + | (FStar_Syntax_Syntax.Delta_equational_at_level i, + FStar_Syntax_Syntax.Delta_equational_at_level j) -> i > j + | (FStar_Syntax_Syntax.Delta_constant_at_level i, + FStar_Syntax_Syntax.Delta_constant_at_level j) -> i > j + | (FStar_Syntax_Syntax.Delta_abstract d, uu___) -> + delta_depth_greater_than d m + | (uu___, FStar_Syntax_Syntax.Delta_abstract d) -> + delta_depth_greater_than l d + | (FStar_Syntax_Syntax.Delta_equational_at_level uu___, uu___1) -> true + | (uu___, FStar_Syntax_Syntax.Delta_equational_at_level uu___1) -> + false +let rec (decr_delta_depth : + FStar_Syntax_Syntax.delta_depth -> + FStar_Syntax_Syntax.delta_depth FStar_Pervasives_Native.option) + = + fun uu___ -> + match uu___ with + | FStar_Syntax_Syntax.Delta_constant_at_level uu___1 when + uu___1 = Prims.int_zero -> FStar_Pervasives_Native.None + | FStar_Syntax_Syntax.Delta_equational_at_level uu___1 when + uu___1 = Prims.int_zero -> FStar_Pervasives_Native.None + | FStar_Syntax_Syntax.Delta_constant_at_level i -> + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Delta_constant_at_level (i - Prims.int_one)) + | FStar_Syntax_Syntax.Delta_equational_at_level i -> + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Delta_equational_at_level (i - Prims.int_one)) + | FStar_Syntax_Syntax.Delta_abstract d -> decr_delta_depth d +let (showable_guard_formula : guard_formula FStar_Class_Show.showable) = + { + FStar_Class_Show.show = + (fun uu___ -> + match uu___ with + | Trivial -> "Trivial" + | NonTrivial f -> + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term f in + Prims.op_Hat "NonTrivial " uu___1) + } type deferred_reason = | Deferred_univ_constraint | Deferred_occur_check_failed @@ -176,6 +238,23 @@ let (uu___is_Deferred_delay_match_heuristic : deferred_reason -> Prims.bool) let (uu___is_Deferred_to_user_tac : deferred_reason -> Prims.bool) = fun projectee -> match projectee with | Deferred_to_user_tac -> true | uu___ -> false +let (showable_deferred_reason : deferred_reason FStar_Class_Show.showable) = + { + FStar_Class_Show.show = + (fun uu___ -> + match uu___ with + | Deferred_univ_constraint -> "Deferred_univ_constraint" + | Deferred_occur_check_failed -> "Deferred_occur_check_failed" + | Deferred_first_order_heuristic_failed -> + "Deferred_first_order_heuristic_failed" + | Deferred_flex -> "Deferred_flex" + | Deferred_free_names_check_failed -> + "Deferred_free_names_check_failed" + | Deferred_not_a_pattern -> "Deferred_not_a_pattern" + | Deferred_flex_flex_nonpattern -> "Deferred_flex_flex_nonpattern" + | Deferred_delay_match_heuristic -> "Deferred_delay_match_heuristic" + | Deferred_to_user_tac -> "Deferred_to_user_tac") + } type deferred = (deferred_reason * Prims.string * prob) Prims.list type univ_ineq = (FStar_Syntax_Syntax.universe * FStar_Syntax_Syntax.universe) @@ -225,57 +304,6 @@ let (__proj__Mkid_info_table__item__id_info_buffer : fun projectee -> match projectee with | { id_info_enabled; id_info_db; id_info_buffer;_} -> id_info_buffer -let (mk_by_tactic : - FStar_Syntax_Syntax.term -> - FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) - = - fun tac -> - fun f -> - let t_by_tactic = - let uu___ = - FStar_Syntax_Syntax.tabbrev FStar_Parser_Const.by_tactic_lid in - FStar_Syntax_Syntax.mk_Tm_uinst uu___ [FStar_Syntax_Syntax.U_zero] in - let uu___ = - let uu___1 = FStar_Syntax_Syntax.as_arg tac in - let uu___2 = let uu___3 = FStar_Syntax_Syntax.as_arg f in [uu___3] in - uu___1 :: uu___2 in - FStar_Syntax_Syntax.mk_Tm_app t_by_tactic uu___ - FStar_Compiler_Range_Type.dummyRange -let rec (delta_depth_greater_than : - FStar_Syntax_Syntax.delta_depth -> - FStar_Syntax_Syntax.delta_depth -> Prims.bool) - = - fun l -> - fun m -> - match (l, m) with - | (FStar_Syntax_Syntax.Delta_equational_at_level i, - FStar_Syntax_Syntax.Delta_equational_at_level j) -> i > j - | (FStar_Syntax_Syntax.Delta_constant_at_level i, - FStar_Syntax_Syntax.Delta_constant_at_level j) -> i > j - | (FStar_Syntax_Syntax.Delta_abstract d, uu___) -> - delta_depth_greater_than d m - | (uu___, FStar_Syntax_Syntax.Delta_abstract d) -> - delta_depth_greater_than l d - | (FStar_Syntax_Syntax.Delta_equational_at_level uu___, uu___1) -> true - | (uu___, FStar_Syntax_Syntax.Delta_equational_at_level uu___1) -> - false -let rec (decr_delta_depth : - FStar_Syntax_Syntax.delta_depth -> - FStar_Syntax_Syntax.delta_depth FStar_Pervasives_Native.option) - = - fun uu___ -> - match uu___ with - | FStar_Syntax_Syntax.Delta_constant_at_level uu___1 when - uu___1 = Prims.int_zero -> FStar_Pervasives_Native.None - | FStar_Syntax_Syntax.Delta_equational_at_level uu___1 when - uu___1 = Prims.int_zero -> FStar_Pervasives_Native.None - | FStar_Syntax_Syntax.Delta_constant_at_level i -> - FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Delta_constant_at_level (i - Prims.int_one)) - | FStar_Syntax_Syntax.Delta_equational_at_level i -> - FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Delta_equational_at_level (i - Prims.int_one)) - | FStar_Syntax_Syntax.Delta_abstract d -> decr_delta_depth d let (insert_col_info : Prims.int -> identifier_info -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index 2228c4ae461..f2c20517889 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -14211,150 +14211,159 @@ let (try_solve_deferred_constraints : smt_ok && (let uu___ = FStar_Options.ml_ish () in Prims.op_Negation uu___) in - let uu___ = - let uu___1 = - let uu___2 = FStar_TypeChecker_Env.current_module env in - FStar_Ident.string_of_lid uu___2 in - FStar_Pervasives_Native.Some uu___1 in - FStar_Profiling.profile - (fun uu___1 -> - let typeclass_variables = - FStar_Compiler_Effect.op_Bar_Greater - g.FStar_TypeChecker_Common.implicits - (FStar_Compiler_List.collect - (fun i -> - match (i.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_meta - with - | FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Ctx_uvar_meta_tac tac) -> - let uu___2 = - FStar_Syntax_Util.head_and_args_full tac in - (match uu___2 with - | (head, uu___3) -> - let uu___4 = - FStar_Syntax_Util.is_fvar - FStar_Parser_Const.tcresolve_lid head in - if uu___4 - then - let goal_type = - FStar_Syntax_Util.ctx_uvar_typ - i.FStar_TypeChecker_Common.imp_uvar in - let uvs = - FStar_Syntax_Free.uvars goal_type in - FStar_Compiler_Util.set_elements uvs - else []) - | uu___2 -> [])) in - let wl = + FStar_Errors.with_ctx "While solving deferred constraints" + (fun uu___ -> + let uu___1 = let uu___2 = - wl_of_guard env g.FStar_TypeChecker_Common.deferred in - { - attempting = (uu___2.attempting); - wl_deferred = (uu___2.wl_deferred); - wl_deferred_to_tac = (uu___2.wl_deferred_to_tac); - ctr = (uu___2.ctr); - defer_ok; - smt_ok = smt_ok1; - umax_heuristic_ok = (uu___2.umax_heuristic_ok); - tcenv = (uu___2.tcenv); - wl_implicits = (uu___2.wl_implicits); - repr_subcomp_allowed = (uu___2.repr_subcomp_allowed); - typeclass_variables - } in - let fail uu___2 = - match uu___2 with - | (d, s) -> - let msg = explain wl d s in - FStar_Errors.raise_error - (FStar_Errors_Codes.Fatal_ErrorInSolveDeferredConstraints, - msg) (p_loc d) in - (let uu___3 = - FStar_Compiler_Effect.op_Less_Bar - (FStar_TypeChecker_Env.debug env) - (FStar_Options.Other "Rel") in - if uu___3 - then - let uu___4 = - FStar_Compiler_Util.string_of_bool deferred_to_tac_ok in - let uu___5 = wl_to_string wl in - let uu___6 = - FStar_Compiler_Util.string_of_int - (FStar_Compiler_List.length - g.FStar_TypeChecker_Common.implicits) in - FStar_Compiler_Util.print4 - "Trying to solve carried problems (defer_ok=%s) (deferred_to_tac_ok=%s): begin\n\t%s\nend\n and %s implicits\n" - (string_of_defer_ok defer_ok) uu___4 uu___5 uu___6 - else ()); - (let g1 = - let uu___3 = solve_and_commit wl fail in - match uu___3 with - | FStar_Pervasives_Native.Some - (uu___4::uu___5, uu___6, uu___7) when - defer_ok = NoDefer -> - failwith - "Impossible: Unexpected deferred constraints remain" - | FStar_Pervasives_Native.Some - (deferred, defer_to_tac, imps) -> + let uu___3 = FStar_TypeChecker_Env.current_module env in + FStar_Ident.string_of_lid uu___3 in + FStar_Pervasives_Native.Some uu___2 in + FStar_Profiling.profile + (fun uu___2 -> + let typeclass_variables = + FStar_Compiler_Effect.op_Bar_Greater + g.FStar_TypeChecker_Common.implicits + (FStar_Compiler_List.collect + (fun i -> + match (i.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_meta + with + | FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Ctx_uvar_meta_tac + tac) -> + let uu___3 = + FStar_Syntax_Util.head_and_args_full + tac in + (match uu___3 with + | (head, uu___4) -> + let uu___5 = + FStar_Syntax_Util.is_fvar + FStar_Parser_Const.tcresolve_lid + head in + if uu___5 + then + let goal_type = + FStar_Syntax_Util.ctx_uvar_typ + i.FStar_TypeChecker_Common.imp_uvar in + let uvs = + FStar_Syntax_Free.uvars + goal_type in + FStar_Compiler_Util.set_elements + uvs + else []) + | uu___3 -> [])) in + let wl = + let uu___3 = + wl_of_guard env g.FStar_TypeChecker_Common.deferred in + { + attempting = (uu___3.attempting); + wl_deferred = (uu___3.wl_deferred); + wl_deferred_to_tac = (uu___3.wl_deferred_to_tac); + ctr = (uu___3.ctr); + defer_ok; + smt_ok = smt_ok1; + umax_heuristic_ok = (uu___3.umax_heuristic_ok); + tcenv = (uu___3.tcenv); + wl_implicits = (uu___3.wl_implicits); + repr_subcomp_allowed = + (uu___3.repr_subcomp_allowed); + typeclass_variables + } in + let fail uu___3 = + match uu___3 with + | (d, s) -> + let msg = explain wl d s in + FStar_Errors.raise_error + (FStar_Errors_Codes.Fatal_ErrorInSolveDeferredConstraints, + msg) (p_loc d) in + (let uu___4 = + FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug env) + (FStar_Options.Other "Rel") in + if uu___4 + then + let uu___5 = + FStar_Compiler_Util.string_of_bool + deferred_to_tac_ok in + let uu___6 = wl_to_string wl in + let uu___7 = + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length + g.FStar_TypeChecker_Common.implicits) in + FStar_Compiler_Util.print4 + "Trying to solve carried problems (defer_ok=%s) (deferred_to_tac_ok=%s): begin\n\t%s\nend\n and %s implicits\n" + (string_of_defer_ok defer_ok) uu___5 uu___6 uu___7 + else ()); + (let g1 = + let uu___4 = solve_and_commit wl fail in + match uu___4 with + | FStar_Pervasives_Native.Some + (uu___5::uu___6, uu___7, uu___8) when + defer_ok = NoDefer -> + failwith + "Impossible: Unexpected deferred constraints remain" + | FStar_Pervasives_Native.Some + (deferred, defer_to_tac, imps) -> + { + FStar_TypeChecker_Common.guard_f = + (g.FStar_TypeChecker_Common.guard_f); + FStar_TypeChecker_Common.deferred_to_tac = + (FStar_Compiler_List.op_At + g.FStar_TypeChecker_Common.deferred_to_tac + defer_to_tac); + FStar_TypeChecker_Common.deferred = deferred; + FStar_TypeChecker_Common.univ_ineqs = + (g.FStar_TypeChecker_Common.univ_ineqs); + FStar_TypeChecker_Common.implicits = + (FStar_Compiler_List.op_At + g.FStar_TypeChecker_Common.implicits imps) + } + | uu___5 -> + failwith + "Impossible: should have raised a failure already" in + solve_universe_inequalities env + g1.FStar_TypeChecker_Common.univ_ineqs; + (let g2 = + if deferred_to_tac_ok + then + let uu___5 = + let uu___6 = + let uu___7 = + FStar_TypeChecker_Env.current_module env in + FStar_Ident.string_of_lid uu___7 in + FStar_Pervasives_Native.Some uu___6 in + FStar_Profiling.profile + (fun uu___6 -> + FStar_TypeChecker_DeferredImplicits.solve_deferred_to_tactic_goals + env g1) uu___5 + "FStar.TypeChecker.Rel.solve_deferred_to_tactic_goals" + else g1 in + (let uu___6 = + FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug env) + (FStar_Options.Other "ResolveImplicitsHook") in + if uu___6 + then + let uu___7 = guard_to_string env g2 in + let uu___8 = + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length + g2.FStar_TypeChecker_Common.implicits) in + FStar_Compiler_Util.print2 + "ResolveImplicitsHook: Solved deferred to tactic goals, remaining guard is\n%s (and %s implicits)\n" + uu___7 uu___8 + else ()); { FStar_TypeChecker_Common.guard_f = - (g.FStar_TypeChecker_Common.guard_f); + (g2.FStar_TypeChecker_Common.guard_f); FStar_TypeChecker_Common.deferred_to_tac = - (FStar_Compiler_List.op_At - g.FStar_TypeChecker_Common.deferred_to_tac - defer_to_tac); - FStar_TypeChecker_Common.deferred = deferred; - FStar_TypeChecker_Common.univ_ineqs = - (g.FStar_TypeChecker_Common.univ_ineqs); + (g2.FStar_TypeChecker_Common.deferred_to_tac); + FStar_TypeChecker_Common.deferred = + (g2.FStar_TypeChecker_Common.deferred); + FStar_TypeChecker_Common.univ_ineqs = ([], []); FStar_TypeChecker_Common.implicits = - (FStar_Compiler_List.op_At - g.FStar_TypeChecker_Common.implicits imps) - } - | uu___4 -> - failwith - "Impossible: should have raised a failure already" in - solve_universe_inequalities env - g1.FStar_TypeChecker_Common.univ_ineqs; - (let g2 = - if deferred_to_tac_ok - then - let uu___4 = - let uu___5 = - let uu___6 = - FStar_TypeChecker_Env.current_module env in - FStar_Ident.string_of_lid uu___6 in - FStar_Pervasives_Native.Some uu___5 in - FStar_Profiling.profile - (fun uu___5 -> - FStar_TypeChecker_DeferredImplicits.solve_deferred_to_tactic_goals - env g1) uu___4 - "FStar.TypeChecker.Rel.solve_deferred_to_tactic_goals" - else g1 in - (let uu___5 = - FStar_Compiler_Effect.op_Less_Bar - (FStar_TypeChecker_Env.debug env) - (FStar_Options.Other "ResolveImplicitsHook") in - if uu___5 - then - let uu___6 = guard_to_string env g2 in - let uu___7 = - FStar_Compiler_Util.string_of_int - (FStar_Compiler_List.length - g2.FStar_TypeChecker_Common.implicits) in - FStar_Compiler_Util.print2 - "ResolveImplicitsHook: Solved deferred to tactic goals, remaining guard is\n%s (and %s implicits)\n" - uu___6 uu___7 - else ()); - { - FStar_TypeChecker_Common.guard_f = - (g2.FStar_TypeChecker_Common.guard_f); - FStar_TypeChecker_Common.deferred_to_tac = - (g2.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = - (g2.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = ([], []); - FStar_TypeChecker_Common.implicits = - (g2.FStar_TypeChecker_Common.implicits) - }))) uu___ - "FStar.TypeChecker.Rel.try_solve_deferred_constraints" + (g2.FStar_TypeChecker_Common.implicits) + }))) uu___1 + "FStar.TypeChecker.Rel.try_solve_deferred_constraints") let (solve_deferred_constraints : FStar_TypeChecker_Env.env -> FStar_TypeChecker_Common.guard_t -> FStar_TypeChecker_Common.guard_t) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index 81e9ae05ca4..5dd9d9aca09 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -7107,7 +7107,7 @@ let (short_circuit : match uu___ with | [] -> FStar_TypeChecker_Common.Trivial | (fst, uu___1)::[] -> f fst - | uu___1 -> failwith "Unexpexted args to binary operator" in + | uu___1 -> failwith "Unexpected args to binary operator" in let op_and_e e = let uu___ = FStar_Syntax_Util.b2t e in FStar_Compiler_Effect.op_Bar_Greater uu___ diff --git a/src/basic/FStar.Compiler.Util.fsti b/src/basic/FStar.Compiler.Util.fsti index 11754081e71..ff9e04d1e6a 100644 --- a/src/basic/FStar.Compiler.Util.fsti +++ b/src/basic/FStar.Compiler.Util.fsti @@ -170,7 +170,7 @@ val print_any : 'a -> unit val strcat : string -> string -> string val concat_l : string -> list string -> string -val write_file: string -> string -> unit +val write_file: fn:string -> contents:string -> unit val copy_file: string -> string -> unit val delete_file: string -> unit val file_get_contents: string -> string diff --git a/src/class/FStar.Class.Hashable.fst b/src/class/FStar.Class.Hashable.fst new file mode 100644 index 00000000000..a0f2039a3da --- /dev/null +++ b/src/class/FStar.Class.Hashable.fst @@ -0,0 +1,3 @@ +module FStar.Class.Hashable + +(* empty *) diff --git a/src/class/FStar.Class.Hashable.fsti b/src/class/FStar.Class.Hashable.fsti new file mode 100644 index 00000000000..de34f4f7475 --- /dev/null +++ b/src/class/FStar.Class.Hashable.fsti @@ -0,0 +1,12 @@ +module FStar.Class.Hashable + +include FStar.Hash + +class hashable (a:Type) = { + hash : a -> hash_code; +} + +instance hashable_int : hashable int = { hash = of_int; } +instance hashable_string : hashable string = { hash = of_string; } + +instance showable_hash_code : showable hash_code = { show = string_of_hash_code; } diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst index 7d9bf011777..59da092f661 100644 --- a/src/smtencoding/FStar.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst @@ -876,7 +876,7 @@ let __ask_solver (with_fuel_and_diagnostics config []) (BU.format2 "(%s, %s)" config.query_name (string_of_int config.query_index)) (Some (Z3.mk_fresh_scope())) - (used_hint config) + (used_hint config) // hint queries run in a fresh solver in fold_queries configs check_one_config process_result @@ -1006,6 +1006,22 @@ let ask_solver_quake ; tried_recovery = false (* possibly set by caller *) } +(* A very simple command language for recovering, though keep in +mind its execution is stateful in the sense that anything after a +(RestartSolver h) will run in the new solver instance. *) +type recovery_hammer = + | IncreaseRLimit of (*factor : *)int + | RestartAnd of recovery_hammer + +let rec pp_hammer (h : recovery_hammer) : Pprint.document = + let open FStar.Errors.Msg in + let open FStar.Pprint in + match h with + | IncreaseRLimit factor -> + text "increasing its rlimit by" ^/^ pp factor ^^ doc_of_string "x" + | RestartAnd h -> + text "restarting the solver and" ^/^ pp_hammer h + (* If --proof_recovery is on, then we retry the query multiple times, increasing rlimits, until we get a success. If not, we just call ask_solver_quake. *) @@ -1013,47 +1029,78 @@ let ask_solver_recover (configs : list query_settings) : answer = - let open FStar.Pprint in - let open FStar.Errors.Msg in - let open FStar.Class.PP in - if Options.proof_recovery () then ( - let r = ask_solver_quake configs in - if r.ok then r else ( - let last_cfg = List.last configs in - Errors.diag_doc last_cfg.query_range [ - text "This query failed to be solved. Will now retry with higher rlimits due to --proof_recovery."; - ]; - - let try_factor (n:int) : answer = - let open FStar.Mul in - Errors.diag_doc last_cfg.query_range [ - text "Retrying query with rlimit factor" ^/^ pp n; - ]; - let cfg = { last_cfg with query_rlimit = n * last_cfg.query_rlimit } in - ask_solver_quake [cfg] - in + let open FStar.Pprint in + let open FStar.Errors.Msg in + let open FStar.Class.PP in + if Options.proof_recovery () then ( + let r = ask_solver_quake configs in + if r.ok then r else ( + let restarted = BU.mk_ref false in + let cfg = List.last configs in + + Errors.diag_doc cfg.query_range [ + text "This query failed to be solved. Will now retry with higher rlimits due to --proof_recovery."; + ]; + + let try_factor (n:int) : answer = + let open FStar.Mul in + Errors.diag_doc cfg.query_range [text "Retrying query with rlimit factor" ^/^ pp n]; + let cfg = { cfg with query_rlimit = n * cfg.query_rlimit } in + ask_solver_quake [cfg] + in - let rec aux (factors : list int) : answer = - match factors with - | [] -> - { r with tried_recovery = true } - | n::ns -> - let r = try_factor n in - if r.ok then ( - Errors.log_issue_doc last_cfg.query_range (Errors.Warning_ProofRecovery, [ - text "This query succeeded after increasing its rlimit by" ^/^ - pp n ^^ doc_of_string "x"; - text "Increase the rlimit in the file or simplify the proof. \ - This is only succeeding due to --proof_recovery being given." - ]); - r - ) else - aux ns - in - aux [2;4;8] - ) - ) else - ask_solver_quake configs + let rec try_hammer (h : recovery_hammer) : answer = + match h with + | IncreaseRLimit factor -> try_factor factor + | RestartAnd h -> + Errors.diag_doc cfg.query_range [text "Trying a solver restart"]; + cfg.query_env.solver.refresh(); + try_hammer h + in + + let rec aux (hammers : list recovery_hammer) : answer = + match hammers with + | [] -> { r with tried_recovery = true } + | h::hs -> + let r = try_hammer h in + if r.ok then ( + Errors.log_issue_doc cfg.query_range (Errors.Warning_ProofRecovery, [ + text "This query succeeded after " ^/^ pp_hammer h; + text "Increase the rlimit in the file or simplify the proof. \ + This is only succeeding due to --proof_recovery being given." + ]); + r + ) else + aux hs + in + aux [ + IncreaseRLimit 2; + IncreaseRLimit 4; + IncreaseRLimit 8; + RestartAnd (IncreaseRLimit 8); + ] + ) + ) else + ask_solver_quake configs + +let failing_query_ctr : ref int = BU.mk_ref 0 + +let maybe_save_failing_query (env:env_t) (prefix:list decl) (qs:query_settings) : unit = + if Options.proof_recovery () then ( + let mod = show (Env.current_module env) in + let n = (failing_query_ctr := !failing_query_ctr + 1; !failing_query_ctr) in + let file_name = BU.format2 "failedQueries-%s-%s.smt2" mod (show n) in + let query_str = Z3.ask_text + qs.query_range + (filter_assertions qs.query_env None qs.query_hint) + qs.query_hash + qs.query_all_labels + (with_fuel_and_diagnostics qs []) + (BU.format2 "(%s, %s)" qs.query_name (string_of_int qs.query_index)) + in + write_file file_name query_str; + () + ) let ask_solver (can_split : bool) @@ -1094,7 +1141,11 @@ let ask_solver // once for every VC. Every actual query will push and pop // whatever else they encode. Z3.giveZ3 prefix; - ask_solver_recover configs + let ans = ask_solver_recover configs in + if not ans.ok then + maybe_save_failing_query env prefix (List.last configs); + ans + ) in configs, ans diff --git a/src/smtencoding/FStar.SMTEncoding.Term.fst b/src/smtencoding/FStar.SMTEncoding.Term.fst index 99abf1ee3bd..8bbdb7363e2 100644 --- a/src/smtencoding/FStar.SMTEncoding.Term.fst +++ b/src/smtencoding/FStar.SMTEncoding.Term.fst @@ -14,15 +14,15 @@ limitations under the License. *) module FStar.SMTEncoding.Term -open FStar.Compiler.Effect -open FStar.Compiler.List + open FStar open FStar.Compiler -open FStar.Syntax.Syntax -open FStar.Syntax -open FStar.Compiler.Util -module BU = FStar.Compiler.Util -module U = FStar.Syntax.Util +open FStar.Compiler.Effect +open FStar.Compiler.List + +module S = FStar.Syntax.Syntax +module BU = FStar.Compiler.Util +module U = FStar.Syntax.Util let escape (s:string) = BU.replace_char s '\'' '_' @@ -129,6 +129,7 @@ let mk_decls_trivial decls = [{ let decls_list_of l = l |> List.collect (fun elt -> elt.decls) let mk_fv (x, y) : fv = x, y, false + let fv_name (x:fv) = let nm, _, _ = x in nm let fv_sort (x:fv) = let _, sort, _ = x in sort let fv_force (x:fv) = let _, _, force = x in force diff --git a/src/smtencoding/FStar.SMTEncoding.Term.fsti b/src/smtencoding/FStar.SMTEncoding.Term.fsti index 63fde99772b..2dfa902e7dd 100644 --- a/src/smtencoding/FStar.SMTEncoding.Term.fsti +++ b/src/smtencoding/FStar.SMTEncoding.Term.fsti @@ -15,14 +15,13 @@ *) module FStar.SMTEncoding.Term -open FStar.Compiler.Effect -open Prims -open FStar + open FStar.Compiler -open FStar.Syntax.Syntax -open FStar.Syntax +open FStar.Compiler.Effect open FStar.Compiler.Util +module S = FStar.Syntax.Syntax + type sort = | Bool_sort | Int_sort @@ -87,7 +86,7 @@ type term' = | Labeled of term * string * Range.range | LblPos of term * string and pat = term -and term = {tm:term'; freevars:Syntax.memo fvs; rng:Range.range} +and term = {tm:term'; freevars:S.memo fvs; rng:Range.range} and fv = string * sort * bool (* bool iff variable must be forced/unthunked *) and fvs = list fv diff --git a/src/smtencoding/FStar.SMTEncoding.Z3.fst b/src/smtencoding/FStar.SMTEncoding.Z3.fst index e714057cea2..b83365ca61f 100644 --- a/src/smtencoding/FStar.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStar.SMTEncoding.Z3.fst @@ -217,14 +217,17 @@ let check_z3version (p:proc) : unit = let ver_found : string = BU.trim_string (List.hd (BU.split (getinfo "version") "-")) in let ver_conf : string = BU.trim_string (Options.z3_version ()) in if ver_conf <> ver_found && not (!_already_warned_version_mismatch) then ( - Errors.log_issue Range.dummyRange (Errors.Warning_SolverMismatch, - BU.format5 "Unexpected Z3 version for `%s': expected `%s', got `%s'.\n\ - Please download the correct version of Z3 from %s\n\ - and install it into your $PATH as `%s'." - (proc_prog p) - ver_conf ver_found - z3url (Platform.exe ("z3-" ^ Options.z3_version ())) - ); + let open FStar.Errors in + let open FStar.Pprint in + Errors.log_issue_doc Range.dummyRange (Errors.Warning_SolverMismatch, [ + text (BU.format3 "Unexpected Z3 version for '%s': expected '%s', got '%s'." + (proc_prog p) ver_conf ver_found); + prefix 4 1 (text "Please download the correct version of Z3 from") + (url z3url) ^/^ + group (text "and install it into your $PATH as" ^/^ squotes + (doc_of_string (Platform.exe ("z3-" ^ Options.z3_version ()))) ^^ dot); + ]); + Errors.stop_if_err(); (* stop now if this was a hard error *) _already_warned_version_mismatch := true ); () @@ -594,9 +597,12 @@ let context_profile (theory:list decl) = (string_of_int n)) modules -let mk_input fresh theory = +let mk_input (fresh : bool) (theory : list decl) : string & option string & option string = let ver = Options.z3_version () in - let options = z3_options ver in + let options = "; Z3 invocation started by F*\n" in + let options = options ^ "; F* version: " ^ !Options._version ^ " -- hash: " ^ !Options._commit ^ "\n" in + let options = options ^ "; Z3 version (according to F*): " ^ Options.z3_version() ^ "\n" in + let options = options ^ z3_options ver in let options = options ^ (Options.z3_smtopt() |> String.concat "\n") in if Options.print_z3_statistics() then context_profile theory; let r, hash = @@ -688,6 +694,22 @@ let z3_job (log_file:_) (r:Range.range) fresh (label_messages:error_labels) inpu z3result_query_hash = qhash; z3result_log_file = log_file } +let ask_text + (r:Range.range) + (filter_theory:list decl -> list decl * bool) + (cache:option string) + (label_messages:error_labels) + (qry:list decl) + (queryid:string) + : string + = (* Mimics a fresh ask, and just returns the string that would + be sent to the solver. *) + let theory = flatten_fresh_scope() in + let theory = theory @[Push]@qry@[Pop] in + let theory, _used_unsat_core = filter_theory theory in + let input, qhash, log_file_name = mk_input true theory in + input + let ask (r:Range.range) (filter_theory:list decl -> list decl * bool) diff --git a/src/smtencoding/FStar.SMTEncoding.Z3.fsti b/src/smtencoding/FStar.SMTEncoding.Z3.fsti index 2435f44e0cd..29744f46455 100644 --- a/src/smtencoding/FStar.SMTEncoding.Z3.fsti +++ b/src/smtencoding/FStar.SMTEncoding.Z3.fsti @@ -51,6 +51,15 @@ type query_log = { val status_string_and_errors : z3status -> string * error_labels val giveZ3 : list decl -> unit +val ask_text + : r:Range.range + -> filter:(list decl -> list decl * bool) + -> cache:(option string) // hash + -> label_messages:error_labels + -> qry:list decl + -> queryid:string + -> string + val ask: r:Range.range -> filter:(list decl -> list decl * bool) -> cache:(option string) // hash diff --git a/src/tactics/FStar.Tactics.V2.Interpreter.fst b/src/tactics/FStar.Tactics.V2.Interpreter.fst index 4a29910cf06..303bd7bcd91 100644 --- a/src/tactics/FStar.Tactics.V2.Interpreter.fst +++ b/src/tactics/FStar.Tactics.V2.Interpreter.fst @@ -808,6 +808,9 @@ let run_tactic_on_ps' match res with | Success (ret, ps) -> + if !tacdbg then + do_dump_proofstate ps "at the finish line"; + (* if !tacdbg || Options.tactics_info () then *) (* BU.print1 "Tactic generated proofterm %s\n" (show w); *) let remaining_smt_goals = ps.goals@ps.smt_goals in @@ -825,27 +828,25 @@ let run_tactic_on_ps' remaining_smt_goals; // Check that all implicits were instantiated - if !tacdbg then - BU.print1 "About to check tactic implicits: %s\n" (FStar.Common.string_of_list - (fun imp -> show imp.imp_uvar) - ps.all_implicits); - - let g = {Env.trivial_guard with TcComm.implicits=ps.all_implicits} in - let g = TcRel.solve_deferred_constraints env g in - if !tacdbg then - BU.print2 "Checked %s implicits (1): %s\n" - (show (List.length ps.all_implicits)) - (show ps.all_implicits); - let tagged_implicits = TcRel.resolve_implicits_tac env g in - if !tacdbg then - BU.print2 "Checked %s implicits (2): %s\n" - (show (List.length ps.all_implicits)) - (show ps.all_implicits); - report_implicits rng_goal tagged_implicits; - // /implicits - - if !tacdbg then - do_dump_proofstate ps "at the finish line"; + Errors.with_ctx "While checking implicits left by a tactic" (fun () -> + if !tacdbg then + BU.print1 "About to check tactic implicits: %s\n" (FStar.Common.string_of_list + (fun imp -> show imp.imp_uvar) + ps.all_implicits); + + let g = {Env.trivial_guard with TcComm.implicits=ps.all_implicits} in + let g = TcRel.solve_deferred_constraints env g in + if !tacdbg then + BU.print2 "Checked %s implicits (1): %s\n" + (show (List.length ps.all_implicits)) + (show ps.all_implicits); + let tagged_implicits = TcRel.resolve_implicits_tac env g in + if !tacdbg then + BU.print2 "Checked %s implicits (2): %s\n" + (show (List.length ps.all_implicits)) + (show ps.all_implicits); + report_implicits rng_goal tagged_implicits + ); (remaining_smt_goals, ret) diff --git a/src/typechecker/FStar.TypeChecker.Common.fst b/src/typechecker/FStar.TypeChecker.Common.fst index 693ccbd40c8..749b66e2a30 100644 --- a/src/typechecker/FStar.TypeChecker.Common.fst +++ b/src/typechecker/FStar.TypeChecker.Common.fst @@ -57,6 +57,25 @@ let rec decr_delta_depth = function | Delta_equational_at_level i -> Some (Delta_equational_at_level (i - 1)) | Delta_abstract d -> decr_delta_depth d +instance showable_guard_formula : showable guard_formula = { + show = (function + | Trivial -> "Trivial" + | NonTrivial f -> "NonTrivial " ^ show f) +} + +instance showable_deferred_reason : showable deferred_reason = { + show = (function + | Deferred_univ_constraint -> "Deferred_univ_constraint" + | Deferred_occur_check_failed -> "Deferred_occur_check_failed" + | Deferred_first_order_heuristic_failed -> "Deferred_first_order_heuristic_failed" + | Deferred_flex -> "Deferred_flex" + | Deferred_free_names_check_failed -> "Deferred_free_names_check_failed" + | Deferred_not_a_pattern -> "Deferred_not_a_pattern" + | Deferred_flex_flex_nonpattern -> "Deferred_flex_flex_nonpattern" + | Deferred_delay_match_heuristic -> "Deferred_delay_match_heuristic" + | Deferred_to_user_tac -> "Deferred_to_user_tac" + ); +} (***********************************************************************************) (* A table of file -> starting row -> starting col -> identifier info *) (* Used to support querying information about an identifier in interactive mode *) diff --git a/src/typechecker/FStar.TypeChecker.Common.fsti b/src/typechecker/FStar.TypeChecker.Common.fsti index 2bbf86535ad..b95180e7aa1 100644 --- a/src/typechecker/FStar.TypeChecker.Common.fsti +++ b/src/typechecker/FStar.TypeChecker.Common.fsti @@ -73,6 +73,8 @@ type guard_formula = | Trivial | NonTrivial of formula +instance val showable_guard_formula : showable guard_formula + type deferred_reason = | Deferred_univ_constraint | Deferred_occur_check_failed @@ -84,6 +86,8 @@ type deferred_reason = | Deferred_delay_match_heuristic | Deferred_to_user_tac +instance val showable_deferred_reason : showable deferred_reason + type deferred = list (deferred_reason * string * prob) type univ_ineq = universe * universe diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 2ae0bad305e..11ee66171b9 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -4943,6 +4943,7 @@ let solve_universe_inequalities env ineqs : unit = let try_solve_deferred_constraints (defer_ok:defer_ok_t) smt_ok deferred_to_tac_ok env (g:guard_t) : guard_t = let smt_ok = smt_ok && not (Options.ml_ish ()) in + Errors.with_ctx "While solving deferred constraints" (fun () -> Profiling.profile (fun () -> let typeclass_variables = g.implicits @@ -5003,7 +5004,7 @@ let try_solve_deferred_constraints (defer_ok:defer_ok_t) smt_ok deferred_to_tac_ {g with univ_ineqs=([], [])} ) (Some (Ident.string_of_lid (Env.current_module env))) - "FStar.TypeChecker.Rel.try_solve_deferred_constraints" + "FStar.TypeChecker.Rel.try_solve_deferred_constraints") let solve_deferred_constraints env (g:guard_t) = diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index d5de3ef7476..c4374cf388f 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -3080,7 +3080,7 @@ let short_circuit (head:term) (seen_args:args) : guard_formula = let short_bin_op f : args -> guard_formula = function | [] -> (* no args seen yet *) Trivial | [(fst, _)] -> f fst - | _ -> failwith "Unexpexted args to binary operator" in + | _ -> failwith "Unexpected args to binary operator" in let op_and_e e = U.b2t e |> NonTrivial in let op_or_e e = U.mk_neg (U.b2t e) |> NonTrivial in diff --git a/tests/vale/X64.Vale.Decls.fst b/tests/vale/X64.Vale.Decls.fst index b4e93ffcb4e..6fa0bc2b476 100644 --- a/tests/vale/X64.Vale.Decls.fst +++ b/tests/vale/X64.Vale.Decls.fst @@ -96,7 +96,7 @@ let va_code_Mov64 dst src = irreducible val va_irreducible_lemma_Mov64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Mov64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -119,7 +119,7 @@ let va_code_Load64 dst src offset = irreducible val va_irreducible_lemma_Load64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_reg_operand -> offset:int - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Load64 dst src offset) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_reg_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (valid_src_addr (va_get_mem va_s0) ((va_eval_reg_operand_uint64 va_s0 src) @@ -143,7 +143,7 @@ let va_code_Store64 dst src offset = irreducible val va_irreducible_lemma_Store64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_reg_operand -> src:va_operand -> offset:int - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Store64 dst src offset) va_s0 va_sN) /\ (va_is_src_reg_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (valid_dst_addr (va_get_mem va_s0) ((va_eval_reg_operand_uint64 va_s0 dst) + @@ -169,7 +169,7 @@ let va_code_Add64 dst src = irreducible val va_irreducible_lemma_Add64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Add64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (va_eval_operand_uint64 va_s0 src) + (va_eval_dst_operand_uint64 va_s0 dst) < @@ -193,7 +193,7 @@ let va_code_Add64Wrap dst src = irreducible val va_irreducible_lemma_Add64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Add64Wrap dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -219,7 +219,7 @@ let va_code_AddLea64 dst src1 src2 = irreducible val va_irreducible_lemma_AddLea64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src1:va_operand -> src2:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_AddLea64 dst src1 src2) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src1 va_s0) /\ (va_is_src_operand_uint64 src2 va_s0) /\ (va_get_ok va_s0) /\ (va_eval_operand_uint64 va_s0 @@ -243,7 +243,7 @@ let va_code_Adc64Wrap dst src = irreducible val va_irreducible_lemma_Adc64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Adc64Wrap dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -269,7 +269,7 @@ let va_code_Sub64 dst src = irreducible val va_irreducible_lemma_Sub64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Sub64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ 0 <= (va_eval_dst_operand_uint64 va_s0 dst) - (va_eval_operand_uint64 va_s0 src))) @@ -292,7 +292,7 @@ let va_code_Sub64Wrap dst src = irreducible val va_irreducible_lemma_Sub64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Sub64Wrap dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -315,7 +315,7 @@ let va_code_Mul64Wrap src = irreducible val va_irreducible_lemma_Mul64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Mul64Wrap src) va_s0 va_sN) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) (ensures (fun ((va_bM:va_codes), (va_sM:va_state)) -> ((va_ensure va_b0 va_bM va_s0 va_sM va_sN) @@ -338,7 +338,7 @@ let va_code_IMul64 dst src = irreducible val va_irreducible_lemma_IMul64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_IMul64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (va_eval_dst_operand_uint64 va_s0 dst) `op_Multiply` (va_eval_operand_uint64 va_s0 @@ -364,7 +364,7 @@ let va_code_Xor64 dst src = irreducible val va_irreducible_lemma_Xor64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Xor64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -387,7 +387,7 @@ let va_code_And64 dst src = irreducible val va_irreducible_lemma_And64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_And64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -410,7 +410,7 @@ let va_code_Shl64 dst amt = irreducible val va_irreducible_lemma_Shl64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> amt:va_shift_amt - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Shl64 dst amt) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_shift_amt_uint64 amt va_s0) /\ (va_get_ok va_s0))) @@ -433,7 +433,7 @@ let va_code_Shr64 dst amt = irreducible val va_irreducible_lemma_Shr64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> amt:va_shift_amt - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Shr64 dst amt) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_shift_amt_uint64 amt va_s0) /\ (va_get_ok va_s0))) diff --git a/tests/vale/X64.Vale.Decls.fsti b/tests/vale/X64.Vale.Decls.fsti index a07c95e0f45..bb47cdecf47 100644 --- a/tests/vale/X64.Vale.Decls.fsti +++ b/tests/vale/X64.Vale.Decls.fsti @@ -288,7 +288,7 @@ val va_code_Mov64 : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_Mov64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Mov64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -300,7 +300,7 @@ val va_code_Load64 : dst:va_dst_operand -> src:va_reg_operand -> offset:int -> T val va_lemma_Load64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_reg_operand -> offset:int - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Load64 dst src offset) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_reg_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (valid_src_addr (va_get_mem va_s0) ((va_eval_reg_operand_uint64 va_s0 src) @@ -314,7 +314,7 @@ val va_code_Store64 : dst:va_reg_operand -> src:va_operand -> offset:int -> Tot val va_lemma_Store64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_reg_operand -> src:va_operand -> offset:int - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Store64 dst src offset) va_s0 va_sN) /\ (va_is_src_reg_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (valid_dst_addr (va_get_mem va_s0) ((va_eval_reg_operand_uint64 va_s0 dst) + @@ -328,7 +328,7 @@ val va_code_Add64 : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_Add64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Add64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (va_eval_operand_uint64 va_s0 src) + (va_eval_dst_operand_uint64 va_s0 dst) < @@ -342,7 +342,7 @@ val va_code_Add64Wrap : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_Add64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Add64Wrap dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -357,7 +357,7 @@ val va_code_AddLea64 : dst:va_dst_operand -> src1:va_operand -> src2:va_operand val va_lemma_AddLea64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src1:va_operand -> src2:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_AddLea64 dst src1 src2) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src1 va_s0) /\ (va_is_src_operand_uint64 src2 va_s0) /\ (va_get_ok va_s0) /\ (va_eval_operand_uint64 va_s0 @@ -371,7 +371,7 @@ val va_code_Adc64Wrap : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_Adc64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Adc64Wrap dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -387,7 +387,7 @@ val va_code_Sub64 : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_Sub64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Sub64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ 0 <= (va_eval_dst_operand_uint64 va_s0 dst) - (va_eval_operand_uint64 va_s0 src))) @@ -400,7 +400,7 @@ val va_code_Sub64Wrap : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_Sub64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Sub64Wrap dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -412,7 +412,7 @@ val va_lemma_Sub64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> d val va_code_Mul64Wrap : src:va_operand -> Tot va_code val va_lemma_Mul64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Mul64Wrap src) va_s0 va_sN) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) (ensures (fun ((va_bM:va_codes), (va_sM:va_state)) -> ((va_ensure va_b0 va_bM va_s0 va_sM va_sN) @@ -425,7 +425,7 @@ val va_code_IMul64 : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_IMul64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_IMul64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0) /\ (va_eval_dst_operand_uint64 va_s0 dst) `op_Multiply` (va_eval_operand_uint64 va_s0 @@ -440,7 +440,7 @@ val va_code_Xor64 : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_Xor64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Xor64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -453,7 +453,7 @@ val va_code_And64 : dst:va_dst_operand -> src:va_operand -> Tot va_code val va_lemma_And64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_And64 dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) @@ -466,7 +466,7 @@ val va_code_Shl64 : dst:va_dst_operand -> amt:va_shift_amt -> Tot va_code val va_lemma_Shl64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> amt:va_shift_amt - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Shl64 dst amt) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_shift_amt_uint64 amt va_s0) /\ (va_get_ok va_s0))) @@ -479,7 +479,7 @@ val va_code_Shr64 : dst:va_dst_operand -> amt:va_shift_amt -> Tot va_code val va_lemma_Shr64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> amt:va_shift_amt - -> Ghost ((va_bM:va_codes) * (va_sM:va_state)) + -> Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Shr64 dst amt) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_shift_amt_uint64 amt va_s0) /\ (va_get_ok va_s0)))