Definitions of other non-deterministic computations
All the *-logic functions (like HW_RND_GEN-logic
for the RDRAND instruction) should be untouchable --- we want to
disallow the use of these functions during evaluation as well as proof
since they aren't the top-level interface functions (like hw_rnd_gen).
- Definitions of non-deterministic computations to be used for