Separate soundness proof of executable semantics.
Update docs.