Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T13:59:44Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/228"expression validity" in WP2019-11-01T13:59:44ZJonas Kastberg"expression validity" in WPI propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid in the absence of certain properties on the state. A predicate on expression, that are preserved under step reduction, could be used to differentiate such expressions.
Furthermore, being able to derive certain properties about expressions when opening the weakest precondition might allow for some automation in regards to "pure" reductions that depend on the state while not changing it.
Specific Case:
My Iris instantation is a "language" over processes, where ```pstate := gmap pid (state)``` and ```pexpr := pid * expr```, where ```pid``` is a process identifier.
For modularity I have separate reduction layers, with the top-layer looking up the state of the process in the state map ```step ((p,e), <[p := σh]>σp) -> ((p,e'), <[p := σh']>σp), efs)```.
This means that every single reduction requires the process id of the expression to be in the map, even if it does not change (in case the underlying reduction is pure).
The presence of the necessary mapping is then expressed as a logical fragment, which is required by every single of my weakest precondition rules. Furthermore, I cannot do "Pure" reductions, as conceptualised with the existing ```PureExec``` class.
Proposed Solution:
Update the language instantiation to include a predicate over expressions (here named ```well_formed```), and use it in the weakest precondition.
The predicate should uphold certain properties, such as being preserved under step reduction and contexts.
```
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κ κs n,
state_interp σ1 (κ ++ κs) n ∗ well_formed e1 ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs (length efs + n) ∗
well_formed e2 ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, well_formed ef ∗ wp ⊤ ef fork_post
end%I.
```
Define a lifted ```PureExecState```, which defines expressions that are reducible and "pure" assuming that the state interpretation and well-formedness predicates hold:
```
Record pure_step_state (e1 e2 : expr Λ) := {
pure_exec_val_state : to_val e1 = None;
pure_step_safe_state σ1 κ n : state_interp σ1 κ n -∗ well_formed e1 -∗ ⌜reducible_no_obs e1 σ1⌝;
pure_step_det_state σ1 κ κs e2' σ2 efs n :
state_interp σ1 (κ++κs) n -∗ well_formed e1 -∗ ⌜prim_step e1 σ1 κ e2' σ2 efs⌝ → ⌜κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []⌝
}.
```
An important property of the proposed change is that original Iris instances remain unchanged when given ```True``` as the well_formed predicate.
Points of discussion:
- It has earlier been suggested to introduce closedness of expression in a [similar manner](https://gitlab.mpi-sws.org/iris/iris/merge_requests/58). Note however that the closedness condition on expressions has been phased out of the current iteration of Iris.
- The change would mean that any WP holds trivially true for invalid expressions, which must then suddenly be considered in many places.I propose updating the weakest precondition with a predicate over expressions,
mainly for the purpose of establishing a notion of ```well formed``` expressions.
General idea:
The idea is that some expressions might be outright invalid in the absence of certain properties on the state. A predicate on expression, that are preserved under step reduction, could be used to differentiate such expressions.
Furthermore, being able to derive certain properties about expressions when opening the weakest precondition might allow for some automation in regards to "pure" reductions that depend on the state while not changing it.
Specific Case:
My Iris instantation is a "language" over processes, where ```pstate := gmap pid (state)``` and ```pexpr := pid * expr```, where ```pid``` is a process identifier.
For modularity I have separate reduction layers, with the top-layer looking up the state of the process in the state map ```step ((p,e), <[p := σh]>σp) -> ((p,e'), <[p := σh']>σp), efs)```.
This means that every single reduction requires the process id of the expression to be in the map, even if it does not change (in case the underlying reduction is pure).
The presence of the necessary mapping is then expressed as a logical fragment, which is required by every single of my weakest precondition rules. Furthermore, I cannot do "Pure" reductions, as conceptualised with the existing ```PureExec``` class.
Proposed Solution:
Update the language instantiation to include a predicate over expressions (here named ```well_formed```), and use it in the weakest precondition.
The predicate should uphold certain properties, such as being preserved under step reduction and contexts.
```
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κ κs n,
state_interp σ1 (κ ++ κs) n ∗ well_formed e1 ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs (length efs + n) ∗
well_formed e2 ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, well_formed ef ∗ wp ⊤ ef fork_post
end%I.
```
Define a lifted ```PureExecState```, which defines expressions that are reducible and "pure" assuming that the state interpretation and well-formedness predicates hold:
```
Record pure_step_state (e1 e2 : expr Λ) := {
pure_exec_val_state : to_val e1 = None;
pure_step_safe_state σ1 κ n : state_interp σ1 κ n -∗ well_formed e1 -∗ ⌜reducible_no_obs e1 σ1⌝;
pure_step_det_state σ1 κ κs e2' σ2 efs n :
state_interp σ1 (κ++κs) n -∗ well_formed e1 -∗ ⌜prim_step e1 σ1 κ e2' σ2 efs⌝ → ⌜κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []⌝
}.
```
An important property of the proposed change is that original Iris instances remain unchanged when given ```True``` as the well_formed predicate.
Points of discussion:
- It has earlier been suggested to introduce closedness of expression in a [similar manner](https://gitlab.mpi-sws.org/iris/iris/merge_requests/58). Note however that the closedness condition on expressions has been phased out of the current iteration of Iris.
- The change would mean that any WP holds trivially true for invalid expressions, which must then suddenly be considered in many places.https://gitlab.mpi-sws.org/iris/iris/-/issues/138wp_apply/Texan triple improvements2020-02-23T22:25:25ZRalf Jungjung@mpi-sws.orgwp_apply/Texan triple improvements* `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* When proving a tirple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
Blocked by #130* `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* When proving a tirple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
Blocked by #130https://gitlab.mpi-sws.org/iris/iris/-/issues/134Document language interface2019-11-01T13:08:15ZRobbertDocument language interfaceIt would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related documentation, also including the current `ProofMode.md`. We could also LaTeX-ify all Coq documentation, and add it to the already existing theoretical documentation.It would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own `wp_` tactics, and so on.
Considering #131, it may be good to have a separate folder with Coq related documentation, also including the current `ProofMode.md`. We could also LaTeX-ify all Coq documentation, and add it to the already existing theoretical documentation.https://gitlab.mpi-sws.org/iris/iris/-/issues/117Make some of the `wp_` tactics language independent2019-11-01T13:23:45ZRobbertMake some of the `wp_` tactics language independentA large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.A large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.