Lift requirement that choice_types have to be inhabited

[MarkusKL]

This PR lifts the requirement that choice_types are inhabited, which allows for significant simplifications. This also allows us to model all finTypes as choice_type instead of just the inhabited ones, which makes parametric arguments simpler. All in all: less up front proof obligations (and custom concepts) for the user.

A canonical element (chCanonical) was relied upon in the following constructs:

• The canonical element was used as a default value when function resolution failed (resolve). Instead, we sample from the null distribution (corresponding to fail or #assert false). The behavior on failed resolution is not relied upon by any of the code as it cannot happen when two packages with compatible interfaces are composed.
• The canonical element was used in the semantics on opr (a call to underlying module). Like above, we sample from the null distribution instead.
• The canonical element was used as the initial value of heap variables. Instead, the Location also carries the initial value. I think that this is better, because it makes the user aware that there even is an initial value and what it is, which is now up to the user to decide.

This has led to the following simplifications and improvements:

• chFin uses a nat instead of a custom positive record (which is a nat including a proof of positivity). As a consequence all finTypes can be represented and there is no need for a Positive proof.
• uniform is defined for all natural numbers, but uniform 0 is equivalent to fail. So to prove LosslessOp of uniform n we require that 0 < n. However, this is only required to be known in very few places throughout the examples.
• chCanonical, positive and Positive and minor definitions have been removed. This has led to simplifications in all affected the examples.
• coerce returns an option and callees have to decide what happens on failed type coercion.
• mkloc n (v : T) defines a Location numbered n : nat with initial value v of type T (which should be a choice_type by reverse coercion).
• An initialization bug in tSDH.v has been fixed (adversary was able to call guess before set_up. This kind of bug should become less prevalent because there is no obvious initial element to choose and therefore the location should be an option.

[MarkusKL]

@ErVinuelas, I made some changes to tSDH.v and I know that you may be depending on it. Will you check that the changes (removing locations and adding default value) are compatible with your development?

[ErVinuelas]

I think the changes should be compatible. I had to change the tSDH.v in my own development, so it is no longer the same as the one in main. When I merge (my own branch) I will probably have to change some parts of the proof to accommodate this changes, but I think it should be doable. Thank you for the heads-up.

[ErVinuelas]

I was planning to make a pull request regarding adding a chTuple to the choice_type. I will wait for these changes to be merged to make the pull request.

[spitters]

Thanks! LGTM. @4ever2 feel free to merge when you're happy.