feat: Use hashmap in bit heap

[osmanyasar05]

This PR modifies the bit heap structure so that it now uses hash maps, instead of holding a list of lists.

For now, the columns still hold a List, but we might also change those to use hashsets/arrays.

[bollu]

Looking good so far! I requested changes to (a) fix the asymptotics of insert, and (b) use Circuit.const false as a default value, and (c) to make remove robust to the index not existing. This should help make the library API feel nicer to use.

[bollu]

We're getting there. I request a more idiomatic way of writing get and removeBit so that they'll be easier to prove.

[bollu]

Almost! I requested a change to addBit where I noticed that we don't compute a index uniquely for a column. I'm happy with everything else

[bollu]

Great, can you now split this into multiple files? Example, BitHeap/Basic.lean, BitHeap/FullAdder.lean, BitHeap/Examples.lean, and a toplevel BitHeap.lean that imports all of these, so that running a lake build builds everything? Follow veir style

[bollu]

@osmanyasar05 when we change from List to HashSet, the API will no longer have an index associated to each column. So, maybe we should anticipate this, and change our API to make use of List.insert and List.erase? Then, addBit will have type addBit (column : Nat) (c : Circuit) (h : BitHeap) : BitHeap := ... and similarly, eraseBit (column : Nat) (c : Circuit) := .... Does that make sense to you?

[bollu]

LGTM, let's merge it, and perform the refactor in the next patch as suggested by @osmanyasar05 . the eventual goal should be to have all of this sorry-free!

[bollu]

BTW, for the imports, what one would do is to have a file called DatapathVerification/BitHeap.lean that imports everything inside the subfolder.

[osmanyasar05]

BTW, for the imports, what one would do is to have a file called DatapathVerification/BitHeap.lean that imports everything inside the subfolder.

I was using the Basic.lean for that purpose, if that's what you mean?