This proof demonstrates the memory safety of the TaskGetSchedulerState function.
We assume `xSchedulerRunning` and `uxSchedulerSuspended` to be nondeterministic values.

This proof is a work-in-progress.  Proof assumptions are described in
the harness.