Geometric distribution

In this example we will prove some properties about the geometric distribution. The program below simulates a geometric process with parameter 1/3. On every step it generates a random bit, and it returns the number of failed attempts before returning 0

First, we want to show that the result is always non-negative. Note that below we are proving a partial correctness specification, divergence is a valid behavior, so the specification just says that the probability that the program terminates in a value that is negative is zero

We can use the specification above to reason about the probability that the program returns a strictly positive result. Again, in a partial correctness logic, the only thing we can actually prove is that the probability that the program returns 0 or less is (2/3).

Since we only want to avoid one single outcome, we can use wp_rand_err and spend the error credit to ensure we do not get 0

Similarly, we can prove that the probability that the program does not return 0 or less is (1/3). However this case needs us to reject all cases where we sample 1 or more.

Note that the two specifications together still do not say anything about termination behavior of the geometric process. A program that diverges with probability 1 will satisfy all of the specifications as well. Eris supports as well total correctness specifications that allow us to reason about termination. However, let's keep this aside for now, and just reason about partial correctness. We can try to prove some properties about ranges of outputs, e.g. the probability that the geometric does not return a result equal to or less than 1 is (2/3)*(2/3) = (4/9)

At this point, we do not have enough error credits to outright reject one outcome. Instead, we have to distribute error credits across the outcomes of rand #1. Note that in the case v=0, we can immediately prove the postcondition, since 0 <= 1. That branch then needs 0 error credits. Therefore, we can give all other credits to the other branch By a simple calculation, we get that we can give ↯(2/3) to that branch.

We do a case distinction on whether n = 0

In the case n >= 1, we execute the program until the recursive call We now have ↯ (2/3) and we have to compute geometric #() + #1. In order for the result to be less than 1, geometric must return 0 (or less). We will spend our error credits to use geo_le0.

Let us now try to generalize these results. It is well-known that the mass of the tails of such a geometric, i.e. the probability of sampling larger than n is 2^(n+1) / 3^(n + 1).

We will need some mathematical facts about this function.

Let us now prove a specification about the mass of the tails of the geometric process. Namely, we will show that the probability that the output is not larger than n is less than geo_tail_mass n for every n. The proof goes by induction on n, and uses the specifications and lemmas we introduced above.

We now get to the main part of the proof. Here we need to split error credits depending on whether the result of the sampling is 0 or >= 1. Luckily, we already defined an abstraction over the credit arithmetic to simplify this task.