ofReduceBool and all that

Stream: Equational

[Mario Carneiro]

native_decide is just a wrapper around ofReduceBool

[Mario Carneiro]

currently the design of axiom tracking around compiler things means that it's not just "we trust the compiler", it's really trusting an unbounded set of extensions to the compiler

[Mario Carneiro]

which makes it pretty much useless from a trust perspective unless you are only checking that it isn't present

[Mario Carneiro]

@[csimp] is one of those extension mechanisms

[Shreyas Srinivas]

And bvdecide also trusts the compiler iirc

[Mario Carneiro]

@[csimp], @[implemented_by] and @[extern] all get laundered through ofReduceBool

[Mario Carneiro]

bv_decide also uses ofReduceBool

[Mario Carneiro]

Fun fact, there is also ofReduceNat but I think no one has ever used it

[Shreyas Srinivas]

It seems the more efficient a tactic needs to be, the more its author is willing to trust the compiler.

[Mario Carneiro]

that's kind of a necessity thing. Some tasks are just too big to be done using the 'slow trusted' tools we have

[Mario Carneiro]

But you can get pretty far with kernel computation if you use it right

[Mario Carneiro]

bv_decide is basically not a tactic you or I will ever have cause to use

[Henrik Böving]

Mario Carneiro said:

bv_decide also uses ofReduceBool

But the possible set of csimp/implemented_by/extern that apply to bv_decide are limited to what's available in core and you can review those. So I would argue the set is by no means unbounded in this case and if you trust the attributes in core it is indeed only the compiler you have to trust.

[Mario Carneiro]

@Henrik Böving It uses ofReduceBool, which means it makes post hoc verification very difficult because #print axioms shows it as a use of ofReduceBool and it's not very easy to determine whether a proof containing ofReduceBool got it because bv_decide put it there or something else did

[Mario Carneiro]

It would be better if it used ofReduceBoolForBVDecide

[Mario Carneiro]

Or more to the point, the argument to ofReduceBool (which is always a constant declaration) needs to be marked as "vetted by bv_decide maintainers"

[Mario Carneiro]

i.e. it always boils down to "we need better tracking for ofReduceBool"

[Mario Carneiro]

because the worst part is that you can't look at the term itself to be executed to determine whether it is something bv_decide would have produced

[Mario Carneiro]

If the argument involves saying "I know it's fine because I called the bv_decide function and this definition popped out" then that means you aren't just validating that the proof object is correct, you have to trust that the execution process itself hasn't been compromised. This implicates the entire elaborator and all the rest of lean

[Henrik Böving]

Mario Carneiro said:

It would be better if it used ofReduceBoolForBVDecide

I don't think that would help? Every other person could also use that

[Mario Carneiro]

You're right. That would make tracking easier but not in an adversarial scenario

[Mario Carneiro]

Here's an illustration of the issue:

import Lean

section black_magic
def lie : Bool := false
-- local to destroy the evidence of tampering
@[local csimp] unsafe def lie_eq : lie = true := lie_eq
def prog : Bool := lie

theorem contra : False := nomatch Lean.ofReduceBool prog true rfl
macro_rules | `(tactic| bv_decide) => `(tactic| exact contra)
end black_magic

-- Proof by bv_decide
theorem foo : False := by bv_decide

-- axioms check out
#print axioms foo -- 'foo' depends on axioms: [Lean.ofReduceBool]

-- Even if we poke at each definition evaluated by an `Lean.ofReduceBool` we see nothing weird
#print axioms prog -- 'prog' does not depend on any axioms
#print prog -- def prog : Bool := lie
#print lie -- def lie : Bool := false
open Lean
#eval return Compiler.hasCSimpAttribute (← getEnv) `prog -- false
#eval return Compiler.hasCSimpAttribute (← getEnv) `lie -- false
#eval do logInfo m!"{(IR.findEnvDecl (← getEnv) `prog).get!}"
-- def prog : u8 :=
--   let x_1 : u8 := 1;
--   ret x_1

[Shreyas Srinivas]

I had the same criticism of the Veil tool. In their default setting, they simply insert their SMT verified theorems as theorem statements with a sorry. This doesn't scale well in a large proof development, since it requires extra work to track down where the sorries are coming from, especially since the tool inserted theorems don't show up in the editor.

[Henrik Böving]

Shreyas Srinivas said:

I had the same criticism of the Veil tool. In their default setting, they simply insert their SMT verified theorems as theorem statements with a sorry. This doesn't scale well in a large proof development, since it requires extra work to track down where the sorries are coming from, especially since the tool inserted theorems don't show up in the editor.

bv_decide is very different though, with the SMT stuff you trust arbitrary results from an SMT solver. With bv_decide assuming that all implemented_by/csimp in core are fine (which, given the fact they are one of the most well tested code we have they probably are) and the compiler is fine it is guaranteed to be correct, there is no trusting the SAT solver or something like that.

[Mario Carneiro]

Shreyas Srinivas 's point is about the non-adversarial setting. In a large project there can be bad uses and good uses of sorry and ofReduceBool, and even if one accepts that bv_decide is a "good use" it's still blending into the crowd

[Mario Carneiro]

I suspect that bv_decide is using ofReduceBool more than necessary; I'm sure that large SAT certificates need it but small ones can be evaluated in the kernel

[Shreyas Srinivas]

It's a UX problem. I want to be able to isolate sorrys and ofReduceBools that are generated by specific tools from ones I write and want to remove later.

[Mario Carneiro]

(keep in mind that a significant fraction of calls to linarith and omega are things like x < x + 1 - there is value in optimizing for the small case)

[Henrik Böving]

That's not the only reason bv_decide uses ofReduceBool. It also needs to demonstrate to the kernel that the generated CNF is equivalent to the actual reflected problem which it does by rerunning bitblasting as part of the ofReduceBool invocation. Bitblasting being fast heavily relies on HashMaps, computed_field hash codes etc. You can't just evaluate the bitblaster with kernel reduction.

[Mario Carneiro]

When it's a hashmap with one element in it it's really not a problem

[Mario Carneiro]

unless it literally can't be evaluated of course (because of some irreducible or opaque thing)

[Henrik Böving]

Mario Carneiro said:

When it's a hashmap with one element in it it's really not a problem

There is literally up to hundreds of thousands of elements, the HashMap is linear in the DAG size of the produced circuit

[Sébastien Gouëzel]

But aren't there many concrete use cases where the problem is really simple and there are less than 10 elements? Most of the concrete uses cases, maybe? For a different example, I'm pretty sure most omega uses in mathlib use only one or two inequalities in the context, although omega is powerful enough to handle much more complicated situations.

[Mario Carneiro]

(everyone has permissions to move topics)

[Henrik Böving]

Sébastien Gouëzel said:

But aren't there many concrete use cases where the problem is really simple and there are less than 10 elements? Most of the concrete uses cases, maybe? For a different example, I'm pretty sure most omega uses in mathlib use only one or two inequalities in the context, although omega is powerful enough to handle much more complicated situations.

no, bv_decide builds a circuit from the BitVec statements, there are necessarily linear and quadratic constructions in length of the bit width happening. I've barely seen problems that people practically solve with bv_decide that are below at least hundreds of circuit nodes being worked in the HashMap and not just being solved in pre processing (which does not use axioms). So even if it is possible adding this feature is useful to maybe .1 percent of the users and thus not worth the effort.

[Daniel Weber]

Mario Carneiro said:

(everyone has permissions to move topics)

Not to another channel

[Mario Carneiro]

right now figuring out what percent of users need hard instances means dividing by zero, if we take usage in batteries and mathlib as the metric

[Mario Carneiro]

(which makes it really off topic for this stream. No one here will ever use this tactic)

[Shreyas Srinivas]

I can move the messages, but because zulip doesn't give you the option to exactly select which messages to move, I will have to salami slice this thread, suffix by suffix, moving messages back and forth until every message is in the right thread

[Shreyas Srinivas]

I think I got everything. The discussions about the toolchain bump are in #Equational > Bump to v20.0-rc5 and the ofReduceBool discussion is here

[Henrik Böving]

Mario Carneiro said:

right now figuring out what percent of users need hard instances means dividing by zero, if we take usage in batteries and mathlib as the metric

There are a couple of research and industrial users outside of mathlib and batteries though. And with all the example problems I've seen from them, unless there is just a rewrite to solve the problem the circuit is always in the 100s of nodes up to millions of nodes.

So I'd say as long as you are not just dealing with a BitVec 8 and a problem that's not doable with rewriting the circuit will just end up with at least 100s of nodes, so the in kernel evaluation will not scale for the specific workload that bv_decide puts on it as it makes heavy use of HashMap, Array, String and ByteArray. If these tiny low bit-width instances arise, it' likely more reasonable to just case split that part, instead of trying to figure out how to run a tool like bv_decide completely in the kernel when almost all users we see work on medium to large instances. Alternatively a different tool that can deal with these smaller problems and be specifically optimized for the kernel could exist of course but I'm not seeing any demand for it so far.

[Henrik Böving]

Maybe we could specialize print axioms for ofReduce* to print the term (or given that it only works on closed decls the term in the contained definition) that is being reduced?

[Henrik Böving]

Mario Carneiro said:

It would be better if it used ofReduceBoolForBVDecide

At least unlike this part, this can't cheat in an adversarial scenario (of course assuming sane environment yadda yadda)

[Mario Carneiro]

Henrik Böving said:

Maybe we could specialize print axioms for ofReduce* to print the term (or given that it only works on closed decls the term in the contained definition) that is being reduced?

See my example above, which is designed to foil every post hoc rationalization method available, including this