Simplify validity and refinement of permission bits.
Combine rules for entering/leaving blocks in operational semantics.
Move type checkers to separate file.