Caesar 4.1: Soundness Fixes and Unbounded WLP

Caesar 4.1 fixes soundness bugs in @ast, @past, and @omega_invariant that could let invalid proofs pass verification. It also introduces @uwlp, extends @ast to finite demonic nondeterminism, infers loop terminators, and adds HeyVL reference hovers in Visual Studio Code.

Overview:

1. Almost-Sure Termination: @ast
2. Positive Almost-Sure Termination: @past
3. ω-Invariants: @omega_invariant
4. Unbounded Liberal Pre-expectations: @uwlp
5. Simpler Loop Unrolling
6. Visual Studio Code
7. Other Fixes

Recheck Termination and ω-Invariant Proofs

Earlier versions could accept invalid proofs using @ast, @past, or @omega_invariant. Re-run their verification after upgrading; some previously accepted proofs may now fail.

Almost-Sure Termination: @ast

Bug fix: ignoring the loop's effects

Previously, the @ast encoding removed the loop without checking its invariant at loop entry or accounting for variables modified by the loop. The corrected encoding checks the invariant at loop entry, then verifies subsequent statements for every assignment to loop-modified variables that satisfies the invariant. Variables unchanged by the loop retain their entry values.

Example: a loop changes a value that the old encoding kept

@wp proc stale_loop_value() -> (x: UInt)
    pre 1
    post [x == 1]
{
    x = 1
    @ast(true, x, v, 1, 1)
    while x > 0 {
        x = x - 1
    }
}

The loop finishes with x = 0, so the postcondition is false. Earlier versions accepted it because removing the loop left x = 1 in the verification condition. Caesar now rejects the proof.

Improvements

• Automatic side-condition checks: Caesar now verifies 0 < prob(v) <= 1 and decrease(v) > 0 for every v >= 0 under the invariant. Users previously had to check these conditions themselves. Variable scoping and dependency checks were also tightened.
• Finite demonic nondeterminism: demonic choices and havoc over finite domains are now supported. The expected-variant check uses the largest expected value across choices, so the bound must hold for every choice.
• More permissive progress conditions: an iteration can now satisfy the required progress probability by exiting the loop, even without decreasing the variant. The expected-variant check uses [G] * V after the iteration, where G is the loop guard, so exit-state variant values do not affect the bound. A variant of zero while the loop is active is also allowed if the progress condition holds.
• Antitonicity only on positive arguments: prob and decrease need to be nonincreasing only for v > 0. Their positivity checks still include zero.

See the documentation for restrictions and adaptations to the published theorem.

Positive Almost-Sure Termination: @past

We fixed two bugs in the @past proof rule.

Unsound decrease check: the rule checked the expected-decrease inequality in the wrong direction, allowing some nonterminating loops to verify as having finite expected runtime. The corrected check requires wp[Body](I) <= I - epsilon whenever the loop guard holds, with I - epsilon evaluated before the iteration.

Rejection of valid proofs: the generated decrease check used an uninitialized output variable when evaluating the guard in its precondition. The fix evaluates the guard and I in the same pre-iteration state, allowing valid countdown proofs to verify.

Example: an infinite loop accepted with a runtime bound of zero

@ert coproc infinite_runtime() -> ()
    pre 0
    post 0
{
    @past(1, 0.5, 1)
    while true {
        tick 1
    }
}

This loop accumulates cost forever, yet earlier versions accepted the upper bound of 0. The constant ranking expression 1 never decreases by 0.5, so the corrected decrease check fails.

ω-Invariants: @omega_invariant

Soundness fixes

The @omega_invariant proof rule was unsound for @wlp: its base case started from 0 instead of 1, allowing false upper bounds to verify. With the calculus-semantics fix, @wlp checks upper bounds on loop unfoldings starting from 1; @uwlp starts from \infty. For @wp and @ert, it checks lower bounds starting from 0. These choices follow the calculus annotation rather than proc versus coproc, so refuting a bound no longer changes the loop semantics.

Previously, the base case and induction step were checked only at loop-entry values of modified variables, so a family could pass those checks but fail after an iteration. The corrected checks range over all values of loop-modified variables, while unchanged variables retain their entry values. The index n is scoped to the invariant expression and can no longer be used in the loop guard, body, or following statements.

Example: a false upper bound on wlp

@wlp coproc false_wlp_bound() -> ()
    pre 0
    post 0
{
    @omega_invariant(n, 0)
    while true {}
}

This loop has wlp(0) = 1, yet earlier versions accepted the upper bound of 0. Starting the base check from 1 exposes the invalid constant invariant 0, and Caesar now rejects the proof.

New option: the annotation now accepts an explicit third argument, @omega_invariant(n, I, terminator), and uses the same default terminators as @unroll when it is omitted.

Unbounded Liberal Pre-expectations: @uwlp

Caesar now supports @uwlp, the unbounded weakest liberal pre-expectation calculus. For purely probabilistic programs, wlp is wp plus the probability of nontermination. uwlp is wp plus \infty if a diverging path exists (even one of probability zero), and just wp otherwise.

@uwlp proc maybe_diverge() -> ()
    pre \infty
    post 1
{
    var diverge: Bool = flip(0.5)
    @invariant(ite(diverge, \infty, 1))
    while diverge {}
}

This program terminates immediately with probability 0.5 and otherwise loops forever. For post-expectation 1, its wp is 0.5, its wlp is 0.5 + 0.5 = 1, and its uwlp is \infty, so the procedure verifies.

@uwlp works on both procs and coprocs, with the existing proof-rule soundness checks, calculus checks for procedure calls, and recursion restrictions.

Simpler Loop Unrolling

The loop unrolling annotation now accepts @unroll(k) in addition to @unroll(k, terminator). Caesar infers an omitted terminator from the enclosing procedure's calculus:

Calculus	Default terminator
@wp, @ert	0
@wlp	1
@uwlp	\infty

For example, the following program proves a lower bound of 0.75 on the termination probability of a geometric loop:

@wp proc geo_unroll() -> ()
    pre 0.75
    post 1
{
    var cont: Bool = true
    @unroll(3)
    while cont {
        cont = flip(0.5)
    }
}

Here, @unroll(3) is equivalent to @unroll(3, 0). Verification condition explanations also use the inferred terminator.

Without a calculus annotation or an explicit terminator, @unroll and @omega_invariant default to 0 in a proc and \infty in a coproc. An explicit literal 0, 1, or \infty can select the corresponding semantics when no calculus annotation is present.

Explicit terminators are used as written, with a warning unless they match the expected literal.

Visual Studio Code

The VS Code extension now shows explanations and documentation links when hovering over HeyVL keywords, operators, types, and proof annotations. For example, hovering over proc explains how its pre and post specify a lower bound.

The status bar fix prevents Verified! from appearing when some procedures are refuted or still pending. That status now appears only when verification is complete and all reported results are successful.

We also improved HeyVL syntax highlighting in VS Code and on the website.

Other Fixes

• Fixed extraction of negated embedded Boolean conditions in the model-checking translation.
• Corrected the documented condition for the expected value of the uniform distribution.