Binary Decision Diagrams

Stream: Is there code for X?

[Riya Gupta]

I'm trying to write some proofs about hardware using Lean -- and was wondering if there are implementations which already exist

[Henrik Böving]

No, there does exist a formalization about bit vectors as BitVec and booleans as Bool together with a lot of theory and tactic support like bv_decide, bv_omega and simp though.

Is there a specific use case that requires BDDs which you think would not be covered by these?

[Malvin Gattinger]

I am also interested in BDDs, for example how they are used to encode relations for symbolic model checking. Maybe this is a naive question, but how are bitvectors and Bool a replacement for them? BDDs allow to encode arbitrary Boolean functions and while their worst-case compleity is just as bad, they are often much smaller than the equivalent truth table.

[Riya Gupta]

Malvin Gattinger said:

I am also interested in BDDs, for example how they are used to encode relations for symbolic model checking. Maybe this is a naive question, but how are bitvectors and Bool a replacement for them? BDDs allow to encode arbitrary Boolean functions and while their worst-case compleity is just as bad, they are often much smaller than the equivalent truth table.

To this extent, has anyone looked into wrapping a pre-existing BDD library and making it work for Lean?

[Malvin Gattinger]

Just to also mention it in this older but public thread, I am now supervising a student who is implementing BDDs in Lean (from scratch, i.e. not by wrapping an existing non-Lean library). The goal is to also have correctness proofs. Work in progress can be found at https://github.com/eshelyaron/lean4-bdd

[Malvin Gattinger]

I am happy to report that the masters thesis by Eshel Yaron is now publicly available at https://eprints.illc.uva.nl/id/eprint/2377/ - It describes in detail the implementation of the BDD library available here (same link as above). The doc-gen for the "end user" module Bdd.BDD is also available at https://eshelyaron.com/man/lean4/Bdd/BDD.html
The library is in principle ready for use, though there are still two internal lemmas with sorry - it's of course our next goal to finish those.