@piraipra’s snapshot post (October 2017)

Yoichi Hirai

I write about what I’m doing currently for Ethereum, and why.

Yellow Paper

Yellow Paper is the specification of Ethereum. It’s notoriously terse, but still one of the most precise descriptions of valid Ethereum blocks and the Ethereum Virtual Machine. The contents are getting older with lots of issues and pull-requests. Since it is not licensed, the author has the control over it. What I can do is to submit certain delta’s between protocol versions or certain small fixes. I got some of my previous pull-requests merged, but there is still a lot to be done.

I’m currently syncing the mainnet using a modified cpp-client. This is part of the efforts to tackle the ambiguous specification around empty accounts on precompiled contracts. Although this issue does not pose a threat to the mainnet, it’s a headache when I have to specify the protocol rules. Every client implements something different and tests fail for that. This ambiguity must be resolved before I can work on Spurious dragon version of the Yellow Paper.

By the way, I recently realized that the Homestead version of Yellow Paper is missing.

Bamboo — writing spec to be independent of those warm fuzzy feelings

Bamboo is a new programming language for Ethereum contracts. I wrote about it recently. It is still not very usable because a Bamboo contract cannot call other contracts following Ethereum ABI. For that, I need interface declarations. The implementation has stalled, so I might need to retake it. On some other features, Bamboo is getting nice contributions. Bamboo is a rare OCaml codebase in Ethereum.

I’m writing a specification of Bamboo. With a specification, I can eventually write proofs about Bamboo programs. With a specification, an independent Bamboo interpreter can be written, and the compiler can be tested for functional correctness. I believe that’s the way for independence from the warm, fuzzy feeling you get from reading code.

Eth-Isabelle — OCaml libraries for tests

Eth-Isabelle has been driven by contributors for some time. Now I see some sophisticated separation logic library that works with the EVM definitions. The next step seems like the treatment of reentrancy in this separation logic library. Maybe I should try to search the literature for a Hoare logic treatment of reentrant Java program or something.

I’ve been trying to run the blockchain tests through eth-isabelle. For that, I need to encode a transaction into an RLP and sign it. So, I implemented an RLP library in OCaml, and extended an ecdsa wrapper. I’m currently in the middle of encoding transactions as RLPs.

cpp-ethereum — Removing ThreadSanitizer warnings

I’ve been trying to remove ThreadSanitizer warnings from cpp-ethereum. There were many. The codebase is still reviving from some period of negligence. Every file is crying for some fix. I find it addictive to fix small race conditions and to remove dead code because I can keep fixing them forever. I still see invariant failures whan I sync the mainnet with cpp-ethereum. Still, I think I’ve been spending too much time on this because no colleagues of mine can work on Bamboo or Eth-Isabelle.

Besides, there is a segmentation fault in the macos builds in CircleCI. I’m trying to debug that.


Test cases for Byzantium have not been all implemented although Byzantium went live on the mainnet. What an embarrassment. Several new test cases were proposed before the hard fork. I’ll keep writing a couple of tests every week.

Program Committees

I’m going to serve as a program committee member of WTSC’18 and BPASE 2018. This means I will be reading some of the submissions in hiding.

Looking around

I’m trying to get hold of what other people are doing. I tried running tests through KEVM. I think I should also try to modify contract verification examples there.

When I read about Matching Logic, I will see if I like it or not.

I got interested in the use of erasure coding. I haven’t got a grasp of why the multidimensional treatment gives efficiency. If the proof of proximity really works, that’s like an injective compression that always shrinks the data size. I don’t believe this, so maybe I should try to find a flaw in the calculation.

I still need to update the Isabelle proofs about Casper. The protocol got simpler, so should the proofs.

From a conversation over lunch, I got an inspiration to check MetaMath and see if that can be implemented on Ethereum.

I’m also preparing some slides for Cancun.

Yoichi Hirai

Written by

a convenience logician

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade