Pattern Matching in Rust's Neverland

Recently, I’ve been working on a tool for manipulating EVM bytecode and assembly language. I wanted to describe low level bytecode and assembly language using the same datatype. At the same time, I wanted some instructions to be allowed only in assembly language but not bytecode (e.

Disassembling EVM Bytecode (the Basics)

Recently, I’ve been looking at how to disassemble (and eventually decompile) bytecode for the Ethereum Virtual Machine (EVM). This is an interesting computer science problem which I’ve been thinking about lately.

Formalising a Simple Virtual Machine

Since starting my new role at ConsenSys, I have become interested in formalising virtual machines. For example, there are already some formalisations of the Ethereum Virtual Machine (e.g. in K, Lem, Coq).

Whiley gets Rusty!

I’ve been learning Rust for a while now but, at the same time, trying to continue developing Whiley. Since Whiley was written entirely in Java, these activities were mutually exclusive and it was frustrating trying to balance things!

Puzzling Strong Updates in Rust

The idea of a strong update comes from earlier work on static analysis and, in particular, pointer analysis. To understand this, let’s imagine a hypothetical non-null analysis for C: int* r = (int*) malloc(sizeof(int)); int** p = &r; At this point, our non-null analysis would conclude that p was nonnull and that r was nullable.