From 68409ef6fdebb2a1735f33c871ee13cc51a9e20a Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 24 Sep 2025 15:04:18 +0200 Subject: [PATCH] chore: turn some crashes into errors (#8402) This PR prevents some nonsensical code from crashing the server. Specifically, the kernel is changed to - properly check that passed expressions do not contain loose bvars, which could lead to a segmentation fault on a well-crafted input (discovered through fuzzing), and - check that constants generated when creating a new inductive type do not overwrite each other, which could lead to the kernel taking something out of the environment and then casting it to something it isn't. Partially addresses #8258, but let's keep that one open until the error message is a little better. Fixes #10492. --- src/kernel/inductive.cpp | 5 + src/kernel/type_checker.cpp | 3 +- tests/lean/run/bvarcrash.lean | 645 ++++++++++++++++++++++++ tests/lean/run/recconstructorcrash.lean | 4 + 4 files changed, 655 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/bvarcrash.lean create mode 100644 tests/lean/run/recconstructorcrash.lean diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index 5b17564675..def786cd93 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -325,6 +325,7 @@ public: for (constructor const & cnstr : ind_type.get_cnstrs()) { cnstr_names.push_back(constructor_name(cnstr)); } + m_env.check_name(n); m_env.add_core(constant_info(inductive_val(n, m_lparams, ind_type.get_type(), m_nparams, m_nindices[idx], all, names(cnstr_names), m_nnested, rec, m_is_unsafe, reflexive))); } @@ -467,6 +468,7 @@ public: } lean_assert(arity >= m_nparams); unsigned nfields = arity - m_nparams; + m_env.check_name(n); m_env.add_core(constant_info(constructor_val(n, m_lparams, t, ind_type.get_name(), cidx, m_nparams, nfields, m_is_unsafe))); cidx++; } @@ -766,6 +768,7 @@ public: recursor_rules rules = mk_rec_rules(d_idx, Cs, minors, minor_idx); name rec_name = mk_rec_name(m_ind_types[d_idx].get_name()); names rec_lparams = get_rec_lparams(); + m_env.check_name(rec_name); m_env.add_core(constant_info(recursor_val(rec_name, rec_lparams, rec_ty, all, m_nparams, m_nindices[d_idx], nmotives, nminors, rules, m_K_target, m_is_unsafe))); @@ -1155,6 +1158,7 @@ environment environment::add_inductive(declaration const & d) const { /* We just need to "fix" the `all` fields for ind_info. Remark: if we decide to store the recursor names, we will also need to fix it. */ + new_env.check_name(ind_info.get_name()); new_env.add_core(constant_info(inductive_val(ind_info.get_name(), ind_info.get_lparams(), ind_info.get_type(), ind_val.get_nparams(), ind_val.get_nindices(), all_ind_names, ind_val.get_cnstrs(), ind_val.get_nnested(), @@ -1163,6 +1167,7 @@ environment environment::add_inductive(declaration const & d) const { constant_info cnstr_info = aux_env.get(cnstr_name); constructor_val cnstr_val = cnstr_info.to_constructor_val(); expr new_type = res.restore_nested(cnstr_info.get_type(), aux_env); + new_env.check_name(cnstr_info.get_name()); new_env.add_core(constant_info(constructor_val(cnstr_info.get_name(), cnstr_info.get_lparams(), new_type, cnstr_val.get_induct(), cnstr_val.get_cidx(), cnstr_val.get_nparams(), cnstr_val.get_nfields(), cnstr_val.is_unsafe()))); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 98d7022094..20b2c77db6 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -268,10 +268,9 @@ expr type_checker::infer_proj(expr const & e, bool infer_only) { /** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not. \pre closed(e) */ expr type_checker::infer_type_core(expr const & e, bool infer_only) { - if (is_bvar(e)) + if (has_loose_bvars(e)) throw kernel_exception(env(), "type checker does not support loose bound variables, replace them with free variables before invoking it"); - lean_assert(!has_loose_bvars(e)); check_system("type checker", /* do_check_interrupted */ true); auto it = m_st->m_infer_type[infer_only].find(e); diff --git a/tests/lean/run/bvarcrash.lean b/tests/lean/run/bvarcrash.lean new file mode 100644 index 0000000000..5df064ba54 --- /dev/null +++ b/tests/lean/run/bvarcrash.lean @@ -0,0 +1,645 @@ +import Lean +def decodeNatLit (l : List Nat) : Nat := l.foldl (init := 0) (fun sofar d => 256 * sofar + d) +def name_0 : Lean.Name := .anonymous +def level_0 : Lean.Level := .zero +def name_1 : Lean.Name := .str name_0 "term_+_" +def level_1 : Lean.Level := .param name_1 +def level_2 : Lean.Level := .succ level_1 +def expr_0 : Lean.Expr := .sort level_2 +def expr_1 : Lean.Expr := .bvar 0 +def name_2 : Lean.Name := .str name_0 "_sizeOf_1" +def expr_2 : Lean.Expr := .const name_2 [level_1] +def expr_3 : Lean.Expr := .bvar 1 +def expr_4 : Lean.Expr := .app expr_2 expr_3 +def name_3 : Lean.Name := .str name_0 "term_+_" +def name_4 : Lean.Name := .str name_0 "term_+_" +def name_5 : Lean.Name := .str name_1 "term_+_" +def name_6 : Lean.Name := .str name_0 "term_+_" +def name_7 : Lean.Name := .str name_2 "term_+_" +def name_8 : Lean.Name := .str name_0 "term_+_" +def expr_5 : Lean.Expr := .forallE name_6 expr_1 expr_4 .default +def name_9 : Lean.Name := .str name_6 "term_+_" +def expr_6 : Lean.Expr := .forallE name_6 expr_0 expr_5 .default +def name_10 : Lean.Name := .str name_6 "term_+_" +def constructor_0 : Lean.Constructor where + name := name_10 + type := expr_6 +def name_11 : Lean.Name := .str name_5 "term_+_" +def expr_7 : Lean.Expr := .forallE name_0 expr_5 expr_4 .default +def expr_8 : Lean.Expr := .forallE name_0 expr_0 expr_7 .default +def name_12 : Lean.Name := .str name_0 "ε'" +def constructor_1 : Lean.Constructor where + name := name_12 + type := expr_8 +def expr_9 : Lean.Expr := .forallE name_12 expr_0 expr_0 .default +def inductive_0 : Lean.InductiveType where + name := name_2 + type := expr_9 + ctors := [constructor_0, constructor_1] +def decl_0 : Lean.Declaration := + .inductDecl [name_4] 1 [inductive_0] false +def name_13 : Lean.Name := .str name_2 "rec" +def expr_10 : Lean.Expr := .app expr_2 expr_1 +def name_14 : Lean.Name := .str name_2 "term_+_" +def level_3 : Lean.Level := .param name_14 +def expr_11 : Lean.Expr := .sort level_3 +def name_15 : Lean.Name := .str name_6 "term_+_" +def expr_12 : Lean.Expr := .forallE name_0 expr_10 expr_11 .default +def expr_13 : Lean.Expr := .bvar 2 +def expr_14 : Lean.Expr := .const name_10 [level_1] +def expr_15 : Lean.Expr := .bvar 3 +def expr_16 : Lean.Expr := .app expr_14 expr_15 +def expr_17 : Lean.Expr := .app expr_16 expr_1 +def expr_18 : Lean.Expr := .app expr_13 expr_17 +def expr_19 : Lean.Expr := .forallE name_0 expr_13 expr_18 .default +def expr_20 : Lean.Expr := .bvar 4 +def expr_21 : Lean.Expr := .app expr_2 expr_20 +def name_16 : Lean.Name := .str name_0 "term_+_" +def expr_22 : Lean.Expr := .forallE name_11 expr_15 expr_21 .default +def expr_23 : Lean.Expr := .const name_12 [level_1] +def expr_24 : Lean.Expr := .app expr_23 expr_20 +def expr_25 : Lean.Expr := .app expr_24 expr_1 +def expr_26 : Lean.Expr := .app expr_15 expr_25 +def expr_27 : Lean.Expr := .forallE name_11 expr_22 expr_26 .default +def expr_28 : Lean.Expr := .app expr_15 expr_13 +def name_17 : Lean.Name := .str name_11 "term_+_" +def expr_29 : Lean.Expr := .forallE name_6 expr_27 expr_28 .default +def name_18 : Lean.Name := .str name_6 "term_+_" +def expr_30 : Lean.Expr := .forallE name_5 expr_19 expr_29 .default +def expr_31 : Lean.Expr := .forallE name_5 expr_4 expr_30 .default +def name_19 : Lean.Name := .str name_5 "term_+_" +def expr_32 : Lean.Expr := .forallE name_16 expr_12 expr_31 .default +def expr_33 : Lean.Expr := .forallE name_16 expr_0 expr_32 .default +def expr_34 : Lean.Expr := .const name_13 [level_3, level_1] +def expr_35 : Lean.Expr := .app expr_34 expr_20 +def expr_36 : Lean.Expr := .app expr_35 expr_15 +def expr_37 : Lean.Expr := .app expr_13 expr_1 +def expr_38 : Lean.Expr := .lam name_16 expr_20 expr_37 .default +def expr_39 : Lean.Expr := .app expr_36 expr_38 +def expr_40 : Lean.Expr := .bvar 5 +def expr_41 : Lean.Expr := .app expr_2 expr_40 +def expr_42 : Lean.Expr := .forallE name_16 expr_20 expr_41 .default +def expr_43 : Lean.Expr := .app expr_3 expr_1 +def expr_44 : Lean.Expr := .app expr_40 expr_43 +def expr_45 : Lean.Expr := .forallE name_16 expr_40 expr_44 .default +def expr_46 : Lean.Expr := .app expr_13 expr_3 +def name_20 : Lean.Name := .str name_16 "term_+_" +def name_21 : Lean.Name := .str name_9 "term_+_" +def name_22 : Lean.Name := .str name_16 "term_+_" +def name_23 : Lean.Name := .str name_8 "term_+_" +def name_24 : Lean.Name := .str name_0 "term_+_" +def name_25 : Lean.Name := .str name_11 "term_+_" +def expr_47 : Lean.Expr := .lam name_12 expr_45 expr_46 .default +def expr_48 : Lean.Expr := .lam name_12 expr_42 expr_47 .default +def expr_49 : Lean.Expr := .app expr_39 expr_48 +def expr_50 : Lean.Expr := .app expr_49 expr_13 +def expr_51 : Lean.Expr := .lam name_12 expr_27 expr_50 .default +def expr_52 : Lean.Expr := .lam name_12 expr_19 expr_51 .default +def expr_53 : Lean.Expr := .lam name_12 expr_4 expr_52 .default +def expr_54 : Lean.Expr := .lam name_12 expr_12 expr_53 .default +def expr_55 : Lean.Expr := .lam name_12 expr_0 expr_54 .default +def name_26 : Lean.Name := .str name_12 "term_+_" +def decl_1 : Lean.Declaration := + .defnDecl { + name := name_26 + levelParams := [name_14, name_24] + type := expr_33 + value := expr_55 + hints := .opaque + safety := .safe + all := [name_26] + } +def expr_56 : Lean.Expr := .app expr_2 expr_13 +def name_27 : Lean.Name := .str name_24 "term_+_" +def expr_57 : Lean.Expr := .forallE name_16 expr_56 expr_11 .default +def name_28 : Lean.Name := .str name_16 "term_+_" +def expr_58 : Lean.Expr := .forallE name_11 expr_4 expr_57 .default +def name_29 : Lean.Name := .str name_11 "term_+_" +def expr_59 : Lean.Expr := .forallE name_6 expr_11 expr_58 .default +def expr_60 : Lean.Expr := .forallE name_6 expr_0 expr_59 .default +def level_4 : Lean.Level := .succ level_3 +def expr_61 : Lean.Expr := .const name_26 [level_4, level_1] +def expr_62 : Lean.Expr := .app expr_61 expr_15 +def expr_63 : Lean.Expr := .app expr_2 expr_15 +def expr_64 : Lean.Expr := .lam name_6 expr_63 expr_11 .default +def expr_65 : Lean.Expr := .app expr_62 expr_64 +def expr_66 : Lean.Expr := .app expr_65 expr_3 +def expr_67 : Lean.Expr := .app expr_61 expr_20 +def expr_68 : Lean.Expr := .lam name_6 expr_21 expr_11 .default +def expr_69 : Lean.Expr := .app expr_67 expr_68 +def expr_70 : Lean.Expr := .app expr_69 expr_3 +def name_30 : Lean.Name := .str name_0 "Eq" +def expr_71 : Lean.Expr := .const name_30 [level_2] +def expr_72 : Lean.Expr := .app expr_71 expr_40 +def expr_73 : Lean.Expr := .app expr_72 expr_3 +def expr_74 : Lean.Expr := .app expr_73 expr_1 +def name_31 : Lean.Name := .str name_29 "term_+_" +def name_32 : Lean.Name := .str name_16 "term_+_" +def name_33 : Lean.Name := .str name_27 "term_+_" +def name_34 : Lean.Name := .str name_28 "term_+_" +def name_35 : Lean.Name := .str name_16 "term_+_" +def name_36 : Lean.Name := .str name_24 "term_+_" +def expr_75 : Lean.Expr := .forallE name_15 expr_74 expr_40 .default +def expr_76 : Lean.Expr := .forallE name_15 expr_75 expr_40 .default +def expr_77 : Lean.Expr := .lam name_15 expr_20 expr_76 .default +def expr_78 : Lean.Expr := .app expr_70 expr_77 +def expr_79 : Lean.Expr := .lam name_15 expr_42 expr_20 .default +def expr_80 : Lean.Expr := .app expr_78 expr_79 +def expr_81 : Lean.Expr := .lam name_15 expr_15 expr_80 .default +def expr_82 : Lean.Expr := .app expr_66 expr_81 +def expr_83 : Lean.Expr := .lam name_15 expr_20 expr_20 .default +def expr_84 : Lean.Expr := .app expr_70 expr_83 +def expr_85 : Lean.Expr := .bvar 6 +def expr_86 : Lean.Expr := .app expr_2 expr_85 +def expr_87 : Lean.Expr := .forallE name_15 expr_40 expr_86 .default +def expr_88 : Lean.Expr := .app expr_71 expr_87 +def expr_89 : Lean.Expr := .app expr_88 expr_3 +def expr_90 : Lean.Expr := .app expr_89 expr_1 +def name_37 : Lean.Name := .str name_15 "term_+_" +def expr_91 : Lean.Expr := .forallE name_24 expr_90 expr_40 .default +def expr_92 : Lean.Expr := .forallE name_24 expr_91 expr_40 .default +def expr_93 : Lean.Expr := .lam name_24 expr_42 expr_92 .default +def expr_94 : Lean.Expr := .app expr_84 expr_93 +def expr_95 : Lean.Expr := .lam name_24 expr_22 expr_94 .default +def expr_96 : Lean.Expr := .app expr_82 expr_95 +def expr_97 : Lean.Expr := .lam name_24 expr_56 expr_96 .default +def expr_98 : Lean.Expr := .lam name_24 expr_4 expr_97 .default +def expr_99 : Lean.Expr := .lam name_24 expr_11 expr_98 .default +def expr_100 : Lean.Expr := .lam name_24 expr_0 expr_99 .default +def name_38 : Lean.Name := .str name_24 "inj" +def decl_2 : Lean.Declaration := + .defnDecl { + name := name_38 + levelParams := [name_14, name_4] + type := expr_60 + value := expr_100 + hints := .opaque + safety := .safe + all := [name_38] + } +def expr_101 : Lean.Expr := .sort level_4 +def expr_102 : Lean.Expr := .const name_2 [level_3] +def expr_103 : Lean.Expr := .app expr_102 expr_1 +def name_39 : Lean.Name := .str name_12 "term_+_" +def level_5 : Lean.Level := .succ level_3 +def expr_104 : Lean.Expr := .sort level_5 +def name_40 : Lean.Name := .str name_16 "term_+_" +def name_41 : Lean.Name := .str name_36 "term_+_" +def name_42 : Lean.Name := .str name_30 "term_+_" +def name_43 : Lean.Name := .str name_38 "term_+_" +def name_44 : Lean.Name := .str name_16 "term_+_" +def name_45 : Lean.Name := .str name_6 "term_+_" +def name_46 : Lean.Name := .str name_8 "term_+_" +def expr_105 : Lean.Expr := .forallE name_22 expr_103 expr_104 .default +def expr_106 : Lean.Expr := .app expr_102 expr_3 +def expr_107 : Lean.Expr := .const name_10 [level_3] +def expr_108 : Lean.Expr := .app expr_107 expr_15 +def expr_109 : Lean.Expr := .app expr_108 expr_1 +def expr_110 : Lean.Expr := .app expr_13 expr_109 +def name_47 : Lean.Name := .str name_22 "term_+_" +def expr_111 : Lean.Expr := .forallE name_0 expr_13 expr_110 .default +def expr_112 : Lean.Expr := .app expr_102 expr_20 +def expr_113 : Lean.Expr := .forallE name_0 expr_15 expr_112 .default +def expr_114 : Lean.Expr := .const name_12 [level_3] +def expr_115 : Lean.Expr := .app expr_114 expr_20 +def expr_116 : Lean.Expr := .app expr_115 expr_1 +def expr_117 : Lean.Expr := .app expr_15 expr_116 +def name_48 : Lean.Name := .str name_0 "term_+_" +def expr_118 : Lean.Expr := .forallE name_37 expr_113 expr_117 .default +def name_49 : Lean.Name := .str name_37 "term_+_" +def expr_119 : Lean.Expr := .forallE name_36 expr_118 expr_28 .default +def name_50 : Lean.Name := .str name_36 "term_+_" +def expr_120 : Lean.Expr := .forallE name_45 expr_111 expr_119 .default +def expr_121 : Lean.Expr := .forallE name_45 expr_106 expr_120 .default +def expr_122 : Lean.Expr := .forallE name_45 expr_105 expr_121 .default +def expr_123 : Lean.Expr := .forallE name_45 expr_101 expr_122 .default +def expr_124 : Lean.Expr := .const name_26 [level_5, level_3] +def expr_125 : Lean.Expr := .app expr_124 expr_20 +def expr_126 : Lean.Expr := .app expr_20 expr_1 +def expr_127 : Lean.Expr := .lam name_45 expr_112 expr_126 .default +def expr_128 : Lean.Expr := .app expr_125 expr_127 +def expr_129 : Lean.Expr := .app expr_128 expr_13 +def expr_130 : Lean.Expr := .app expr_129 expr_38 +def expr_131 : Lean.Expr := .app expr_102 expr_40 +def expr_132 : Lean.Expr := .forallE name_45 expr_20 expr_131 .default +def name_51 : Lean.Name := .str name_45 "term_+_" +def expr_133 : Lean.Expr := .lam name_12 expr_132 expr_43 .default +def expr_134 : Lean.Expr := .app expr_130 expr_133 +def expr_135 : Lean.Expr := .lam name_12 expr_118 expr_134 .default +def expr_136 : Lean.Expr := .lam name_12 expr_111 expr_135 .default +def expr_137 : Lean.Expr := .lam name_12 expr_106 expr_136 .default +def expr_138 : Lean.Expr := .lam name_12 expr_105 expr_137 .default +def expr_139 : Lean.Expr := .lam name_12 expr_101 expr_138 .default +def name_52 : Lean.Name := .str name_12 "term_+_" +def name_53 : Lean.Name := .str name_40 "term_+_" +def decl_3 : Lean.Declaration := + .defnDecl { + name := name_29 + levelParams := [name_14, name_24] + type := expr_123 + value := expr_139 + hints := .opaque + safety := .safe + all := [name_29] + } +def expr_140 : Lean.Expr := .app expr_71 expr_63 +def expr_141 : Lean.Expr := .app expr_140 expr_3 +def expr_142 : Lean.Expr := .app expr_141 expr_1 +def expr_143 : Lean.Expr := .const name_38 [level_3, level_1] +def expr_144 : Lean.Expr := .app expr_143 expr_20 +def expr_145 : Lean.Expr := .app expr_144 expr_15 +def expr_146 : Lean.Expr := .app expr_145 expr_13 +def expr_147 : Lean.Expr := .app expr_146 expr_3 +def name_54 : Lean.Name := .str name_24 "term_+_" +def expr_148 : Lean.Expr := .forallE name_16 expr_142 expr_147 .default +def expr_149 : Lean.Expr := .forallE name_16 expr_56 expr_148 .default +def expr_150 : Lean.Expr := .forallE name_16 expr_4 expr_149 .default +def expr_151 : Lean.Expr := .forallE name_16 expr_11 expr_150 .default +def expr_152 : Lean.Expr := .forallE name_16 expr_0 expr_151 .default +def name_55 : Lean.Name := .str name_30 "ndrec" +def expr_153 : Lean.Expr := .const name_55 [level_3, level_2] +def expr_154 : Lean.Expr := .app expr_153 expr_21 +def expr_155 : Lean.Expr := .app expr_154 expr_13 +def expr_156 : Lean.Expr := .app expr_71 expr_41 +def expr_157 : Lean.Expr := .app expr_156 expr_15 +def expr_158 : Lean.Expr := .app expr_157 expr_1 +def expr_159 : Lean.Expr := .app expr_143 expr_85 +def expr_160 : Lean.Expr := .app expr_159 expr_40 +def expr_161 : Lean.Expr := .app expr_160 expr_20 +def expr_162 : Lean.Expr := .app expr_161 expr_3 +def name_56 : Lean.Name := .str name_16 "term_+_" +def expr_163 : Lean.Expr := .forallE name_24 expr_158 expr_162 .default +def expr_164 : Lean.Expr := .lam name_24 expr_21 expr_163 .default +def expr_165 : Lean.Expr := .app expr_155 expr_164 +def expr_166 : Lean.Expr := .app expr_71 expr_21 +def expr_167 : Lean.Expr := .app expr_166 expr_13 +def expr_168 : Lean.Expr := .app expr_167 expr_13 +def expr_169 : Lean.Expr := .const name_26 [level_3, level_1] +def expr_170 : Lean.Expr := .app expr_169 expr_40 +def expr_171 : Lean.Expr := .app expr_160 expr_1 +def expr_172 : Lean.Expr := .app expr_171 expr_1 +def expr_173 : Lean.Expr := .lam name_24 expr_41 expr_172 .default +def expr_174 : Lean.Expr := .app expr_170 expr_173 +def expr_175 : Lean.Expr := .app expr_174 expr_15 +def expr_176 : Lean.Expr := .app expr_71 expr_85 +def expr_177 : Lean.Expr := .app expr_176 expr_1 +def expr_178 : Lean.Expr := .app expr_177 expr_1 +def expr_179 : Lean.Expr := .forallE name_24 expr_178 expr_85 .default +def name_57 : Lean.Name := .str name_30 "refl" +def expr_180 : Lean.Expr := .const name_57 [level_2] +def expr_181 : Lean.Expr := .bvar 7 +def expr_182 : Lean.Expr := .app expr_180 expr_181 +def expr_183 : Lean.Expr := .app expr_182 expr_3 +def expr_184 : Lean.Expr := .app expr_1 expr_183 +def expr_185 : Lean.Expr := .lam name_40 expr_179 expr_184 .default +def expr_186 : Lean.Expr := .lam name_40 expr_40 expr_185 .default +def expr_187 : Lean.Expr := .app expr_175 expr_186 +def expr_188 : Lean.Expr := .app expr_2 expr_181 +def expr_189 : Lean.Expr := .forallE name_40 expr_85 expr_188 .default +def expr_190 : Lean.Expr := .app expr_71 expr_189 +def expr_191 : Lean.Expr := .app expr_190 expr_1 +def expr_192 : Lean.Expr := .app expr_191 expr_1 +def expr_193 : Lean.Expr := .forallE name_40 expr_192 expr_85 .default +def expr_194 : Lean.Expr := .bvar 8 +def expr_195 : Lean.Expr := .app expr_2 expr_194 +def expr_196 : Lean.Expr := .forallE name_40 expr_181 expr_195 .default +def expr_197 : Lean.Expr := .app expr_180 expr_196 +def expr_198 : Lean.Expr := .app expr_197 expr_3 +def expr_199 : Lean.Expr := .app expr_1 expr_198 +def expr_200 : Lean.Expr := .lam name_40 expr_193 expr_199 .default +def expr_201 : Lean.Expr := .lam name_40 expr_87 expr_200 .default +def expr_202 : Lean.Expr := .app expr_187 expr_201 +def name_58 : Lean.Name := .str name_40 "term_+_" +def expr_203 : Lean.Expr := .lam name_5 expr_168 expr_202 .default +def expr_204 : Lean.Expr := .app expr_165 expr_203 +def expr_205 : Lean.Expr := .app expr_204 expr_3 +def expr_206 : Lean.Expr := .app expr_205 expr_1 +def expr_207 : Lean.Expr := .app expr_206 expr_1 +def expr_208 : Lean.Expr := .lam name_5 expr_142 expr_207 .default +def expr_209 : Lean.Expr := .lam name_5 expr_56 expr_208 .default +def expr_210 : Lean.Expr := .lam name_5 expr_4 expr_209 .default +def expr_211 : Lean.Expr := .lam name_5 expr_11 expr_210 .default +def expr_212 : Lean.Expr := .lam name_5 expr_0 expr_211 .default +def name_59 : Lean.Name := .str name_5 "term_+_" +def decl_4 : Lean.Declaration := + .defnDecl { + name := name_47 + levelParams := [name_14, name_48] + type := expr_152 + value := expr_212 + hints := .opaque + safety := .safe + all := [name_47] + } +def expr_213 : Lean.Expr := .forallE name_36 expr_10 expr_101 .default +def level_6 : Lean.Level := .max level_4 level_2 +def expr_214 : Lean.Expr := .sort level_6 +def expr_215 : Lean.Expr := .forallE name_36 expr_4 expr_214 .default +def expr_216 : Lean.Expr := .forallE name_36 expr_213 expr_215 .default +def expr_217 : Lean.Expr := .forallE name_36 expr_0 expr_216 .default +def level_7 : Lean.Level := .succ level_6 +def expr_218 : Lean.Expr := .const name_13 [level_7, level_1] +def expr_219 : Lean.Expr := .app expr_218 expr_13 +def expr_220 : Lean.Expr := .lam name_36 expr_56 expr_214 .default +def expr_221 : Lean.Expr := .app expr_219 expr_220 +def name_60 : Lean.Name := .str name_0 "PUnit" +def expr_222 : Lean.Expr := .const name_60 [level_6] +def expr_223 : Lean.Expr := .lam name_14 expr_13 expr_222 .default +def expr_224 : Lean.Expr := .app expr_221 expr_223 +def expr_225 : Lean.Expr := .forallE name_14 expr_13 expr_63 .default +def expr_226 : Lean.Expr := .forallE name_14 expr_15 expr_214 .default +def name_61 : Lean.Name := .str name_0 "PProd" +def level_8 : Lean.Level := .max level_2 level_4 +def expr_227 : Lean.Expr := .const name_61 [level_8, level_8] +def expr_228 : Lean.Expr := .app expr_20 expr_37 +def expr_229 : Lean.Expr := .forallE name_60 expr_20 expr_228 .default +def expr_230 : Lean.Expr := .app expr_227 expr_229 +def expr_231 : Lean.Expr := .forallE name_60 expr_20 expr_43 .default +def expr_232 : Lean.Expr := .app expr_230 expr_231 +def expr_233 : Lean.Expr := .lam name_60 expr_226 expr_232 .default +def expr_234 : Lean.Expr := .lam name_60 expr_225 expr_233 .default +def expr_235 : Lean.Expr := .app expr_224 expr_234 +def expr_236 : Lean.Expr := .app expr_235 expr_1 +def expr_237 : Lean.Expr := .lam name_60 expr_4 expr_236 .default +def expr_238 : Lean.Expr := .lam name_60 expr_213 expr_237 .default +def expr_239 : Lean.Expr := .lam name_60 expr_0 expr_238 .default +def name_62 : Lean.Name := .str name_60 "below" +def decl_5 : Lean.Declaration := + .defnDecl { + name := name_62 + levelParams := [name_14, name_4] + type := expr_217 + value := expr_239 + hints := .opaque + safety := .safe + all := [name_62] + } +def expr_240 : Lean.Expr := .sort level_0 +def expr_241 : Lean.Expr := .forallE name_51 expr_10 expr_240 .default +def expr_242 : Lean.Expr := .forallE name_51 expr_4 expr_240 .default +def expr_243 : Lean.Expr := .forallE name_51 expr_241 expr_242 .default +def expr_244 : Lean.Expr := .forallE name_51 expr_0 expr_243 .default +def level_9 : Lean.Level := .succ level_0 +def expr_245 : Lean.Expr := .const name_13 [level_9, level_1] +def expr_246 : Lean.Expr := .app expr_245 expr_13 +def expr_247 : Lean.Expr := .lam name_51 expr_56 expr_240 .default +def expr_248 : Lean.Expr := .app expr_246 expr_247 +def name_63 : Lean.Name := .str name_0 "True" +def expr_249 : Lean.Expr := .const name_63 [] +def expr_250 : Lean.Expr := .lam name_48 expr_13 expr_249 .default +def expr_251 : Lean.Expr := .app expr_248 expr_250 +def expr_252 : Lean.Expr := .forallE name_48 expr_15 expr_240 .default +def name_64 : Lean.Name := .str name_0 "And" +def expr_253 : Lean.Expr := .const name_64 [] +def expr_254 : Lean.Expr := .app expr_253 expr_229 +def expr_255 : Lean.Expr := .app expr_254 expr_231 +def expr_256 : Lean.Expr := .lam name_51 expr_252 expr_255 .default +def expr_257 : Lean.Expr := .lam name_51 expr_225 expr_256 .default +def expr_258 : Lean.Expr := .app expr_251 expr_257 +def expr_259 : Lean.Expr := .app expr_258 expr_1 +def expr_260 : Lean.Expr := .lam name_51 expr_4 expr_259 .default +def expr_261 : Lean.Expr := .lam name_51 expr_241 expr_260 .default +def expr_262 : Lean.Expr := .lam name_51 expr_0 expr_261 .default +def name_65 : Lean.Name := .str name_51 "casesOn" +def decl_6 : Lean.Declaration := + .defnDecl { + name := name_65 + levelParams := [name_48] + type := expr_244 + value := expr_262 + hints := .opaque + safety := .safe + all := [name_65] + } +def expr_263 : Lean.Expr := .const name_65 [level_1] +def expr_264 : Lean.Expr := .app expr_263 expr_15 +def expr_265 : Lean.Expr := .app expr_264 expr_13 +def expr_266 : Lean.Expr := .app expr_265 expr_1 +def expr_267 : Lean.Expr := .app expr_15 expr_3 +def expr_268 : Lean.Expr := .forallE name_60 expr_266 expr_267 .default +def expr_269 : Lean.Expr := .forallE name_60 expr_56 expr_268 .default +def name_66 : Lean.Name := .str name_60 "term_+_" +def expr_270 : Lean.Expr := .forallE name_8 expr_269 expr_46 .default +def expr_271 : Lean.Expr := .forallE name_8 expr_4 expr_270 .default +def expr_272 : Lean.Expr := .forallE name_8 expr_241 expr_271 .default +def expr_273 : Lean.Expr := .forallE name_8 expr_0 expr_272 .default +def expr_274 : Lean.Expr := .const name_13 [level_0, level_1] +def expr_275 : Lean.Expr := .app expr_274 expr_15 +def expr_276 : Lean.Expr := .app expr_15 expr_1 +def expr_277 : Lean.Expr := .app expr_253 expr_276 +def expr_278 : Lean.Expr := .app expr_263 expr_20 +def expr_279 : Lean.Expr := .app expr_278 expr_15 +def expr_280 : Lean.Expr := .app expr_279 expr_1 +def expr_281 : Lean.Expr := .app expr_277 expr_280 +def expr_282 : Lean.Expr := .lam name_8 expr_63 expr_281 .default +def expr_283 : Lean.Expr := .app expr_275 expr_282 +def name_67 : Lean.Name := .str name_64 "intro" +def expr_284 : Lean.Expr := .const name_67 [] +def expr_285 : Lean.Expr := .app expr_14 expr_20 +def expr_286 : Lean.Expr := .app expr_285 expr_1 +def expr_287 : Lean.Expr := .app expr_15 expr_286 +def expr_288 : Lean.Expr := .app expr_284 expr_287 +def expr_289 : Lean.Expr := .app expr_288 expr_249 +def expr_290 : Lean.Expr := .app expr_3 expr_286 +def name_68 : Lean.Name := .str name_63 "intro" +def expr_291 : Lean.Expr := .const name_68 [] +def expr_292 : Lean.Expr := .app expr_290 expr_291 +def expr_293 : Lean.Expr := .app expr_289 expr_292 +def expr_294 : Lean.Expr := .app expr_293 expr_291 +def expr_295 : Lean.Expr := .lam name_54 expr_15 expr_294 .default +def expr_296 : Lean.Expr := .app expr_283 expr_295 +def expr_297 : Lean.Expr := .app expr_20 expr_43 +def expr_298 : Lean.Expr := .app expr_253 expr_297 +def expr_299 : Lean.Expr := .app expr_263 expr_40 +def expr_300 : Lean.Expr := .app expr_299 expr_20 +def expr_301 : Lean.Expr := .app expr_300 expr_43 +def expr_302 : Lean.Expr := .app expr_298 expr_301 +def expr_303 : Lean.Expr := .forallE name_54 expr_20 expr_302 .default +def expr_304 : Lean.Expr := .app expr_23 expr_40 +def expr_305 : Lean.Expr := .app expr_304 expr_3 +def expr_306 : Lean.Expr := .app expr_20 expr_305 +def expr_307 : Lean.Expr := .app expr_284 expr_306 +def expr_308 : Lean.Expr := .app expr_40 expr_37 +def expr_309 : Lean.Expr := .forallE name_54 expr_40 expr_308 .default +def expr_310 : Lean.Expr := .app expr_253 expr_309 +def expr_311 : Lean.Expr := .app expr_263 expr_85 +def expr_312 : Lean.Expr := .app expr_311 expr_40 +def expr_313 : Lean.Expr := .app expr_312 expr_37 +def expr_314 : Lean.Expr := .forallE name_54 expr_40 expr_313 .default +def expr_315 : Lean.Expr := .app expr_310 expr_314 +def expr_316 : Lean.Expr := .app expr_307 expr_315 +def expr_317 : Lean.Expr := .app expr_13 expr_305 +def expr_318 : Lean.Expr := .app expr_284 expr_309 +def expr_319 : Lean.Expr := .app expr_318 expr_314 +def expr_320 : Lean.Expr := .proj name_64 0 expr_43 +def expr_321 : Lean.Expr := .lam name_54 expr_40 expr_320 .default +def expr_322 : Lean.Expr := .app expr_319 expr_321 +def expr_323 : Lean.Expr := .proj name_64 1 expr_43 +def expr_324 : Lean.Expr := .lam name_54 expr_40 expr_323 .default +def expr_325 : Lean.Expr := .app expr_322 expr_324 +def expr_326 : Lean.Expr := .app expr_317 expr_325 +def expr_327 : Lean.Expr := .app expr_316 expr_326 +def expr_328 : Lean.Expr := .app expr_327 expr_325 +def expr_329 : Lean.Expr := .lam name_54 expr_303 expr_328 .default +def expr_330 : Lean.Expr := .lam name_54 expr_22 expr_329 .default +def expr_331 : Lean.Expr := .app expr_296 expr_330 +def expr_332 : Lean.Expr := .app expr_331 expr_3 +def expr_333 : Lean.Expr := .proj name_64 0 expr_332 +def expr_334 : Lean.Expr := .lam name_54 expr_269 expr_333 .default +def expr_335 : Lean.Expr := .lam name_54 expr_4 expr_334 .default +def expr_336 : Lean.Expr := .lam name_54 expr_241 expr_335 .default +def expr_337 : Lean.Expr := .lam name_54 expr_0 expr_336 .default +def name_69 : Lean.Name := .str name_54 "mp" +def decl_7 : Lean.Declaration := + .defnDecl { + name := name_69 + levelParams := [name_16] + type := expr_273 + value := expr_337 + hints := .opaque + safety := .safe + all := [name_69] + } +def expr_338 : Lean.Expr := .const name_62 [level_3, level_1] +def expr_339 : Lean.Expr := .app expr_338 expr_15 +def expr_340 : Lean.Expr := .app expr_339 expr_13 +def expr_341 : Lean.Expr := .app expr_340 expr_1 +def expr_342 : Lean.Expr := .forallE name_16 expr_341 expr_267 .default +def expr_343 : Lean.Expr := .forallE name_16 expr_56 expr_342 .default +def expr_344 : Lean.Expr := .forallE name_16 expr_343 expr_46 .default +def expr_345 : Lean.Expr := .forallE name_16 expr_4 expr_344 .default +def expr_346 : Lean.Expr := .forallE name_16 expr_213 expr_345 .default +def expr_347 : Lean.Expr := .forallE name_16 expr_0 expr_346 .default +def expr_348 : Lean.Expr := .const name_13 [level_6, level_1] +def expr_349 : Lean.Expr := .app expr_348 expr_15 +def expr_350 : Lean.Expr := .const name_61 [level_4, level_6] +def expr_351 : Lean.Expr := .app expr_350 expr_276 +def expr_352 : Lean.Expr := .app expr_338 expr_20 +def expr_353 : Lean.Expr := .app expr_352 expr_15 +def expr_354 : Lean.Expr := .app expr_353 expr_1 +def expr_355 : Lean.Expr := .app expr_351 expr_354 +def expr_356 : Lean.Expr := .lam name_16 expr_63 expr_355 .default +def expr_357 : Lean.Expr := .app expr_349 expr_356 +def name_70 : Lean.Name := .str name_61 "mk" +def expr_358 : Lean.Expr := .const name_70 [level_4, level_6] +def expr_359 : Lean.Expr := .app expr_358 expr_287 +def expr_360 : Lean.Expr := .app expr_359 expr_222 +def name_71 : Lean.Name := .str name_60 "unit" +def expr_361 : Lean.Expr := .const name_71 [level_6] +def expr_362 : Lean.Expr := .app expr_290 expr_361 +def expr_363 : Lean.Expr := .app expr_360 expr_362 +def expr_364 : Lean.Expr := .app expr_363 expr_361 +def expr_365 : Lean.Expr := .lam name_24 expr_15 expr_364 .default +def expr_366 : Lean.Expr := .app expr_357 expr_365 +def expr_367 : Lean.Expr := .app expr_350 expr_297 +def expr_368 : Lean.Expr := .app expr_338 expr_40 +def expr_369 : Lean.Expr := .app expr_368 expr_20 +def expr_370 : Lean.Expr := .app expr_369 expr_43 +def expr_371 : Lean.Expr := .app expr_367 expr_370 +def expr_372 : Lean.Expr := .forallE name_24 expr_20 expr_371 .default +def level_10 : Lean.Level := .max level_6 level_6 +def expr_373 : Lean.Expr := .const name_70 [level_5, level_10] +def expr_374 : Lean.Expr := .app expr_373 expr_306 +def expr_375 : Lean.Expr := .app expr_227 expr_309 +def expr_376 : Lean.Expr := .app expr_338 expr_85 +def expr_377 : Lean.Expr := .app expr_376 expr_40 +def expr_378 : Lean.Expr := .app expr_377 expr_37 +def expr_379 : Lean.Expr := .forallE name_24 expr_40 expr_378 .default +def expr_380 : Lean.Expr := .app expr_375 expr_379 +def expr_381 : Lean.Expr := .app expr_374 expr_380 +def expr_382 : Lean.Expr := .const name_70 [level_8, level_8] +def expr_383 : Lean.Expr := .app expr_382 expr_309 +def expr_384 : Lean.Expr := .app expr_383 expr_379 +def expr_385 : Lean.Expr := .proj name_61 0 expr_43 +def expr_386 : Lean.Expr := .lam name_24 expr_40 expr_385 .default +def expr_387 : Lean.Expr := .app expr_384 expr_386 +def expr_388 : Lean.Expr := .proj name_61 1 expr_43 +def expr_389 : Lean.Expr := .lam name_24 expr_40 expr_388 .default +def expr_390 : Lean.Expr := .app expr_387 expr_389 +def expr_391 : Lean.Expr := .app expr_317 expr_390 +def expr_392 : Lean.Expr := .app expr_381 expr_391 +def expr_393 : Lean.Expr := .app expr_392 expr_390 +def expr_394 : Lean.Expr := .lam name_24 expr_372 expr_393 .default +def expr_395 : Lean.Expr := .lam name_24 expr_22 expr_394 .default +def expr_396 : Lean.Expr := .app expr_366 expr_395 +def expr_397 : Lean.Expr := .app expr_396 expr_3 +def expr_398 : Lean.Expr := .proj name_61 0 expr_397 +def expr_399 : Lean.Expr := .lam name_24 expr_343 expr_398 .default +def expr_400 : Lean.Expr := .lam name_24 expr_4 expr_399 .default +def expr_401 : Lean.Expr := .lam name_24 expr_213 expr_400 .default +def expr_402 : Lean.Expr := .lam name_24 expr_0 expr_401 .default +def level_11 : Lean.Level := .succ level_5 +def decl_8 : Lean.Declaration := + .defnDecl { + name := `foo42 + levelParams := [name_14, name_24] + type := expr_347 + value := expr_402 + hints := .opaque + safety := .safe + all := [`foo42] + } +def expr_403 : Lean.Expr := .app expr_246 expr_246 +def expr_404 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_405 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_406 : Lean.Expr := .const `foo42 [level_0, level_0] +def expr_407 : Lean.Expr := .app expr_406 expr_126 +def expr_408 : Lean.Expr := .lam name_24 expr_96 expr_15 .default +def expr_409 : Lean.Expr := .app expr_407 expr_408 +def expr_410 : Lean.Expr := .app expr_409 expr_36 +def expr_411 : Lean.Expr := .const name_24 [level_0] +def expr_412 : Lean.Expr := .app expr_388 expr_388 +def expr_413 : Lean.Expr := .lam name_24 expr_359 expr_359 .default +def expr_414 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_415 : Lean.Expr := .proj name_24 12336 expr_301 +def expr_416 : Lean.Expr := .bvar 12336 +def expr_417 : Lean.Expr := .app expr_243 expr_243 +def expr_418 : Lean.Expr := .app expr_214 expr_214 +def expr_419 : Lean.Expr := .lam name_24 expr_185 expr_185 .default +def expr_420 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_421 : Lean.Expr := .app expr_127 expr_127 +def expr_422 : Lean.Expr := .forallE name_24 expr_98 expr_98 .default +def expr_423 : Lean.Expr := .lam name_24 expr_69 expr_69 .default +def expr_424 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_425 : Lean.Expr := .app expr_11 expr_11 +def expr_426 : Lean.Expr := .app expr_408 expr_408 +def expr_427 : Lean.Expr := .bvar 12336 +def expr_428 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_429 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def level_12 : Lean.Level := .succ level_0 +def expr_430 : Lean.Expr := .lam name_24 expr_296 expr_296 .default +def expr_431 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_432 : Lean.Expr := .app expr_240 expr_240 +def expr_433 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_434 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_435 : Lean.Expr := .app expr_156 expr_156 +def expr_436 : Lean.Expr := .lam name_24 expr_128 expr_128 .default +def expr_437 : Lean.Expr := .lam name_24 expr_100 expr_100 .default +def expr_438 : Lean.Expr := .app expr_72 expr_72 +def expr_439 : Lean.Expr := .app expr_44 expr_44 +def expr_440 : Lean.Expr := .lit (.natVal (decodeNatLit [0])) +def expr_441 : Lean.Expr := .lam name_24 expr_429 expr_429 .default +def expr_442 : Lean.Expr := .app expr_410 expr_402 +def expr_443 : Lean.Expr := .lam name_24 expr_375 expr_442 .default +def expr_444 : Lean.Expr := .lit (.natVal (decodeNatLit [])) +def decl_9 : Lean.Declaration := + .thmDecl { + name := name_24 + levelParams := [] + type := expr_443 + value := expr_0 + } +run_meta Lean.addDecl decl_0 +run_meta Lean.addDecl decl_1 +run_meta Lean.addDecl decl_2 +run_meta Lean.addDecl decl_3 +run_meta Lean.addDecl decl_4 +run_meta Lean.addDecl decl_5 +run_meta Lean.addDecl decl_6 +run_meta Lean.addDecl decl_7 +run_meta Lean.addDecl decl_8 +/-- +error: (kernel) type checker does not support loose bound variables, replace them with free variables before invoking it +-/ +#guard_msgs in +run_meta Lean.addDecl decl_9 diff --git a/tests/lean/run/recconstructorcrash.lean b/tests/lean/run/recconstructorcrash.lean new file mode 100644 index 0000000000..334ee41e62 --- /dev/null +++ b/tests/lean/run/recconstructorcrash.lean @@ -0,0 +1,4 @@ +/-- error: (kernel) constant has already been declared 'X.rec' -/ +#guard_msgs in +inductive X where + | rec