5.2. Weakest Precondition🔗

The first construct for specifying program behaviour is the weakest precondition. In Iris, a weakest precondition has the form WP e {{ v, Φ v }}. This asserts that if the HeapLang program e terminates at some value v, then v satisfies the predicate Φ. The double curly brackets are the postcondition.

The Rocq tutorial begins with a pure arithmetic example #1 + #2 * #3 + #4 + #5 and uses the wp_op/wp_pure/wp_pures tactics to symbolically execute it. The Lean version of these tactics is wp_pure/wp_pures, which iterate the wp_pure_step_fupd rule. However, iris-lean's HeapLang only provides PureExec instances for β-reduction, if/case/inj, pair projections, and ≤ on integers. The arithmetic operators have no PureExec instance, so wp_pure cannot fire on #2 * #3 or any of the additions.

-- TODO (upstream — iris-lean): register `PureExec` instances for
-- the arithmetic binops on `BaseLit.int` (and ideally also on
-- bit-wise / shift operators). Until then `arith_spec` cannot be
-- proved in the natural way.

-- Rocq tutorial reference:
--   Example arith : expr := #1 + #2 * #3 + #4 + #5.
--   Lemma arith_spec : ⊢ WP arith {{ v, ⌜v = #16⌝ }}.
--   Proof. rewrite /arith. wp_op. wp_pure. wp_pures.
--          iModIntro. iPureIntro. reflexivity. Qed.

To showcase the tactics that do work, here is the same shape of proof on a program that only uses β-reduction and if:

The tactic wp_pures symbolically executes all pure steps for which a PureExec instance exists. Each step internally applies the wp_pure_step_fupd rule from Iris.ProgramLogic.Lifting, which says (informally):

e₁ →pure e₂
──────────────────────────────────
WP e₂ {{ Φ }} ⊢ WP e₁ {{ Φ }}

After every pure step has fired, the goal is reduced to proving the postcondition behind a fancy-update modality |={⊤}=>; itrivial discharges the residual proposition ⌜#1 = #1⌝.

The lambda program from the previous chapter mixes lambda application with arithmetic. Because of the same PureExec gap, we cannot symbolically evaluate it end-to-end in iris-lean today.

-- TODO (upstream — iris-lean): same as above — `lambda` contains
-- `+` and `*`. The lambda β-reductions all work via
-- `wp_pure`/`wp_pures`, but the arithmetic reductions do not.

-- Rocq tutorial reference:
--   Lemma lambda_spec : ⊢ WP lambda {{ v, ⌜v = #20⌝ }}.
--   Proof. rewrite /lambda. wp_pures. done. Qed.

A purely β-driven analogue does prove cleanly: