leanprover-community / lean-auto

Experiments in automation for Lean
Apache License 2.0
70 stars 12 forks source link

LT and LE for bitvectors #10

Closed shigoel closed 9 months ago

shigoel commented 10 months ago

The following is a theorem, but worryingly, auto reported a counterexample.

theorem auto_bitvec_inequality_test (i j max : Std.BitVec 64)
  (h0 : i < max) (h1 : j <= max - i) (h2 : 0#64 < j) :
  (max - (i + j)) < (max - i) := by
  auto

From the generated SMT commands (pasted in at the end of this message), one can see that the issue was that < and <= were defined as uninterpreted SMT functions, and not in terms of bvult and bvule, as I had expected.

This was inconsistent with + and -, which were indeed resolved to bvadd and bvneg.

 (declare-sort |Empty| 0)
 (define-fun |nsub| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|>=| |x| |y|) (|-| |x| |y|) 0))
 (define-fun |itdiv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|div| |x| |y|) (|-| (|div| (|-| |x|) |y|)))))
 (define-fun |itmod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|mod| |x| |y|) (|-| (|mod| (|-| |x|) |y|)))))
 (define-fun |iediv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) 0 (|div| |x| |y|)))
 (define-fun |iemod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|mod| |x| |y|)))
 (declare-fun |smti_0| () (_ BitVec 64))
 (declare-fun |smti_1| () (_ BitVec 64))
 (declare-fun |smti_2| ((_ BitVec 64) (_ BitVec 64)) |Bool|)
 (assert (! (|smti_2| |smti_0| |smti_1|) :named valid_fact_0))
 (declare-fun |smti_3| () (_ BitVec 64))
 (declare-fun |smti_4| ((_ BitVec 64) (_ BitVec 64)) |Bool|)
 (assert (! (|smti_4| |smti_3| (|bvadd| |smti_1| (|bvneg| |smti_0|))) :named valid_fact_1))
 (assert (! (|smti_2| #b0000000000000000000000000000000000000000000000000000000000000000 |smti_3|) :named valid_fact_2))
 (assert (! (|not| (|smti_2| (|bvadd| |smti_1| (|bvneg| (|bvadd| |smti_0| |smti_3|))) (|bvadd| |smti_1| (|bvneg| |smti_0|)))) :named valid_fact_3))

[auto.smt.result] z3 says Sat, model:
    ((|define-fun| |smti_0| () (|_| |BitVec| 64) 0) (|define-fun| |smti_3| () (|_| |BitVec| 64) 18446744073709549568) (|define-fun| |valid_fact_3| () |Bool| (|let| ((|a!1| (|smti_2| (|bvadd| |smti_1| (|bvneg| (|bvadd| |smti_0| |smti_3|))) (|bvadd| |smti_1| (|bvneg| |smti_0|))))) (|not| |a!1|))) (|define-fun| |valid_fact_2| () |Bool| (|smti_2| 0 |smti_3|)) (|define-fun| |valid_fact_1| () |Bool| (|smti_4| |smti_3| (|bvadd| |smti_1| (|bvneg| |smti_0|)))) (|define-fun| |valid_fact_0| () |Bool| (|smti_2| |smti_0| |smti_1|)) (|define-fun| |smti_1| () (|_| |BitVec| 64) 262160) (|define-fun| |smti_4| ((|x!0| (|_| |BitVec| 64)) (|x!1| (|_| |BitVec| 64))) |Bool| |true|) (|define-fun| |smti_2| ((|x!0| (|_| |BitVec| 64)) (|x!1| (|_| |BitVec| 64))) |Bool| (|ite| (|and| (|=| |x!0| 264208) (|=| |x!1| 262160)) |false| |true|)))
shigoel commented 10 months ago

Here is an attempt to re-state the formula in terms of Std.BitVec.ult and Std.BitVec.ule to get around the issue:

theorem auto_bitvec_inequality_test_1 (i j max : Std.BitVec 64)
   (h0 : Std.BitVec.ult i max) (h1 : Std.BitVec.ule j (max - i))
   (h2 : Std.BitVec.ult 0#64 j) :
   Std.BitVec.ult (max - (i + j)) (max - i) := by
   auto

Unfortunately, auto ran for several minutes, and produced the following: [auto.smt.result] z3 produces unexpected check-sat response |timeout|

However, when I independently submitted the SMT file to z3 (version 4.11.2 - 64 bit), it was solved in ~0.06s.

Generated SMT file:

 (declare-sort |Empty| 0) 
 (define-fun |nsub| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|>=| |x| |y|) (|-| |x| |y|) 0)) 
 (define-fun |itdiv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|div| |x| |y|) (|-| (|div| (|-| |x|) |y|))))) 
 (define-fun |itmod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|mod| |x| |y|) (|-| (|mod| (|-| |x|) |y|))))) 
 (define-fun |iediv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) 0 (|div| |x| |y|))) 
 (define-fun |iemod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|mod| |x| |y|))) 
 (declare-fun |smti_0| () (_ BitVec 64)) 
 (declare-fun |smti_1| () (_ BitVec 64)) 
 (assert (! (|=| (|bvult| |smti_0| |smti_1|) |true|) :named valid_fact_0)) 
 (declare-fun |smti_2| () (_ BitVec 64)) 
(assert (! (|=| (|bvule| |smti_2| (|bvadd| |smti_1| (|bvneg| |smti_0|))) |true|) :named valid_fact_1)) 
 (assert (! (|=| (|bvult| #b0000000000000000000000000000000000000000000000000000000000000000 |smti_2|) |true|) :named valid_fact_2)) 
 (assert (! (|not| (|=| (|bvult| (|bvadd| |smti_1| (|bvneg| (|bvadd| |smti_0| |smti_2|))) (|bvadd| |smti_1| (|bvneg| |smti_0|))) |true|)) :named valid_fact_3)) 
PratherConid commented 10 months ago

I cannot reproduce [auto.smt.result] z3 produces unexpected check-sat response |timeout|, and instead got a crash in the Lean server. According to the behaviour of lean-auto on my machine, there are three separate issues:

  1. The signature of fun (a b : BitVec 64) => a <= b is different from @Std.BitVec.ule 64, so auto does not recognize them as the same. To fix this, more simplification rules are needed. This is a more involved issue and I'll fix it later.
  2. The Sexp parser in Lean-auto is too slow and it times out when parsing the proof (which is ~30 million bytes long) of your second example. I've added an option auto.smt.rconsProof to temporarily skip proof parsing, which should have no negative impact on the current behaviour of lean-auto.
  3. The trace[auto.smt.result] ...{proof}... causes Lean to crash, presumably because proof is too long. I've splitted auto.smt.result into auto.smt.result, auto.smt.proof and auto.smt.model.

Hopefully this will make the second example work on your machine.

shigoel commented 10 months ago

Thank you, @PratherConid! Indeed, the second example (the one with Std.BitVec.ult and Std.BitVec.ule) does work for me after turning off proof.