Change pHL to prevent negative probabilities

[oskgo]

This essentially changes the semantics of phoare[M.f: pre ==> post] R x to be
forall m arg, 0 <= x{m} /\ pre{m} => Pr[M.f(arg)@&m: post] R x{m}
instead of
forall m arg, pre{m} => Pr[M.f(arg)@&m: post] R x{m}.

This is one possible resolution to most of the issues we're having with negative probabilities.

The advantage of this approach is that we do not require proving bounds when using pHL seq and call. The disadvantage is that we need to prove bounds when changing them using conseq and when proving phoare statements from statements not involving phoare, such as with exfalso and bypr.

[fdupress]

Does this handle the few situations that allow the code to change the value of the bound? (Those are usually framed, and my assumption is that there is then a conseq that handles the bound change, but I though it good to ask explicitly.)

[oskgo]

I believe so. There are some tactics where we should be able to get rid of the bound unconditionally (I'm aware of phoare split), but for now those require proving bounds.

The while variant in #1102 also proves the bad result directly, so that will have to be changed no matter which solution we go for and thus isn't addressed here.

For the record, I'm not certain that this is the right approach, but I thought it useful to at least see what the fallout would be. There's going to be a significant amount of breakage regardless AFAICT.

[fdupress]

Failures in external projects are where I would expect—developments that involve a lot of cross-logic reasoning (and therefore a lot of bypr). All of them have bounds that should be obviously positive, so I'm not too worried about our ability to fix it in a timely manner.

The main blocker is that I, personally, will likely not have the capacity to deal with any of them for about 2 weeks.