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 <https://github.com/metamath/metamath-exe/issues/184>, 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
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/80b230a1-e247-4096-97cb-01ab1a114fb7n%40googlegroups.com.
$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 $.
