Specify the non-determinism in more detail

[RalfJung]

We need some maths to make the non-determinism used by MiniRust fully precise -- it's the one thing code cannot describe. Or maybe it can but then we need some code that makes explicit the "explore all possible branches" nature of angelic non-determinism.