Bitcoin Lean Project

Stream: new members

[Nadav Kohen]

Hello everyone! I am a software engineer and maintainer of the Scala library bitcoin-s. I have had some previous experience in Agda and just finished all of the exercises in the (Lean) tutorials project. I am interested in starting a github repo called lean-bitcoin where I want to construct Bitcoin's basic data structures (transactions, spending conditions, etc.) with the goal of implementing protocols such as DLC construction and proving the fidelity of those implementations, including correctness/bounds on fees and the like, and maybe even generating test vectors for other more efficient implementations (in other languages).

I won't be needing any help with any Bitcoin-related knowledge, but I would really appreciate advice and help in setting up a lean project and high-level design and structuring of that project and some other more general getting-started help.

Would anyone be interested and willing to chat with me sometime in the near future about this project?

[Alex J. Best]

For the basic setup you can check out https://leanprover-community.github.io/leanproject.html and for adding more advanced CI to ensure your project is building daily we have https://github.com/leanprover-contrib/leanprover-contrib .

[Nadav Kohen]

Thanks Alex for the response :) I do have the project generated by leanproject but I am generally unsure of how to continue from here. I think the natural starting place would be that I need definitions of ByteVectors and with those define types such as UInt32 and the like. I'm sure that I could accomplish this in some crude way but I was hoping someone might be able to give me some pointers.

[Alex J. Best]

You might want to check out some of the threads in the Program Verification stream, I think there were some threads about using bitvectors there, but I'm no expert