new way to break the system in Lean

[fpvandoorn]

See submission 3181:

universe variable u

def «quot.mk» {α : Sort u} (r : α → α → Prop) (a : α) : α := a

axiom «quot.sound» : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → «quot.mk» r a = «quot.mk» r b

theorem soundness_bug : false :=
begin
  have : tt = ff := @«quot.sound» _ (λ _ _, true) _ _ trivial,
  contradiction
end

The reason it works is that Leanchecker prints «quot.sound» in exactly the same way as the trusted axiom quot.sound.

Possible fixes:

• Change leanchecker so that it prints the French quotes «» for "illegal" names like this.
• Run #print axioms within Lean, and check that there are only 3 declared axioms in the output (this will disallow all submissions that add another axiom, even if that axiom is not used).
• Use another external type checker that does distinguish «quot.sound» and quot.sound

[fpvandoorn]

Oh, #print axioms is problematic:

open lean lean.parser tactic interactive

@[user_command] meta def foo (_ : parse $ tk "#print axioms") : parser unit :=
do _ ← optional ident,
trace "quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
classical.choice : Π {α : Sort u}, nonempty α → α
propext : ∀ {a b : Prop}, (a ↔ b) → a = b"

axiom innocent : false

def soundness_bug : false := innocent

#print axioms
#print axioms soundness_bug
#print axioms nat

[kappelmann]

I'd like to have leanchecker to print the actual name. Are there any other problematic characters you are aware of? Or, even better, are you already aware of the critical piece of code in the leanchecker that is responsible for the name printing?

[fpvandoorn]

This line is responsible for the name:
https://github.com/leanprover-community/lean/blob/master/src/checker/checker.cpp#L41

Recall that names in Lean are basically lists of strings:

inductive name
| anonymous  : name
| mk_string  : string → name → name
| mk_numeral : unsigned → name → name

When I write axiom quot.sound the name becomes mk_string "sound" (mk_string "quot" anonymous), but when writing axiom «quot.sound» the French quotes are removed, but we get mk_string "quot.sound" anonymous. So the test should be "if a component contains a ., print it using French quotes".

There should be no other problematic characters, other than the .

[kappelmann]

The opened issue was closed, but I still think there is another problem. I commented on leanprover-community/lean#114