Understanding @ast in 1d random walk

[ahuoguo]

I'm trying to prove AST of 1d random walk similar to the escaping spline program:

proc rdwalk(init_x: UInt) -> (x: UInt)
{
    var prob_choice: Bool
    x = init_x
    @ast(
        /* invariant: */    true,
        /* variant: */      x,
        /* variable: */     v,
        /* prob(v): */      0,
        /* decrease(v): */  0,
    )
    while x != 0 {
        prob_choice = flip(1/2)
        if prob_choice {
            x = x - 1
        } else {
            x = x + 1
        }
    }
}

I'm not quite sure how caesar is able to prove the almost sure termination of the loop as the values I give to @ast(...) don't seem to be decreasing. In fact, the proof goes through when I specify the invariant as false.

[ahuoguo]

Oh, the caesar verify --print-theorem --no-slice-error pgcl/examples-heyvl/1drwalk.heyvl command is quite helpful.

Based on https://www.caesarverifier.org/docs/proof-rules/ast, I guess most of the heavy lifting is done by the superinvariant rule, which only needs me to supply the correct /* variant: */ x?

[ahuoguo]

Actually, I still can't follow this example:

proc rdwalk(init_x: UInt) -> (x: UInt)
    pre 1
    post 1
{
    var prob_choice: Bool
    x = init_x
    @ast(
        /* invariant: */    false,
        /* variant: */      1,
        /* variable: */     v,
        /* prob(v): */      0,
        /* decrease(v): */  1,
    )
    while x != 0 {
        prob_choice = flip(1/2)
        if prob_choice {
            x = x - 1
        } else {
            x = x + 1
        }
    }
}

I don't think I provided anything helpful for the prover to conclude AST

[darionhaase]

I think the chosen prob and decrease are the main problem.

The documentation's formal statement of the AST rule states that the range of prob and decrease must be strictly positive. Intuitively, you have to show that the variant actually decreases by a value > 0 with a probability > 0 (in expectation).

However, it appears this is never checked by Caesar. Instead, we rely on the user providing correct parameters, which is not the case in your examples. Caesar only checks the six conditions listed in the documentation. With the given values, Caesar can (trivially) verify them and wrongly reports successful verification.

Ideally, Caesar should also check these parameter constraints. I don't recall why this is not done. This should at least be clarified in the documentation.

[umutdural]

There are two different but equivalent perspectives to see why setting invariant to false still works. The first one is an indirect explanation based on the definition of the proof rule and the second one is the technical explanation.

• Quoting the documentation: "Additionally, a Boolean invariant I must be specified which limits the set of states on which almost-sure termination is checked." Hence, the proof rule proves that "while G { Body } is almost-surely terminating from all initial states satisfying I." If you pick false as I (or invariant) then no initial state satisfies false. When there are no states that satisfy the invariant, the property trivially holds because the statement is quantified with "for all".
• What this proof rule actually proves is the following: [I] <= wp[while G { Body }](1). Therefore, if one picks I := false then [I] = [false] = 0. Furthermore 0 is a lower bound to the wp of every program and post expectation, i.e., 0 <= wp[C](X) for all program C and post-expectation X. Hence, regardless of the program, it should always verify.

Similarly we can also argue why we set the invariant to true again in those two perspectives:

• If we want to prove that the program almost surely terminates for all initial states, we must set I to true so that we do not filter out any initial state while checking almost sure termination with this proof rule.
• For the technical explanation, we can look at what proving almost sure termination in terms of wp means. In order to prove almost sure termination (for every initial state), one can prove a lower bound of 1 on the termination probability wp[C](1), i.e., 1 <= wp[C](1). This is also explained briefly in the documentation. There are multiple approaches for encoding this proof in HeyVL but we focus on how we can encode it with this AST proof rule now. Recall that this proof rule actually proves the following: [I] <= wp[while G { Body }](1). To prove almost sure termination for every initial state with this proof rule, one must set I to true to get [I] = [true] = 1 <= wp[while G { Body }](1).

This also means that if the proof rule works for the invariant true, then it should work for any other invariant because [phi] <= [true] = 1 for all boolean predicates phi. In other words if [true] <= wp[C](1) holds, then [phi] <= wp[C](1) will also hold by transitivity ([phi] <= [true] <= wp[C](1)).

In that sense true is the most strict invariant one can pick and false is the loosest. If a program does not terminate almost surely for all initial states but only for some of them defined by a predicate phi, one can also use phi instead of true as the invariant in this proof rule.

[ahuoguo]

Thanks for the detailed answer!

If a program does not terminate almost surely for all initial states but only for some of them defined by a predicate phi

I guess one (not very interesting) example is:

proc rdwalk(init_x: UInt,) -> (x: UInt)
{
    var prob_choice: Bool
    x = init_x
    @ast(
        /* invariant: */    x < 3,
        /* variant: */      x,
        /* variable: */     v,
        /* prob(v): */      1/2,
        /* decrease(v): */  1,
    )
    while x != 0 {
        if x < 3 {
            x = 0
        } else {

        }
    }
}

(the prob and decrease here are redundant)

[ahuoguo]

One more interesting example, which looks like the use of invariants like how it works in non-probabilistic automated theorem provers

proc rdwalk(init_x: UInt, init_y: UReal) -> (x: UInt)
{
    var prob_choice: Bool
    var y: UReal
    x = init_x
    y = init_y
    y = 1 / 2
    // It can't verify if I provide invariant `true`.
    @ast(
        /* invariant: */    y == 1/2,
        /* variant: */      x,
        /* variable: */     v,
        /* prob(v): */      1/2,
        /* decrease(v): */  1,
    )
    while x != 0 {
      prob_choice = flip(y)

      if prob_choice {
          x = x - 1
      } else {
          x = x + 1
      }
    }
}

But if I change the invariant to y >= 1/2, it can't verify (though I would think those initial states should all be AST).

[Philipp15b]

Indeed, your example (#97 (reply in thread)) shows how one can use the invariant properly.

The second example (#97 (reply in thread)) correctly does not verify, as it does not guarantee that 0 <= y <= 1. If the parameter y for prob_choice = flip(y) is not in this range, the result is undefined and Caesar rejects the program. With the invariant y >= 1/2 && y <= 1, the program verifies again.

Although it's technically documented that y > 1 yields undefined behavior (c.f. https://www.caesarverifier.org/docs/stdlib/distributions#symbolic-with-probabilities), there should be an explicit check in Caesar with a proper error message. I've opened issue #98 to fix this.

The fact that the invariant false makes the whole proc verify immediately is also confusing. I've opened issue #99 to address this. In the future, users would have to explicitly add pre ?(invariant) to the proc. E.g. with pre ?(false) it is very explicit that there are no initial states from which AST is proven.

[ahuoguo]

Thanks for being super responsive!