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.
[link] [comments]
You can get bonuses upto $100 FREE BONUS when you:
💰 Install these recommended apps:
💲 SocialGood - 100% Crypto Back on Everyday Shopping
💲 xPortal - The DeFi For The Next Billion
💲 CryptoTab Browser - Lightweight, fast, and ready to mine!
💰 Register on these recommended exchanges:
🟡 Binance🟡 Bitfinex🟡 Bitmart🟡 Bittrex🟡 Bitget
🟡 CoinEx🟡 Crypto.com🟡 Gate.io🟡 Huobi🟡 Kucoin.
Comments