"Mutable Forest" Memory Model for blockchain specs

[ericsson49]

@norswap

I think a solution is to simply fork the spec, make it functional but still readable!

BTW, my colleagues at ConsenSys are re-writing beacon chain specs in Dafny and they avoid destructive updates as far as I remember.