I’ve just written a formally verified version of RLP encode/decode in Kind-Lang

I've just implemented Ethereum's RLP (Recursive Length Prefix) encoding in Kind, and proven the identity theorem (decode(encode(tree)) == tree). RLP is a dirty optimized serialization format that converts trees of bytes to a compressed binary format, back and forth, and it is used in many places in Ethereum, such as when sending a transaction to the blockchain. RLP embeds a lot of different information in the same header byte, which makes the proofs are quite complex. It took me about ~1h to implement the functions, and ~20h to prove the theorems. While doing so, I've realized Kind-Lang has a lot to improve before having a good UX for theorem proving. In special, it is very annoying (and noisy) to have to copy/paste goals over and over to do rewrites. That needs to go.

The encoder/decoder are here:

https://github.com/kind-lang/Kind/blob/master/base/RLP.kind

The identity proof is here:

https://github.com/kind-lang/Kind/blob/master/base/RLP/encode_identity.kind

I think this is the most complex theorem proven in Kind-Lang. To be fair, there are some minor numeric lemmas missing. My colleagues will prove these over the next days. Honestly, I can't want to improve these aspects of the language. I have many powerful ideas, I just need time.

In a future I may write a blog post to explain how these things work, in case anyone is interested.