search

isabelle-prover / proving-contest-backends

"proving-contest"-backends for several theorem provers
MIT License
12 stars 5 forks source link

Disable lean global notation in submission #22

Closed kappelmann closed 5 years ago

kappelmann commented 5 years ago

Lean allows global notation overrides, which let's the user manipulate the check file. For example, the following submission

notation `false` := true

theorem soundness_bug : false := trivial

makes this check pass:

import .submission

lemma you_broke_it : false := soundness_bug

Possible fix: disallow notation in check files.

maxhaslbeck commented 5 years ago

0706159717a4484688198becd13247f37b7f8a73 has a quick fix, blacklisting "notation", do you think this is too eager? would you prefer some other method of disallowing notation in the submission file? are there other keywords that should be blacklisted?

in section 2 of http://www21.in.tum.de/~haslbema/documents/Haslbeck_Wimmer-Competitive_Proving_for_Fun.pdf we describe some other "break the system" solutions that may be replayed in Lean? the list of blacklisted keywords for Isabelle can be found here: https://github.com/maxhaslbeck/proving-contest-backends/blob/0706159717a4484688198becd13247f37b7f8a73/Isabelle/poller_isa.py#L23-L64

kappelmann commented 5 years ago

Notation cheats can be prevented by defining the noation in defs.lean and importing defs.lean before submission.lean in check.lean. Cf notes here.