feat: additional tests for bad recursors

tests/rec-orphan-bad-ind.lean

@@ -0,0 +1,29 @@
+module
+import all Lean.Environment
+import Lean
+
+public section
+open Lean Elab Command
+set_option Elab.async false
+
+run_cmd do
+  let rogue : RecursorVal := {
+    name := `rogue
+    levelParams := []
+    type := mkConst ``False
+    all := [`Foo]
+    numParams := 0
+    numIndices := 0
+    numMotives := 0
+    numMinors := 0
+    rules := []
+    k := false
+    isUnsafe := false
+  }
+  modifyEnv fun env => env.lakeAdd (.recInfo rogue)
+  liftCoreM <| addDecl <| .thmDecl {
+    name := `inconsistent
+    levelParams := []
+    type := mkConst ``False
+    value := mkConst `rogue
+  }

tests/rec-orphan-bad-ind.ndjson

@@ -0,0 +1,22 @@
+{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"format":{"version":"3.1.0"},"lean":{"githash":"f72c35b3f637c8c6571d353742168ab66cc22c00","version":"4.29.1"}}}
+{"in":1,"str":{"pre":0,"str":"False"}}
+{"ie":0,"sort":0}
+{"in":2,"str":{"pre":0,"str":"rogue"}}
+{"const":{"name":1,"us":[]},"ie":1}
+{"in":3,"str":{"pre":1,"str":"rec"}}
+{"in":4,"str":{"pre":0,"str":"u"}}
+{"il":1,"param":4}
+{"in":5,"str":{"pre":0,"str":"motive"}}
+{"in":6,"str":{"pre":0,"str":"t"}}
+{"ie":2,"sort":1}
+{"forallE":{"binderInfo":"default","body":2,"name":6,"type":1},"ie":3}
+{"bvar":1,"ie":4}
+{"bvar":0,"ie":5}
+{"app":{"arg":5,"fn":4},"ie":6}
+{"forallE":{"binderInfo":"default","body":6,"name":6,"type":1},"ie":7}
+{"forallE":{"binderInfo":"default","body":7,"name":5,"type":3},"ie":8}
+{"in":7,"str":{"pre":0,"str":"Foo"}}
+{"inductive":{"ctors":[],"recs":[{"all":[7],"isUnsafe":false,"k":false,"levelParams":[],"name":2,"numIndices":0,"numMinors":0,"numMotives":0,"numParams":0,"rules":[],"type":1},{"all":[1],"isUnsafe":false,"k":false,"levelParams":[4],"name":3,"numIndices":0,"numMinors":0,"numMotives":1,"numParams":0,"rules":[],"type":8}],"types":[{"all":[1],"ctors":[],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":1,"numIndices":0,"numNested":0,"numParams":0,"type":0}]}}
+{"in":8,"str":{"pre":0,"str":"inconsistent"}}
+{"const":{"name":2,"us":[]},"ie":9}
+{"thm":{"all":[8],"levelParams":[],"name":8,"type":1,"value":9}}

tests/rec-orphan-bad-ind.yaml

@@ -0,0 +1,19 @@
+description: |
+  Proof of `False` from an extra recursor claiming it is derived from an 
+  inductive type that does not actually exist in the environment.
+
+  A checker must derive the recursors of an inductive group from a legitimate 
+  inductive declaration and reject any exported recursor that is not tied to 
+  an inductive type.
+
+  The export contains `False` exactly as the prelude has it — an empty
+  `Prop`-valued inductive with no constructors — together with its ordinary
+  `False.rec`. The theorem `inconsistent : False` is then simply
+  `rogue`.
+# Frozen as a static export file: the recursor is injected with the private,
+# kernel-bypassing `Environment.lakeAdd`, which is liable to change, whereas this
+# export is small and needs to stay exactly as it is.  It was produced by
+# tests/rec-orphan-bad-ind.lean, kept next to it as the reproducer, with the toolchain
+# from tests/lean-toolchain (v4.29.1).
+leanfile: tests/rec-orphan-bad-ind.lean
+outcome: reject

tests/rec-orphan-empty.lean

@@ -0,0 +1,29 @@
+module
+import all Lean.Environment
+import Lean
+
+public section
+open Lean Elab Command
+set_option Elab.async false
+
+run_cmd do
+  let rogue : RecursorVal := {
+    name := `rogue
+    levelParams := []
+    type := mkConst ``False
+    all := []
+    numParams := 0
+    numIndices := 0
+    numMotives := 0
+    numMinors := 0
+    rules := []
+    k := false
+    isUnsafe := false
+  }
+  modifyEnv fun env => env.lakeAdd (.recInfo rogue)
+  liftCoreM <| addDecl <| .thmDecl {
+    name := `inconsistent
+    levelParams := []
+    type := mkConst ``False
+    value := mkConst `rogue
+  }

tests/rec-orphan-empty.ndjson

@@ -0,0 +1,21 @@
+{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"format":{"version":"3.1.0"},"lean":{"githash":"f72c35b3f637c8c6571d353742168ab66cc22c00","version":"4.29.1"}}}
+{"in":1,"str":{"pre":0,"str":"False"}}
+{"ie":0,"sort":0}
+{"in":2,"str":{"pre":0,"str":"rogue"}}
+{"const":{"name":1,"us":[]},"ie":1}
+{"in":3,"str":{"pre":1,"str":"rec"}}
+{"in":4,"str":{"pre":0,"str":"u"}}
+{"il":1,"param":4}
+{"in":5,"str":{"pre":0,"str":"motive"}}
+{"in":6,"str":{"pre":0,"str":"t"}}
+{"ie":2,"sort":1}
+{"forallE":{"binderInfo":"default","body":2,"name":6,"type":1},"ie":3}
+{"bvar":1,"ie":4}
+{"bvar":0,"ie":5}
+{"app":{"arg":5,"fn":4},"ie":6}
+{"forallE":{"binderInfo":"default","body":6,"name":6,"type":1},"ie":7}
+{"forallE":{"binderInfo":"default","body":7,"name":5,"type":3},"ie":8}
+{"inductive":{"ctors":[],"recs":[{"all":[],"isUnsafe":false,"k":false,"levelParams":[],"name":2,"numIndices":0,"numMinors":0,"numMotives":0,"numParams":0,"rules":[],"type":1},{"all":[1],"isUnsafe":false,"k":false,"levelParams":[4],"name":3,"numIndices":0,"numMinors":0,"numMotives":1,"numParams":0,"rules":[],"type":8}],"types":[{"all":[1],"ctors":[],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":1,"numIndices":0,"numNested":0,"numParams":0,"type":0}]}}
+{"in":7,"str":{"pre":0,"str":"inconsistent"}}
+{"const":{"name":2,"us":[]},"ie":9}
+{"thm":{"all":[7],"levelParams":[],"name":7,"type":1,"value":9}}

tests/rec-orphan-empty.yaml

@@ -0,0 +1,19 @@
+description: |
+  Proof of `False` from an extra recursor not claiming to be tied to any 
+  inductive.
+
+  A checker must derive the recursors of an inductive group from an inductive
+  declaration and reject any exported recursor that is not tied to an 
+  inductive type. 
+
+  The export contains `False` exactly as the prelude has it — an empty
+  `Prop`-valued inductive with no constructors — together with its ordinary
+  `False.rec`. The theorem `inconsistent : False` is then simply
+  `rogue`.
+# Frozen as a static export file: the recursor is injected with the private,
+# kernel-bypassing `Environment.lakeAdd`, which is liable to change, whereas this
+# export is small and needs to stay exactly as it is.  It was produced by
+# tests/rec-orphan-empty.lean, kept next to it as the reproducer, with the toolchain
+# from tests/lean-toolchain (v4.29.1).
+file: tests/rec-orphan-empty.ndjson
+outcome: reject