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