A curious bug in metamath-exe verification
Matthew House
Some here may be interested in a bug I found in metamath-exe. The underlying issue is a missing overflow check, which I've now reported on GitHub, but one fun consequence is that it can produce false proofs that successfully validate. In particular, the attached file evil.mm contains a "valid" proof of |- ph, assuming nothing but a wff ph hypothesis. The setup is OS-dependent, and I've only tested it to work on my x86-64 Ubuntu 24.04 LTS machine, but it likely works as written on other 64-bit glibc-based Linux distros.
$ cat evil.mm$c wff $.
$c |- $.
$v ph $.
wph $f wff ph $.
$( A benign ` wff ` inference. $)
ww $p wff ph $=
( ) A $.
$( An evil ` |- ph ` proof. $)
evil $p |- ph $=
( ww ) ABBBBBBVYVUXUUXYWYVVUUVUXWYVWYVYWG $.
$ ./metamath
Metamath - Version 0.199.pre 29-Jan-2022 Type HELP for help, EXIT to exit.
MM> read evil.mm /verify
Reading source file "evil.mm"... 224 bytes
224 bytes were read into the source buffer.
The source has 6 statements; 0 are $a and 2 are $p.
0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
..................................................
All proofs in the database were verified in 0.00 s.
No errors were found.
MM> show proof evil /all
1 wph=wph $f wff ph
2 wph=ww $p wff ph
3 wph=ww $p wff ph
4 wph=ww $p wff ph
5 wph=ww $p wff ph
6 wph=ww $p wff ph
7 wph=ww $p wff ph
8 evil=evil $p |- ph
MM> quit
That is to say, multiple separate implementations really are important if you want to confidently verify a database file. In comparison, mmverify.py is written in Python, which has no integer overflows; metamath-knife explicitly checks for overflow; and mmj2 is similarly missing an overflow check, but at worst it can only create a disguised ? step or premature end-of-proof.
I'm now somewhat curious, have there been similar bugs in the past, affecting verification in metamath-exe or other implementations?
Matthew House