Skip to content

WIP: Get rid of closedness conditions

Robbert Krebbers requested to merge no_closed into master

As we all know, and as recently came up again in #93 (closed), it is annoying and inefficient having to prove closedness of the expression for many of the symbolic execution steps. This merge request gets rid of this deficiency by changing the definition of weakest preconditions as follows:

WP e1 @ E {{ Φ }} :=
  match to_val e1 with
  | Some v => |={E}=> Φ v
  | None =>  σ1,
     closed e1 -∗
     state_interp σ1 ={E,}=∗ reducible e1 σ1 
       e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=∗
       state_interp σ2  WP e2 @ E Φ 
       [ list] ef  efs, WP ef @  (λ _, True)
  end%I.

With this new definition, we know everywhere that the expression is closed, and as such, we do not have to re-prove closedness all the time. This change has two obvious consequences: 1.) We need to extend the Iris axiomatization of programming languages with a notion of being closed and some properties about it (like reduction preserving closedness), and 2.) we only get adequacy for expressions that are closed.

IMHO, these consequences are minor, and make a lot of sense, and are thus totally worth it from a pragmatic point of view to get rid of stupid side-conditions. Note that in practice we always invoke adequacy with a value (some function) applied to some other values (the arguments). Values are closed by definition, so the closedness side-condition of adequacy is easily proved.

Note that this merge request is backwards compatible, one can define closed e := True and then one gets back the original definition of weakest preconditions, as well as the original adequacy statement.

Edited by Ralf Jung

Merge request reports