comparator

Stream: lean4

[Jason Gross]

Has anyone gotten the comparator to work when Quot.sound is involved? I am trying to figure out whether uncaught exception: (kernel) unknown constant 'Eq' is a bug in the compartor, lean4export, or lean4checker

[Henrik Böving]

I've previously used comparator to check results from Mathlib so it is certainly possible yes, lean4export also manages to correctly export Quot.sound from the module based from a cursory look at its output so I would suspect that this is an issue with the replay system from lean4checker. Though also a very specific issue because only in the very minimal configurations that you use does Eq not get added through some other mean before Quot.sound pops up eventually.

[Henrik Böving]

CC @Kim Morrison if something in the lean4checker codebase regarding dependencies of axioms comes to mind.

[Kim Morrison]

Sorry, can't think of anything. I'm not sure what "the very minimal configurations that you use" is referring to, but maybe it is out of the intended scope of these tools? :-)

[Henrik Böving]

It very much is in scope. It refers to the very small theorem that Jason is trying to check:

theorem mp : ∀ (P Q : Prop), P → (P → Q) → Q :=
  fun _ _ hp hpq => hpq hp

Comparator will load both the theorem as well as all of the allowed axioms (including Quot.sound) and their dependencies into lean4checker. It appears that usually Eq happens to be addded before Quot.sound through some other dependency path but in this specific situation that does not end up being the case.

[Henrik Böving]

At least when I print both the output from lean4export and the list of declarations that comparator sends to lean4checker I can clearly see that Eq is being sent

[Kim Morrison]

I see. I was wondering (since Quot.sound is involved everywhere) if perhaps there was some alternative prelude being used.

[Kim Morrison]

Repro at https://github.com/kim-em/scratch-comparator-unknown-constant

[Kim Morrison]

Fix at https://github.com/leanprover/lean4checker/pull/79

[Kim Morrison]

@Henrik Böving, if you could update the require statement in comparator?

[Henrik Böving]

Will do

[Henrik Böving]

@Kim Morrison do you want to update the version tag or do I just put the raw commit here?

[Kim Morrison]

Is it okay to just use a raw commit until we release the v4.27.0 or v4.28.0-rc1 tags?

[Kim Morrison]

Alternatively, we could add a v4.27.0-rc1+patch1 tag

[Henrik Böving]

Sure, just wanted to make sure

[Sorrachai Yingchareonthawornchai]

I tried to use a comparator, but it throws an exception on this theorem statement.

 theorem nonzero (n t : ℕ) [NeZero t] :
 0 < t := sorry

uncaught exception: Const not found in target 'IsLeftRegular'

However, it works fine when I remove [NeZero t] in the statement. Any advice?

[Henrik Böving]

Can you please provide a full #mwe here

[Sorrachai Yingchareonthawornchai]

something like this

[Sorrachai Yingchareonthawornchai]

I have this in the config file. The Challenge.lean and Solution.lean are identical to the mwe above.
{
"challenge_module": "Challenge",
"solution_module": "Solution",
"theorem_names": ["nonzero"],
"permitted_axioms": [
"propext", "Quot.sound", "Classical.choice", "sorryAx"
],
"enable_nanoda": false
}

[Sorrachai Yingchareonthawornchai]

When I try to debug in Compare.lean, I found that the following condition is true (when I insert it in line 43) , which triggers an exception.

(← read).solution.constMap[target]? = none ∧ (← read).challenge.constMap[target]? = none

[Henrik Böving]

I think this is most likely going to be an issue with the new parser that we introduced

[Sorrachai Yingchareonthawornchai]

I see. Thanks.

[Henrik Böving]

@Sorrachai Yingchareonthawornchai fixed in https://github.com/leanprover/comparator/pull/16 it was a slightly overzealous behavior that got uncovered because lean4export got more careful with what actually needs to be exported.

[Sorrachai Yingchareonthawornchai]

Thank you very much

[Sorrachai Yingchareonthawornchai]

A quick question. Is it possible to run the comparator without sandboxing (e.g., with an additional flag)?

[Henrik Böving]

No that is not possible. Why do you need that?

[James E Hanson]

Is sandboxing the only thing stopping it from working on Windows (and maybe macOS)?

[James E Hanson]

Everything else is compiled from Lean code, so it should be, right?

[Henrik Böving]

My first intuition would be yes

[James E Hanson]

You said before that comparator is basically where you want it to be feature-wise, but I had wondered in the past whether it might make sense to split it into something that produces an export JSON from a sandboxed environment and something that compares an export JSON against a goal.

I guess one issue with this approach might be that the export format seems to be pretty space inefficient?

[Austin Hatfield]

Hey @Henrik Böving ! I'm trying to integrate Comparator as the final verification gate for my AI benchmark (asiprize.com) which runs models against the 297 unsolved conjectures in DeepMind's formal-conjectures repo. The repo pins Lean 4.22.0 and Comparator is on 4.29.0-rc1 is there a path to running Comparator against proofs built on 4.22.0 or do I need to wait for the repo to upgrade?

[Henrik Böving]

You can try in principle to just set the toolchain to 4.22 but I wouldn't rely on it. Waiting for things to upgrade is likely the better way. That said if they are pinned to 4.22 they haven't updated in half a year by now so maybe this requires some pressure from your side rather than just waiting.

[Floris van Doorn]

formal-conjectures is on v4.27.0, so it's on the latest stable as of yesterday...

[Yaël Dillies]

Yes, we merged the bump PR a few hours ago

[Floris van Doorn]

Oh, merging without squashing gives the misleading impression that the bump happened multiple weeks ago.

[Yaël Dillies]

Sorry for this. We had to not squash due to a limitation of our internal tools

[Austin Hatfield]

Thank you Floris, Yael, Henrik - the version bump is exactly what I needed for the v2 benchmark. Really appreciate the quick responses!

[Sorrachai Yingchareonthawornchai]

Henrik Böving said:

No that is not possible. Why do you need that?

Since I already have a sandbox (docker) I'm running it in and landrun sandbox adds unnecessary complexity?

[Henrik Böving]

The sandbox of comparator is not meant to protect your system from malicious code. It's meant to protect itself from exploits. For example, suppose you are running in dual kernel mode with nanoda and the built-in kernel. An attacker could simply add a meta program to their file that replaces the nanoda binary with one that always says accept, thus reducing the level of trust provided by Comparator. Thus giving up on the sandboxing functionality is not really negotiatable. If anything the sandbox is still too loose.

[Henrik Böving]

In general, the whole architecture of Comparator is built around defense in depth. Even if you manage to find a way to break assumptions that were made during development, it should be as hard as possible to turn these issues into a functioning exploit.