Caesar 4.0: Expression Parsing Changes, Soundness Diagnostics, and More

Caesar 4.0 improves expression parsing, adds explicit soundness guarantees for refutations in CLI/LSP feedback, introduces new weigh and additive choice (if +) statements, and experimental entailment checking.

Breaking Change

Expression parsing precedence and associativity changed in Caesar 4.0. Some expressions now parse differently, and Caesar may reject previously accepted expressions until you add explicit parentheses. See Expression Parsing Changes below.

Overview:

1. Expression Parsing Changes
2. Soundness Checks and Better Diagnostics
3. New HeyVL Statements: weigh and Additive Choice
4. Experimental Entailment Checking
5. Other Improvements

Expression Parsing Changes

We updated expression parsing to follow a clearer, more conventional precedence order and to fix surprising parses reported by users (see #112).

What changed compared to the old parser:

• +, -, *, /, %, and && now parse left-associatively (instead of right-associatively).
• ↘/↖ moved to the looser implication level with →/← (instead of binding tighter than &&/||).
• <, <=, >, >=, and != are now non-associative (== stays left-associative).

Examples of resulting behavior changes:

• n - i + x now parses as (n - i) + x (before: n - (i + x)).
• 3 / 5 * x now parses as (3 / 5) * x (before: 3 / (5 * x)).
• a ==> b && c now parses as a ==> (b && c) (before: (a ==> b) && c).
• Chains like a < b < c and a != b != c are now rejected unless parenthesized explicitly.

Transition Period

For a transition period, Caesar rejects expressions whose meaning changed under the new precedence and requires explicit parentheses. For example: n - i + x and 3 / 5 * x.

You can use --parser new|old|both (default: both) to choose parser behavior explicitly; this option is temporary and will be removed in a future release.

For the full precedence/associativity table, see expressions documentation.

Soundness Checks and Better Diagnostics

Caesar 4.0 extends proof-rule soundness tracking to both proofs and refutations (fixes #75). Previously, Caesar mainly guarded soundness of successful verifications; now it also checks when a reported counterexample is guaranteed to be a real counterexample to the original program.

Caesar now distinguishes four outcome classes (besides solver unknown/timeouts):

• Verified: a sound proof of the property.
• Unsound verification: verification succeeded, but the proof is not guaranteed sound.
• Counter-example to property found: a sound refutation.
• Counter-example to verification found: a counterexample to the encoded verification task that may be spurious for the original program.

In VSCode/LSP reporting, sound refutations are now shown explicitly as refutations, rather than as generic counterexamples.

This is based on tracked approximation kinds (Exact, Over, Under, Unknown) together with proc/coproc direction. For example, in proc checks (lower bounds), refutations are sound with Over/Exact approximations; dually, in coproc checks (upper bounds), refutations are sound with Under/Exact approximations.

Diagnostics in both CLI and LSP were updated accordingly, including clearer messages about whether results are guaranteed or may be spurious.

Read more on the newly written documentation for Soundness of Proof Rules.

New HeyVL Statements: weigh and Additive Choice

Caesar now supports the weigh statement and additive nondeterministic choices (if +) as first-class language constructs. For example:

weigh 2 * x
if + {
    x = x + 1
} else {
    x = x + 2
}

These statements still operate on the domain of extended non-negative reals. More information in the weigh documentation and nondeterministic choices documentation sections.

Experimental Entailment Checking

Caesar now includes experimental support for entailment checking via:

caesar entailment your-file.heyvl

This mode checks entailment between generated verification conditions for matching coproc/proc declarations. The release also fixes issues uncovered during early refactoring of this workflow.

For details, see the entailment documentation.

Other Improvements

This release also includes targeted fixes and quality-of-life improvements:

Proof rules and typing

• Invariant annotation resolution is now robust against shadowing, and undeclared symbols in invariants are diagnosed correctly (fixes #67, #101, #102).
• Type errors are clearer for invalid havoc usage (cf. #93).
• PAST rule fixes for missing/wrong casts and wrong condition (fixes #94; commit 7b0c105, commit 65859c3, commit 4854de1).

Quantifier elimination

• Fixes for unsound rewrite of multiplication (fixes #105) and correct handling of sup under ~ (commit ca39bc6).
  • In particular, Caesar no longer rewrites a * (inf y. ψ) to inf y. (a * ψ) when a may evaluate to ∞ (e.g. ∞ * (inf y. ([y > 0] * y + [y = 0] * 1))).

Tooling and robustness

• LSP/VSCode status reporting now distinguishes sound refutations from generic counterexamples.
• Status bar updates are now correct in error states (fixes #85).
• VSCode gutter result icons now use SVGs, replacing the previous low-resolution PNGs.
• Added CLI alias support to disable quantifier instantiation via --no-qi.
• UInt literals now use big integers, improving robustness for large numeric constants.