search

leanprover-community / lean-auto

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

Zero-width bitvectors #11

Open shigoel opened 11 months ago

shigoel commented 11 months ago

Zero-width bitvectors are not supported by the Fixed-Size Bitvector theory in SMT, but Std.BitVec allows them. This can cause interesting issues. Here is a motivating example.

The following is a theorem in Lean: ∀ (x : BitVec 8), x ++ (Std.BitVec.ofNat 0 0) = x

When auto is used to prove the theorem above, (Std.BitVec.ofNat 0 0) is translated to a 1-bit SMT bitvector, and a sort mismatch error is obtained from the solver (log below).

Perhaps a simplification rule is needed to tackle this case?

[auto.smt.printCommands] (declare-sort |Empty| 0)
[auto.smt.printCommands] (define-fun |nsub| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|>=| |x| |y|) (|-| |x| |y|) 0))
[auto.smt.printCommands] (define-fun |itdiv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|div| |x| |y|) (|-| (|div| (|-| |x|) |y|)))))
[auto.smt.printCommands] (define-fun |itmod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|mod| |x| |y|) (|-| (|mod| (|-| |x|) |y|)))))
[auto.smt.printCommands] (define-fun |iediv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) 0 (|div| |x| |y|)))
[auto.smt.printCommands] (define-fun |iemod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|mod| |x| |y|)))
[auto.smt.printCommands] (declare-fun |smti_0| () (_ BitVec 8))
[auto.smt.printCommands] (assert (! (|not| (|=| (|concat| |smti_0| #b0) |smti_0|)) :named valid_fact_0))
[auto.smt.result] z3 produces unexpected check-sat response
     (|error| "line 10 column 55: Sorts (_ BitVec 9) and (_ BitVec 8) are incompatible")