Veil framework discussion thread

Stream: general

[George Pîrlea]

Discussion thread for Veil. See the announcement at #announce > Veil: A Framework for Automated and Interactive Verification

[Shreyas Srinivas]

Why is proof reconstruction turned off by default?

[Shreyas Srinivas]

More specifically, how is the SMT's output checked when there is no proof reconstruction?

[George Pîrlea]

@Shreyas Srinivas When proof reconstruction is off, the SMT solver's output is simply trusted rather than checked. This is similar to existing non-foundational verifiers. We keep it off by default since it's quite slow (>5x slowdown) and currently a bit brittle for the goals we generate (we'll report this upstream to lean-smt). We're hoping to be able to change this default in the future, though.

[Shreyas Srinivas]

okay, so the TCB is Lean's kernel + SMT solver (z3/cvc5?)

[George Pîrlea]

Yes. We use CVC5 by default and fall back to Z3 when the former times out. (This is configurable using set_option veil.smt.solver and veil.smt.retryOnUnknown)

[Shreyas Srinivas]

@Sasha Rubin and @Ashvni Narayanan you might be interested in this

[Shreyas Srinivas]

Related question : how well can SMT discharged goals (for want of a better word) mix with manually proved goals? I am asking this because being able to take SMT proofs at face value means that you don’t necessarily have a sorry free theorem for it from lean’s perspective.

[Shreyas Srinivas]

Turning on proof reconstruction should let you add theorem declarations with proofs to the environment and let you freely mix autoproved theorems with manually proved theorems.

[George Pîrlea]

It's very easy to mix goals proven interactively and those proven with SMT. All goals that Veil generates are just standard Lean theorems that we add to the environment. For example, instead of using the #check_invariants command, you can do #check_invariants? and see exactly what's being proven behind the scenes.

If you really care about not trusting SMT solvers, you really should use Veil with proof reconstruction at all times, yes. But, again, as proof reconstruction improves in upstream projects, we're hoping to change the default.

[George Pîrlea]

I'd be curious to hear if you have specific projects you'd want to try Veil on where this is a major concern.

[Shreyas Srinivas]

This isn’t about trust. If you generated a lean theorem but no proof, what are you actually assigning to this declaration?

[Shreyas Srinivas]

Is it an assumption that is added to the environment?

[Shreyas Srinivas]

Like adding a variable statement in a section?

[George Pîrlea]

It's a theorem whose body is by sorry.

[Shreyas Srinivas]

Ah, so a lean project using Veil won’t be sorry free

[Shreyas Srinivas]

The problem with this approach is that a large project would have a number of theorems, many auto generated by lean and some handwritten. When reviewing such a project it won’t be sufficient to look for occurrences of sorry by using #print_axioms or checking the output of lake build. One would have to manually check that the only sorrys are coming from the SMT generated proofs

[Shreyas Srinivas]

Also I think #print axioms will show sorryAx as one of the axioms but won’t be able to tell you whether the sorry is one of the by sorrys generated by Veil or a sorry inserted manually during the proof development and forgotten

[George Pîrlea]

Ah, that's a good point. Thank you! We should introduce our own version of sorry such that it's easier to distinguish in #print axioms. (I think lean-auto does something like this.)

But just to point it out, it's difficult to miss that Veil without proof reconstruction uses sorry — there are warnings printed during compilation similar to how Lean sorry works. For instance, #check_invariants in the tutorial prints "Trusting the SMT solver for 12 theorems."

[Shreyas Srinivas]

Okay that’s a good sign. Nevertheless from a UX perspective sorry comes with some bells and whistles (for example yellow squiggly lines) and some output lines in the output of lake build. This makes no distinction between user inserted and automatically inserted sorries. As someone writing proofs, this will be a nightmare for me to make sure I haven’t left any forgotten sorries lying around

[Shreyas Srinivas]

A slightly better idea might be to replicate the axiom command, let’s call it smt_assumption and replicate #print_axioms for this, calling it #print SMT assumptions

[Shreyas Srinivas]

The latter takes a theorem and prints out the smt_assumptions it uses

[George Pîrlea]

Maybe I'm misunderstanding, but you still get all of this (the squiggly lines, etc.) with Veil. You always have to issue a command (e.g. #check_invariants) to generate and prove theorems — it doesn't do it "behind your back". Here's what it looks like:

image.png

[Shreyas Srinivas]

In a large proof development I don’t see how it will be easy to separate the use of smt theorems from user theorems containing sorries. I am thinking about this from a debugging perspective.

[Shreyas Srinivas]

In my suggestion about SMT_assumption, you could also just define an SMT_assumption attribute, tag all the generated theorems with this attribute. The #print SMT assumptions <theorem> command simply prints all uses of theorems with this attribute, in a manner similar to #print axioms

[Shreyas Srinivas]

That way, even if someone turns on proof reconstruction, one can track the uses of SMT proven theorems. only the by sorry part needs to be replaced by the proof as is happening now (I guess)