Geometric distribution

Before, we have mentioned that we are working with a partial correctness version of Eris. That is, we consider non-termination as a valid behavior. In particular a diverging program satisfies any specification. Let's show this more concretely

There is a later modality in front of our IH Let's take a single execution step

Two things have happened. First, the program has taken an execution Second, the ▷ in front of our IH has been removed. We continue the execution

We now apply the IH and conclude

Eris defines a second version of the logic to reason about total correctness. In this case, divergence is considered an erroneous behavior. Triples for total correctness use the syntax [{ P }] e [{ v, RET #v; Q }] Total correctness triples have a different soundness result. Suppose we prove [{ ↯ ε }] e [{ v, RET #v; Q }] Then, the probability that the program diverges or terminates in a value v that does not satisfy Q is at most ε. In other words, with probability at least 1-ε, e will terminate in a result that satisfies Q. In particular, [{ True }] e [{ v, RET #v; Q }] implies that the program terminates with probability 1, and all possible results satisfy Q. Let us now try to prove the specification above with a total triple, and show what happenens

Total correcntness triples unfold into a total correctness WP, which is indicated with the square brackets { } in the postcondition

So far everything looks the same. Let's step our program

Note now that the ▷ is still in front of the IH Let's continue the proof Eris lemmas sampling in the total correctness version of the logic are analogous, and have the same name, with thei prefix twp

We would now like to use the IH. However, the ▷ in front of it prevents us from using it. In fact, we cannot finish this proof

Recall the definition of the geometric process

Let's now show that it terminates with probability 1, and when it does it returns a non-negative number. We will first try the proof technique we used in the partial correctness version, although by now it should be clear that it will not work

We are now unable to use the IH

One now might wonder how to prove the specification above. In the determinstic setting, we can use some form of induction on the argument of a recursive function to prove that it terminates, but geometric does not have an argument, and it is not clear what to induct on. Eris introduces a new kind of induction we call "error induction". Namely, we can induct on the amount of error credits we own. In it simplest form, the rule looks like: ⌜ 0 < ε ⌝ ∗ ⌜ ε < ε' ⌝ ∗ (↯ ε' -∗ P) ∗ ↯ ε ⊢ P

---

↯ ε ⊢ P Let's explain this step by step. Suppose we own ↯ ε for a strictly positive ε, and we are trying to prove P. Then it is sound to choose another ε' such that ε < ε', and assume that (↯ ε' -∗ P). One can think of this as an inductive hypothesis that is "guarded" by some amount of error credits, in a similar manner as our inductive hypothesis from iLöb was guarded by ▷. Instead of taking program steps, the way we can get access to the hypothesis is by amplifying ε into ε', which we can do by using the sampling rules. Let's now try to prove the previous specification again. First let's assume that we start by owning some arbitrary but positive amount of error credits

Error induction can be used through the rule ec_induction. At this point, we have to choose ε'. We now from previous examples that the inductive hypothesis will be used in the case where rand #1 returns 1, which happens with probability 1/2. By using the sampling rules, we can actually get ↯(3/2)*ε in that branch, so let us try that.

We are required to show that the amount of error credits guarding the inductive hypothesis is strictly larger than the amount we own

We choose the same error distribution function

The case n=0 does not make any recursive call, so we can conclude by symbolic execution

The case 1 <= n calls geometric recursively

Note that now, we have amplified our error credits to 3/2 * ε, so we have enough credits to apply IH

The specification above assumed initial ownership of a strictly positive amount of error credits ↯ε. By the soundness result for total Hoare triples, we get that the probability of returning a non-negative number is at least 1-ε. Since ε is arbitrary, we can use a limiting argument to conclude that the probability is actually 1. However, this is not entirely satisfactory, because this is only proven in the ambient logic (Rocq), and outside of Eris. It would be better to be able to write and prove the spec entirely within Eris. Fortunately, it is sound in Eris to assume ownership of an arbitrary positive amount of error credits whenever we are proving a WP (either total or partial). Indeed, the following rules are sound: (∀ ε, ⌜ 0 < ε ⌝ ∗ ↯ ε -∗ WP e Φ ) -∗ WP e Φ ) (∀ ε, ⌜ 0 < ε ⌝ ∗ ↯ ε -∗ WP e { Φ }) -∗ WP e { Φ }) There is a technical side condition that e must not be a value, but this is easily discharged. We can use this principle to prove the final spec

A positive amount of error credits can be obtained with twp_err_pos

We can now use the specification proven above

Correctness of the geometric sampler

In our CPP26 paper, we propose a method to use Eris to design specs for samplers that allows us to show that they are correct, and also that can be used in larger proofs to treat the sampler as if it was a primitive. They key idea is to generalize the principle behind expectation preserving error distribution. Suppose we have a sampler that is implementing a distribution μ. Then, the sampler should satisfy that, for every error distribution function F : nat -> [0,1], if we own ↯ E_μ[F], where E_μ denotes expected value over μ, we can sample n and get ↯(F n) in our postcondition. We will exercise this with the geometric sampler we defined above. Recall that the expected value for F under a geometric with parameter 1/3 is given by Σ_n (1/3)*(2/3)^n*(F n)

The proof goes by error induction

The key idea is the following: we need to send ↯ (F 0) to the branch where we sample 0. Otherwise, we will sample from the geometric recursively and add 1 to the result. Therefore, that case requires:

• ↯ (3/2)*ε to pay for the IH
• ↯ Σ_{n} (1/3)*(2/3)^n*(F (S n)) to be used in the precondition of

the recursive call. This ensures that if the recursive call returns n, it will also have ↯ (F (S n)) in the postcondition, and the overall execution will return n+1, so we have the right amount of credits.

We prove the side conditions of twp_rand_exp

Now we are back to reasoning about the program. Again, we do a case distinction on whether we sample 0 or not

The case for 0 is easy

In the case for >0, we begin by splitting our credits

We instantiate our IH with the error distributing function H. In order to do so, we have to give up ↯(3/2)*ε