Skip to content

feat: test case for leanprover/lean4#10577 #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nomeata merged 4 commits into from
Feb 26, 2026
Merged

feat: test case for leanprover/lean4#10577 #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
54dd11a
Add test case for #10577
TwoFX Feb 26, 2026
b8bc0d2
Claude-produced fix for the problem that file tests are not discovered
TwoFX Feb 26, 2026
1023cae
Improve description
TwoFX Feb 26, 2026
c165f48
Merge master into 10577 (take master's lka.py)
nomeata Feb 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
283 changes: 283 additions & 0 deletions tests/constlevels.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,283 @@
{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"format":{"version":"3.1.0"},"lean":{"githash":"83e54b65b65d1d3ce31d99d820a7bd5f3e219295","version":"4.29.0-rc2"}}}
{"in":1,"str":{"pre":0,"str":"Nat"}}
{"il":1,"succ":0}
{"ie":0,"sort":1}
{"in":2,"str":{"pre":1,"str":"zero"}}
{"in":3,"str":{"pre":1,"str":"succ"}}
{"const":{"name":1,"us":[]},"ie":1}
{"in":4,"str":{"pre":0,"str":"n"}}
{"forallE":{"binderInfo":"default","body":1,"name":4,"type":1},"ie":2}
{"in":5,"str":{"pre":1,"str":"rec"}}
{"in":6,"str":{"pre":0,"str":"u"}}
{"il":2,"param":6}
{"in":7,"str":{"pre":0,"str":"motive"}}
{"in":8,"str":{"pre":0,"str":"t"}}
{"ie":3,"sort":2}
{"forallE":{"binderInfo":"default","body":3,"name":8,"type":1},"ie":4}
{"in":9,"str":{"pre":0,"str":"zero"}}
{"bvar":0,"ie":5}
{"const":{"name":2,"us":[]},"ie":6}
{"app":{"arg":6,"fn":5},"ie":7}
{"in":10,"str":{"pre":0,"str":"succ"}}
{"in":11,"str":{"pre":0,"str":"n_ih"}}
{"bvar":2,"ie":8}
{"app":{"arg":5,"fn":8},"ie":9}
{"bvar":3,"ie":10}
{"const":{"name":3,"us":[]},"ie":11}
{"bvar":1,"ie":12}
{"app":{"arg":12,"fn":11},"ie":13}
{"app":{"arg":13,"fn":10},"ie":14}
{"forallE":{"binderInfo":"default","body":14,"name":11,"type":9},"ie":15}
{"forallE":{"binderInfo":"default","body":15,"name":4,"type":1},"ie":16}
{"app":{"arg":5,"fn":10},"ie":17}
{"forallE":{"binderInfo":"default","body":17,"name":8,"type":1},"ie":18}
{"forallE":{"binderInfo":"default","body":18,"name":10,"type":16},"ie":19}
{"forallE":{"binderInfo":"default","body":19,"name":9,"type":7},"ie":20}
{"forallE":{"binderInfo":"implicit","body":20,"name":7,"type":4},"ie":21}
{"ie":22,"lam":{"binderInfo":"default","body":12,"name":10,"type":16}}
{"ie":23,"lam":{"binderInfo":"default","body":22,"name":9,"type":7}}
{"ie":24,"lam":{"binderInfo":"default","body":23,"name":7,"type":4}}
{"app":{"arg":5,"fn":12},"ie":25}
{"const":{"name":5,"us":[2]},"ie":26}
{"app":{"arg":10,"fn":26},"ie":27}
{"app":{"arg":8,"fn":27},"ie":28}
{"app":{"arg":12,"fn":28},"ie":29}
{"app":{"arg":5,"fn":29},"ie":30}
{"app":{"arg":30,"fn":25},"ie":31}
{"ie":32,"lam":{"binderInfo":"default","body":31,"name":4,"type":1}}
{"ie":33,"lam":{"binderInfo":"default","body":32,"name":10,"type":16}}
{"ie":34,"lam":{"binderInfo":"default","body":33,"name":9,"type":7}}
{"ie":35,"lam":{"binderInfo":"default","body":34,"name":7,"type":4}}
{"inductive":{"ctors":[{"cidx":0,"induct":1,"isUnsafe":false,"levelParams":[],"name":2,"numFields":0,"numParams":0,"type":1},{"cidx":1,"induct":1,"isUnsafe":false,"levelParams":[],"name":3,"numFields":1,"numParams":0,"type":2}],"recs":[{"all":[1],"isUnsafe":false,"k":false,"levelParams":[6],"name":5,"numIndices":0,"numMinors":2,"numMotives":1,"numParams":0,"rules":[{"ctor":2,"nfields":0,"rhs":24},{"ctor":3,"nfields":1,"rhs":35}],"type":21}],"types":[{"all":[1],"ctors":[2,3],"isRec":true,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":1,"numIndices":0,"numNested":0,"numParams":0,"type":0}]}}
{"in":12,"str":{"pre":0,"str":"Eq"}}
{"in":13,"str":{"pre":0,"str":"u_1"}}
{"il":3,"param":13}
{"in":14,"str":{"pre":0,"str":"α"}}
{"ie":36,"sort":3}
{"in":15,"str":{"pre":0,"str":"a"}}
{"in":16,"str":{"pre":15,"str":"_@"}}
{"in":17,"str":{"pre":16,"str":"_internal"}}
{"in":18,"str":{"pre":17,"str":"_hyg"}}
{"in":19,"num":{"i":0,"pre":18}}
{"ie":37,"sort":0}
{"forallE":{"binderInfo":"default","body":37,"name":19,"type":12},"ie":38}
{"forallE":{"binderInfo":"default","body":38,"name":19,"type":5},"ie":39}
{"forallE":{"binderInfo":"implicit","body":39,"name":14,"type":36},"ie":40}
{"in":20,"str":{"pre":12,"str":"refl"}}
{"const":{"name":12,"us":[3]},"ie":41}
{"app":{"arg":12,"fn":41},"ie":42}
{"app":{"arg":5,"fn":42},"ie":43}
{"app":{"arg":5,"fn":43},"ie":44}
{"forallE":{"binderInfo":"default","body":44,"name":15,"type":5},"ie":45}
{"forallE":{"binderInfo":"implicit","body":45,"name":14,"type":36},"ie":46}
{"in":21,"str":{"pre":12,"str":"rec"}}
{"app":{"arg":8,"fn":41},"ie":47}
{"app":{"arg":12,"fn":47},"ie":48}
{"app":{"arg":5,"fn":48},"ie":49}
{"forallE":{"binderInfo":"default","body":3,"name":8,"type":49},"ie":50}
{"forallE":{"binderInfo":"default","body":50,"name":19,"type":12},"ie":51}
{"in":22,"str":{"pre":0,"str":"refl"}}
{"app":{"arg":12,"fn":5},"ie":52}
{"const":{"name":20,"us":[3]},"ie":53}
{"app":{"arg":8,"fn":53},"ie":54}
{"app":{"arg":12,"fn":54},"ie":55}
{"app":{"arg":55,"fn":52},"ie":56}
{"bvar":4,"ie":57}
{"app":{"arg":57,"fn":41},"ie":58}
{"app":{"arg":10,"fn":58},"ie":59}
{"app":{"arg":5,"fn":59},"ie":60}
{"app":{"arg":12,"fn":10},"ie":61}
{"app":{"arg":5,"fn":61},"ie":62}
{"forallE":{"binderInfo":"default","body":62,"name":8,"type":60},"ie":63}
{"forallE":{"binderInfo":"implicit","body":63,"name":19,"type":10},"ie":64}
{"forallE":{"binderInfo":"default","body":64,"name":22,"type":56},"ie":65}
{"forallE":{"binderInfo":"implicit","body":65,"name":7,"type":51},"ie":66}
{"forallE":{"binderInfo":"implicit","body":66,"name":19,"type":5},"ie":67}
{"forallE":{"binderInfo":"implicit","body":67,"name":14,"type":36},"ie":68}
{"ie":69,"lam":{"binderInfo":"default","body":5,"name":22,"type":56}}
{"ie":70,"lam":{"binderInfo":"default","body":69,"name":7,"type":51}}
{"ie":71,"lam":{"binderInfo":"default","body":70,"name":19,"type":5}}
{"ie":72,"lam":{"binderInfo":"implicit","body":71,"name":14,"type":36}}
{"inductive":{"ctors":[{"cidx":0,"induct":12,"isUnsafe":false,"levelParams":[13],"name":20,"numFields":0,"numParams":2,"type":46}],"recs":[{"all":[12],"isUnsafe":false,"k":true,"levelParams":[6,13],"name":21,"numIndices":1,"numMinors":1,"numMotives":1,"numParams":2,"rules":[{"ctor":20,"nfields":0,"rhs":72}],"type":68}],"types":[{"all":[12],"ctors":[20],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[13],"name":12,"numIndices":1,"numNested":0,"numParams":2,"type":40}]}}
{"in":23,"str":{"pre":0,"str":"False"}}
{"in":24,"str":{"pre":23,"str":"rec"}}
{"const":{"name":23,"us":[]},"ie":73}
{"forallE":{"binderInfo":"default","body":3,"name":8,"type":73},"ie":74}
{"forallE":{"binderInfo":"default","body":25,"name":8,"type":73},"ie":75}
{"forallE":{"binderInfo":"default","body":75,"name":7,"type":74},"ie":76}
{"inductive":{"ctors":[],"recs":[{"all":[23],"isUnsafe":false,"k":false,"levelParams":[6],"name":24,"numIndices":0,"numMinors":0,"numMotives":1,"numParams":0,"rules":[],"type":76}],"types":[{"all":[23],"ctors":[],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":23,"numIndices":0,"numNested":0,"numParams":0,"type":37}]}}
{"in":25,"str":{"pre":0,"str":"Not"}}
{"forallE":{"binderInfo":"default","body":37,"name":15,"type":37},"ie":77}
{"forallE":{"binderInfo":"default","body":73,"name":19,"type":5},"ie":78}
{"ie":79,"lam":{"binderInfo":"default","body":78,"name":15,"type":37}}
{"def":{"all":[25],"hints":{"regular":1},"levelParams":[],"name":25,"safety":"safe","type":77,"value":79}}
{"in":26,"str":{"pre":0,"str":"Ne"}}
{"forallE":{"binderInfo":"implicit","body":39,"name":14,"type":3},"ie":80}
{"in":27,"str":{"pre":0,"str":"b"}}
{"const":{"name":25,"us":[]},"ie":81}
{"const":{"name":12,"us":[2]},"ie":82}
{"app":{"arg":8,"fn":82},"ie":83}
{"app":{"arg":12,"fn":83},"ie":84}
{"app":{"arg":5,"fn":84},"ie":85}
{"app":{"arg":85,"fn":81},"ie":86}
{"ie":87,"lam":{"binderInfo":"default","body":86,"name":27,"type":12}}
{"ie":88,"lam":{"binderInfo":"default","body":87,"name":15,"type":5}}
{"ie":89,"lam":{"binderInfo":"implicit","body":88,"name":14,"type":3}}
{"def":{"all":[26],"hints":{"regular":2},"levelParams":[6],"name":26,"safety":"safe","type":80,"value":89}}
{"in":28,"str":{"pre":0,"str":"True"}}
{"in":29,"str":{"pre":28,"str":"intro"}}
{"const":{"name":28,"us":[]},"ie":90}
{"in":30,"str":{"pre":28,"str":"rec"}}
{"forallE":{"binderInfo":"default","body":3,"name":8,"type":90},"ie":91}
{"in":31,"str":{"pre":0,"str":"intro"}}
{"const":{"name":29,"us":[]},"ie":92}
{"app":{"arg":92,"fn":5},"ie":93}
{"forallE":{"binderInfo":"default","body":9,"name":8,"type":90},"ie":94}
{"forallE":{"binderInfo":"default","body":94,"name":31,"type":93},"ie":95}
{"forallE":{"binderInfo":"implicit","body":95,"name":7,"type":91},"ie":96}
{"ie":97,"lam":{"binderInfo":"default","body":5,"name":31,"type":93}}
{"ie":98,"lam":{"binderInfo":"default","body":97,"name":7,"type":91}}
{"inductive":{"ctors":[{"cidx":0,"induct":28,"isUnsafe":false,"levelParams":[],"name":29,"numFields":0,"numParams":0,"type":90}],"recs":[{"all":[28],"isUnsafe":false,"k":true,"levelParams":[6],"name":30,"numIndices":0,"numMinors":1,"numMotives":1,"numParams":0,"rules":[{"ctor":29,"nfields":0,"rhs":98}],"type":96}],"types":[{"all":[28],"ctors":[29],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":28,"numIndices":0,"numNested":0,"numParams":0,"type":37}]}}
{"in":32,"str":{"pre":0,"str":"trivial"}}
{"thm":{"all":[32],"levelParams":[],"name":32,"type":90,"value":92}}
{"in":33,"str":{"pre":0,"str":"rfl"}}
{"app":{"arg":12,"fn":82},"ie":99}
{"app":{"arg":5,"fn":99},"ie":100}
{"app":{"arg":5,"fn":100},"ie":101}
{"forallE":{"binderInfo":"implicit","body":101,"name":15,"type":5},"ie":102}
{"forallE":{"binderInfo":"implicit","body":102,"name":14,"type":3},"ie":103}
{"const":{"name":20,"us":[2]},"ie":104}
{"app":{"arg":12,"fn":104},"ie":105}
{"app":{"arg":5,"fn":105},"ie":106}
{"ie":107,"lam":{"binderInfo":"implicit","body":106,"name":15,"type":5}}
{"ie":108,"lam":{"binderInfo":"implicit","body":107,"name":14,"type":3}}
{"def":{"all":[33],"hints":{"regular":1},"levelParams":[6],"name":33,"safety":"safe","type":103,"value":108}}
{"in":34,"str":{"pre":12,"str":"symm"}}
{"in":35,"str":{"pre":0,"str":"h"}}
{"app":{"arg":10,"fn":82},"ie":109}
{"app":{"arg":12,"fn":109},"ie":110}
{"app":{"arg":8,"fn":110},"ie":111}
{"forallE":{"binderInfo":"default","body":111,"name":35,"type":85},"ie":112}
{"forallE":{"binderInfo":"implicit","body":112,"name":27,"type":12},"ie":113}
{"forallE":{"binderInfo":"implicit","body":113,"name":15,"type":5},"ie":114}
{"forallE":{"binderInfo":"implicit","body":114,"name":14,"type":3},"ie":115}
{"const":{"name":21,"us":[0,2]},"ie":116}
{"app":{"arg":10,"fn":116},"ie":117}
{"app":{"arg":8,"fn":117},"ie":118}
{"in":36,"str":{"pre":0,"str":"x"}}
{"in":37,"str":{"pre":36,"str":"_@"}}
{"in":38,"str":{"pre":37,"str":"Init"}}
{"in":39,"str":{"pre":38,"str":"Prelude"}}
{"in":40,"num":{"i":2345006592,"pre":39}}
{"in":41,"str":{"pre":40,"str":"_hygCtx"}}
{"in":42,"str":{"pre":41,"str":"_hyg"}}
{"in":43,"num":{"i":14,"pre":42}}
{"in":44,"str":{"pre":35,"str":"_@"}}
{"in":45,"str":{"pre":44,"str":"Init"}}
{"in":46,"str":{"pre":45,"str":"Prelude"}}
{"in":47,"num":{"i":2345006592,"pre":46}}
{"in":48,"str":{"pre":47,"str":"_hygCtx"}}
{"in":49,"str":{"pre":48,"str":"_hyg"}}
{"in":50,"num":{"i":15,"pre":49}}
{"app":{"arg":57,"fn":82},"ie":119}
{"app":{"arg":10,"fn":119},"ie":120}
{"app":{"arg":5,"fn":120},"ie":121}
{"bvar":5,"ie":122}
{"app":{"arg":122,"fn":82},"ie":123}
{"app":{"arg":12,"fn":123},"ie":124}
{"app":{"arg":57,"fn":124},"ie":125}
{"ie":126,"lam":{"binderInfo":"default","body":125,"name":50,"type":121}}
{"ie":127,"lam":{"binderInfo":"default","body":126,"name":43,"type":10}}
{"app":{"arg":127,"fn":118},"ie":128}
{"const":{"name":33,"us":[2]},"ie":129}
{"app":{"arg":10,"fn":129},"ie":130}
{"app":{"arg":8,"fn":130},"ie":131}
{"app":{"arg":131,"fn":128},"ie":132}
{"app":{"arg":12,"fn":132},"ie":133}
{"app":{"arg":5,"fn":133},"ie":134}
{"ie":135,"lam":{"binderInfo":"default","body":134,"name":35,"type":85}}
{"ie":136,"lam":{"binderInfo":"implicit","body":135,"name":27,"type":12}}
{"ie":137,"lam":{"binderInfo":"implicit","body":136,"name":15,"type":5}}
{"ie":138,"lam":{"binderInfo":"implicit","body":137,"name":14,"type":3}}
{"thm":{"all":[34],"levelParams":[6],"name":34,"type":115,"value":138}}
{"in":51,"str":{"pre":0,"str":"false_ne_true"}}
{"const":{"name":26,"us":[1]},"ie":139}
{"app":{"arg":37,"fn":139},"ie":140}
{"app":{"arg":73,"fn":140},"ie":141}
{"app":{"arg":90,"fn":141},"ie":142}
{"const":{"name":12,"us":[1]},"ie":143}
{"app":{"arg":37,"fn":143},"ie":144}
{"app":{"arg":73,"fn":144},"ie":145}
{"app":{"arg":90,"fn":145},"ie":146}
{"const":{"name":21,"us":[0,1]},"ie":147}
{"app":{"arg":37,"fn":147},"ie":148}
{"app":{"arg":90,"fn":148},"ie":149}
{"in":52,"str":{"pre":38,"str":"Core"}}
{"in":53,"num":{"i":789336685,"pre":52}}
{"in":54,"str":{"pre":53,"str":"_hygCtx"}}
{"in":55,"str":{"pre":54,"str":"_hyg"}}
{"in":56,"num":{"i":17,"pre":55}}
{"in":57,"str":{"pre":45,"str":"Core"}}
{"in":58,"num":{"i":789336685,"pre":57}}
{"in":59,"str":{"pre":58,"str":"_hygCtx"}}
{"in":60,"str":{"pre":59,"str":"_hyg"}}
{"in":61,"num":{"i":18,"pre":60}}
{"app":{"arg":90,"fn":144},"ie":150}
{"app":{"arg":5,"fn":150},"ie":151}
{"ie":152,"lam":{"binderInfo":"default","body":12,"name":61,"type":151}}
{"ie":153,"lam":{"binderInfo":"default","body":152,"name":56,"type":37}}
{"app":{"arg":153,"fn":149},"ie":154}
{"const":{"name":32,"us":[]},"ie":155}
{"app":{"arg":155,"fn":154},"ie":156}
{"app":{"arg":73,"fn":156},"ie":157}
{"const":{"name":34,"us":[1]},"ie":158}
{"app":{"arg":37,"fn":158},"ie":159}
{"app":{"arg":73,"fn":159},"ie":160}
{"app":{"arg":90,"fn":160},"ie":161}
{"app":{"arg":5,"fn":161},"ie":162}
{"app":{"arg":162,"fn":157},"ie":163}
{"ie":164,"lam":{"binderInfo":"default","body":163,"name":35,"type":146}}
{"thm":{"all":[51],"levelParams":[],"name":51,"type":142,"value":164}}
{"in":62,"str":{"pre":12,"str":"casesOn"}}
{"app":{"arg":10,"fn":41},"ie":165}
{"app":{"arg":8,"fn":165},"ie":166}
{"app":{"arg":5,"fn":166},"ie":167}
{"app":{"arg":10,"fn":8},"ie":168}
{"app":{"arg":57,"fn":53},"ie":169}
{"app":{"arg":10,"fn":169},"ie":170}
{"app":{"arg":170,"fn":168},"ie":171}
{"app":{"arg":8,"fn":10},"ie":172}
{"app":{"arg":12,"fn":172},"ie":173}
{"forallE":{"binderInfo":"default","body":173,"name":22,"type":171},"ie":174}
{"forallE":{"binderInfo":"default","body":174,"name":8,"type":167},"ie":175}
{"forallE":{"binderInfo":"implicit","body":175,"name":19,"type":8},"ie":176}
{"forallE":{"binderInfo":"implicit","body":176,"name":7,"type":51},"ie":177}
{"forallE":{"binderInfo":"implicit","body":177,"name":19,"type":5},"ie":178}
{"forallE":{"binderInfo":"implicit","body":178,"name":14,"type":36},"ie":179}
{"const":{"name":21,"us":[2,3]},"ie":180}
{"app":{"arg":122,"fn":180},"ie":181}
{"app":{"arg":57,"fn":181},"ie":182}
{"app":{"arg":10,"fn":182},"ie":183}
{"app":{"arg":5,"fn":183},"ie":184}
{"app":{"arg":8,"fn":184},"ie":185}
{"app":{"arg":12,"fn":185},"ie":186}
{"ie":187,"lam":{"binderInfo":"default","body":186,"name":22,"type":171}}
{"ie":188,"lam":{"binderInfo":"default","body":187,"name":8,"type":167}}
{"ie":189,"lam":{"binderInfo":"implicit","body":188,"name":19,"type":8}}
{"ie":190,"lam":{"binderInfo":"implicit","body":189,"name":7,"type":51}}
{"ie":191,"lam":{"binderInfo":"implicit","body":190,"name":19,"type":5}}
{"ie":192,"lam":{"binderInfo":"implicit","body":191,"name":14,"type":36}}
{"def":{"all":[62],"hints":"abbrev","levelParams":[6,13],"name":62,"safety":"safe","type":179,"value":192}}
{"in":63,"str":{"pre":0,"str":"_test"}}
{"app":{"arg":1,"fn":5},"ie":193}
{"ie":194,"letE":{"body":5,"name":36,"nondep":false,"type":193,"value":143}}
{"app":{"arg":143,"fn":194},"ie":195}
{"app":{"arg":193,"fn":195},"ie":196}
{"const":{"name":51,"us":[]},"ie":197}
{"app":{"arg":194,"fn":197},"ie":198}
{"const":{"name":62,"us":[]},"ie":199}
{"ie":200,"letE":{"body":193,"name":36,"nondep":false,"type":198,"value":199}}
{"ie":201,"letE":{"body":200,"name":36,"nondep":false,"type":143,"value":196}}
{"ie":202,"letE":{"body":201,"name":36,"nondep":false,"type":143,"value":201}}
{"ie":203,"letE":{"body":202,"name":36,"nondep":false,"type":1,"value":1}}
{"thm":{"all":[63],"levelParams":[],"name":63,"type":203,"value":37}}
13 changes: 13 additions & 0 deletions tests/constlevels.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
description: |
Regression test for undefined behavior in `lazy_delta_reduction_step` in the official kernel

In the function `lazy_delta_reduction_step`, the official kernel expects `unfold_definition`
to always succeed. However, if the constant has an incorrect number of level parameters, it
actually fails, which leads to memory corruption in `lazy_delta_reduction_step`.

This test is to check that the official kernel and also other kernels that closely follow the
logic of the official kernel correctly handle this unfolding failure.

The issue in the official kernel was originally reported as https://github.com/leanprover/lean4/issues/10577.
file: tests/constlevels.ndjson
outcome: reject