Other-non-deterministic-computations
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).
Subtopics
- Hw_rnd_gen-logic
- Hw_rnd_gen
- Other-non-deterministic-computations-exec
- Definitions of non-deterministic computations to be used for
execution
