uvmThreadSemantics was becoming a huge file that took several minutes
to compile, so it's been split into uvmThreadsStacks and
uvmInstructionSemantics.

In uvmThreadsStacks, new 'thread_ok' and 'stack_ok' predicates define
basic consistency requirements for thread and stack data structures.
All functions in this file have also been proven to produce valid
thread/stack structures when given valid input. This is a prerequisite
for proving execution state homomorphisms.

'thread_state' has been renamed to 'thread', and 'state_follows' has
been renamed to 'thread_follows'.