Fixes for Malloc.

1. Give it a rule in the operational semantics.
2. Make it take an expression rather than a fixed number for
   specififying the size of the array.

A couple of later proofs needed minor tweaks.