Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2023-08-05T10:26:57Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/538proofmode: figure out when to call `pm_prettify`2023-08-05T10:26:57ZRalf Jungjung@mpi-sws.orgproofmode: figure out when to call `pm_prettify`https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/956 fixed some display bugs by adding missing `pm_prettify` calls. However I added them in a basically arbitrary place since we don't have a clear pattern of when and when not to pret...https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/956 fixed some display bugs by adding missing `pm_prettify` calls. However I added them in a basically arbitrary place since we don't have a clear pattern of when and when not to prettify. Would be good to sort that out.https://gitlab.mpi-sws.org/iris/iris/-/issues/537`iInduction ... forall (xs)` does not revert persistent hypotheses containing...2023-08-04T08:15:01ZRobbert Krebbers`iInduction ... forall (xs)` does not revert persistent hypotheses containing `xs````coq
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' {PROP : bi} {A B} (l1 : list A) (l2 : list B) :
⊢@{PROP} □ (∀ k x2, ⌜l2 !! k = Some x2⌝ ...```coq
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' {PROP : bi} {A B} (l1 : list A) (l2 : list B) :
⊢@{PROP} □ (∀ k x2, ⌜l2 !! k = Some x2⌝ -∗ True) -∗
True.
Proof. iIntros "#Himpl". iInduction l1 as [|x1 l1] "IH" forall (l2).
```
Example taken from https://gitlab.mpi-sws.org/iris/iris/-/issues/534https://gitlab.mpi-sws.org/iris/iris/-/issues/536`iIntros (?%lemma) "H"` fails if the lemma opens side-conditions2023-08-04T07:57:15ZRalf Jungjung@mpi-sws.org`iIntros (?%lemma) "H"` fails if the lemma opens side-conditionsTest case:
```
Lemma test_iIntros_subgoals (m : gmap nat nat) i x :
⊢@{PROP} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some) "H".
```
If we fix this we should be able to revert...Test case:
```
Lemma test_iIntros_subgoals (m : gmap nat nat) i x :
⊢@{PROP} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some) "H".
```
If we fix this we should be able to revert the hack from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/964.
As @robbertkrebbers says the fix is probably to put `first` in the right places, but the annoying thing is that `first` fails when there are 0 goals, and 0 goals is also a real possibility (when destructing `False`, for instance). We want to run our remaining tactics on "the first goal, but only if any goal exists" -- I don't know how to do that.
Also `_iIntros_go` has a `startproof` variable that is set to `false` in a bunch of random places without any comment that would explain why, so refactoring that code is very hard. I think we should be able to just do `iStartProof` once upfront instead of all of that mess, but that is blocked on https://gitlab.mpi-sws.org/iris/iris/-/issues/535, and even then maybe it breaks whatever logic that `startproof` variable is supposed to capture.https://gitlab.mpi-sws.org/iris/iris/-/issues/535`iStartProof` does not preserve names of quantified variables2023-08-04T07:57:15ZRalf Jungjung@mpi-sws.org`iStartProof` does not preserve names of quantified variables```
Lemma test_iStartProof_variable_names (Φ: nat → PROP) :
∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iStartProof.
```
Now the goal is `∀ x : nat, Φ x -∗ ∃ x0 : nat, Φ x0`: `iStartProof` does not preserve the name `y` properly.```
Lemma test_iStartProof_variable_names (Φ: nat → PROP) :
∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iStartProof.
```
Now the goal is `∀ x : nat, Φ x -∗ ∃ x0 : nat, Φ x0`: `iStartProof` does not preserve the name `y` properly.https://gitlab.mpi-sws.org/iris/iris/-/issues/529Avoid `Local Ltac` and `Local Tactic Notation`2023-09-14T16:04:32ZRobbert KrebbersAvoid `Local Ltac` and `Local Tactic Notation`There appears to be no way to call such tactics outside of the module, making debugging very difficult.
For `Local Ltac`, I think this is a Coq bug, see https://github.com/coq/coq/issues/17884
For `Local Tactic Notation`, I think it's ...There appears to be no way to call such tactics outside of the module, making debugging very difficult.
For `Local Ltac`, I think this is a Coq bug, see https://github.com/coq/coq/issues/17884
For `Local Tactic Notation`, I think it's inherently broken since `Tactic Notation` extends the grammar.https://gitlab.mpi-sws.org/iris/iris/-/issues/528Depend on Coq-elpi2023-08-02T09:51:46ZRobbert KrebbersDepend on Coq-elpiCoq-elpi might bring various benefits to Iris:
- We can use its [locker](https://github.com/LPCIC/coq-elpi/tree/master/apps/locker) to replace our sealing mechanism. As noticed in #527, locker might be more efficient, and it also reduce...Coq-elpi might bring various benefits to Iris:
- We can use its [locker](https://github.com/LPCIC/coq-elpi/tree/master/apps/locker) to replace our sealing mechanism. As noticed in #527, locker might be more efficient, and it also reduces the amount of boilerplate.
- We can use Elpi to create "deriving" like mechanisms, for example, for the infamous `inG` and `Σ` definitions.
- In the future we can investigate if we can use Elpi to implement parts of the Iris Proof mode more efficiently.
Coq-elpi is available in opam, and seems pretty stable. What do we think of letting Iris depend on Coq-elpi?https://gitlab.mpi-sws.org/iris/iris/-/issues/527Sealing of uPred BI layer still causes major slowdowns2023-07-04T23:30:31ZRobbert KrebbersSealing of uPred BI layer still causes major slowdownsThis problem occurs both with evarconv ("new" unification, `apply:` and friends) and tactic unification ("old" unification, `apply` and friends), see:
```coq
From iris.base_logic Require Import base_logic.
Goal ∀ (M : ucmra) (OWN : boo...This problem occurs both with evarconv ("new" unification, `apply:` and friends) and tactic unification ("old" unification, `apply` and friends), see:
```coq
From iris.base_logic Require Import base_logic.
Goal ∀ (M : ucmra) (OWN : bool → bool → uPred M), ∃ b,
let n := 10 in
(Nat.iter n (λ P, OWN b false ∗ P)%I (OWN b false)
= Nat.iter n (λ P, OWN b false ∗ P)%I (OWN b true)).
Proof.
intros M OWN. eexists _. simpl.
Fail Timeout 4 apply: eq_refl.
Fail Timeout 4 reflexivity.
generalize (@bi_sep (uPred M))=> SEP.
Fail apply: eq_refl. (* immediate *)
Fail reflexivity. (* immediate *)
Abort.
```
Until `n = 6` failure is still immediate. For more the time seems to grow exponentially. For the current `n = 10` I am not sure it ever terminates.
This example is generalized from real code where `OWN` is some ownership/representation predicate.https://gitlab.mpi-sws.org/iris/iris/-/issues/526iNext does not remove diamonds from hypotheses2023-06-29T11:00:37ZJules JacobsiNext does not remove diamonds from hypothesesiNext does not remove diamonds from hypotheses.
This feature could be useful, as otherwise you have to iMod everything.
Example:
```
From iris Require Import proofmode.tactics.
Lemma foo {PROP : bi} (P : PROP) :
◇ P ⊢ ▷ P.
Proof.
i...iNext does not remove diamonds from hypotheses.
This feature could be useful, as otherwise you have to iMod everything.
Example:
```
From iris Require Import proofmode.tactics.
Lemma foo {PROP : bi} (P : PROP) :
◇ P ⊢ ▷ P.
Proof.
iIntros "H". iNext.
Admitted.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/525iRewrite throws away non-persistent hypotheses2023-06-27T15:10:57ZRobbert KrebbersiRewrite throws away non-persistent hypotheses```coq
From iris.proofmode Require Import tactics.
Lemma foo `{!BiInternalEq PROP} (A : ofe) (x y : A) :
x ≡ y ⊢@{PROP} y ≡ x.
Proof.
iIntros "H". iRewrite "H". (* H is gone *)
```
Since internal equality is persistent, there is no...```coq
From iris.proofmode Require Import tactics.
Lemma foo `{!BiInternalEq PROP} (A : ofe) (x y : A) :
x ≡ y ⊢@{PROP} y ≡ x.
Proof.
iIntros "H". iRewrite "H". (* H is gone *)
```
Since internal equality is persistent, there is no need for this.https://gitlab.mpi-sws.org/iris/iris/-/issues/523the iInv variant with selection pattern and closing view shift doesn't work f...2023-06-09T07:59:07ZRalf Jungjung@mpi-sws.orgthe iInv variant with selection pattern and closing view shift doesn't work for accessor with variablesSee the failing test added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/937. This should be fairly easy to fix once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931 lands.See the failing test added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/937. This should be fairly easy to fix once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931 lands.https://gitlab.mpi-sws.org/iris/iris/-/issues/521Hint Cut has serious performance regressions2023-05-10T09:46:33ZRobbert KrebbersHint Cut has serious performance regressionsSee timing for !881
http://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=7f20760cdc2418aa89acbb4c9ed3138559e782fe&var-config1=build-coq.8.16.1&var-branch2=master&var-commit2=36982...See timing for !881
http://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=7f20760cdc2418aa89acbb4c9ed3138559e782fe&var-config1=build-coq.8.16.1&var-branch2=master&var-commit2=36982d7ec10c3c4d4402304f139f38512e9745a8&var-config2=build-coq.8.16.1&var-group=(.*)&var-metric=instructions
Overall 47% slower, with peaks up to 274%. This does not look good at al :disappointed:https://gitlab.mpi-sws.org/iris/iris/-/issues/519iRewrite fails when non-expansive function have multiple arguments2023-04-29T01:33:56ZDan FruminiRewrite fails when non-expansive function have multiple argumentsTried to make a meaningful title, but I think this example succinctly demonstrates the issue:
```coq
From iris.proofmode Require Import classes tactics.
From iris.si_logic Require Export bi siprop.
Require Import iris.proofmode.coq_tact...Tried to make a meaningful title, but I think this example succinctly demonstrates the issue:
```coq
From iris.proofmode Require Import classes tactics.
From iris.si_logic Require Export bi siprop.
Require Import iris.proofmode.coq_tactics.
Require Import iris.proofmode.reduction.
Program Definition constt {A B : ofe} : A -n> B -n> B := λne a b, b.
Solve All Obligations with solve_proper.
Lemma test (A B : ofe) (a1 a2 : A) (b1 : B) :
(⊢ a1 ≡ a2 → constt a1 b1 ≡ constt a2 b1 : siProp)%I.
Proof.
iIntros "H". iRewrite "H".
```
The tactic fails with:
```
Error: Tactic failure: Nothing to rewrite.
```
## The core of the issue
The problem with this is not even necessarily in Iris, but with rewriting in Coq in general. However this specific issue can be down to the following. The `iRewrite` tactic applies the lemma `tac_rewrite` with `tac_rewrite _ "H" _ _ Right` and then tries to discharge the goals. It succeeds in finding the right 'context' for rewriting (using `iRewriteFindPred`). However, the last goal is to show that this context is in fact non-expansive. In this specific case the goal is
```coq
NonExpansive (λ a0 : A, (constt a0 b1 ≡ constt a2 b1)%I)
```
The tactic `iRewrite` [tries to solve this goal](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/ltac_tactics.v#L2990) with `intros ??? ->`, which fails because of the issues with Coq rewriting.
## Potential solution
One potential solution is to change the `iRewrite` so it calls solve_proper for proving the NonExpansiveness:
```coq
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
iPoseProofCore lem as true (fun Heq =>
eapply (tac_rewrite _ Heq _ _ lr);
[pm_reflexivity ||
let Heq := pretty_ident Heq in
fail "iRewrite:" Heq "not found"
|tc_solve ||
let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
fail "iRewrite:" P "not an equality"
|iRewriteFindPred
| solve [ intros ??? ->; reflexivity | solve_proper ]
|pm_prettify; iClearHyp Heq]).
```
With this change the proof above goes through. Of course, sometimes `solve_proper` can quite a bit of time. However, this will only be a regression for goals for which `iRewrite` does not work in any case.https://gitlab.mpi-sws.org/iris/iris/-/issues/517Add notion of "allowed to be stuck" terms to WP2023-03-20T12:34:43ZRalf Jungjung@mpi-sws.orgAdd notion of "allowed to be stuck" terms to WPFor some languages it makes sense to distinguish two kinds of "stuck" terms (terms that cannot take a step and aren't a value): some are "bad" and some are "good". For instance, this can be used to model a "halt the program" primitive (t...For some languages it makes sense to distinguish two kinds of "stuck" terms (terms that cannot take a step and aren't a value): some are "bad" and some are "good". For instance, this can be used to model a "halt the program" primitive (though it will only halt the current thread due to the fixed threadpool semantics). Possibly this could also be used to model "blocking" operations.
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/825 started implementing this, but did not get completed. Still some discussion we had around that MR should be taken into account when another attempt is made at implementing this feature, in particular the [proposal for naming things](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/825#note_83734).https://gitlab.mpi-sws.org/iris/iris/-/issues/515Persistent searches can instantiate evars for instance via `big_sepL_nil_pers...2023-02-18T08:10:56ZPaolo G. GiarrussoPersistent searches can instantiate evars for instance via `big_sepL_nil_persistent`Already discussed in https://mattermost.mpi-sws.org/iris/pl/yemuustbc7gatximj8uoxq544r, but probably stuck on `Strict Resolution` not working:
```coq
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import pro...Already discussed in https://mattermost.mpi-sws.org/iris/pl/yemuustbc7gatximj8uoxq544r, but probably stuck on `Strict Resolution` not working:
```coq
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import proofmode.
Section inv.
Context `{!invGS_gen hlc Σ}.
Goal ⊢@{iProp Σ} ∃ (l : list nat) A B, A -∗ ([∗list] x ∈ l, B x) -∗ False.
iIntros. iExists _, _, _.
Set Typeclasses Debug.
iIntros.
(*
Result:
hlc: has_lc
Σ: gFunctors
invGS_gen0: invGS_gen hlc Σ
1/1
_ : [∗ list] x ∈ [], ?Goal0 x
--------------------------------------□
_ : ?Goal
--------------------------------------∗
False
*)
(* The TC trace includes the offending part:
1: looking for (Persistent ([∗ list] x ∈ ?Goal, ?Goal1 x)) with backtracking
1.1: simple apply @big_sepL_nil_persistent on
(Persistent ([∗ list] x ∈ ?Goal, ?Goal1 x)), 0 subgoal(s)
1: looking for (Affine ([∗ list] x ∈ [], ?Goal0 x)) with backtracking
1.1: simple apply @big_sepL_nil_affine on
(Affine ([∗ list] x ∈ [], ?Goal0 x)), 0 subgoal(s)
*)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/507Non-fresh identifiers in intro patterns sometimes turn the goal unprovable in...2023-02-02T17:27:43ZLennard Gähergaeher@mpi-sws.orgNon-fresh identifiers in intro patterns sometimes turn the goal unprovable instead of generating an error messageOn latest Iris master (Coq 8.16.1), I am encountering the following error:
```
From iris Require Import base.
From iris.heap_lang Require Import proofmode.
Local Lemma bla `{!heapGS Σ} :
(True : iProp Σ) -∗
(True ∗ True) -∗ True.
...On latest Iris master (Coq 8.16.1), I am encountering the following error:
```
From iris Require Import base.
From iris.heap_lang Require Import proofmode.
Local Lemma bla `{!heapGS Σ} :
(True : iProp Σ) -∗
(True ∗ True) -∗ True.
Proof.
iIntros "Ha Hc".
iDestruct "Hc" as "(%Ha & Ha)".
(* goal becomes False *)
Abort.
```
It seems like the check for freshness sometimes fails to generate an error message.
Changing the second line of the proof script to `iDestruct "Hc" as "(Hd & Ha)".` correctly generates an error message.https://gitlab.mpi-sws.org/iris/iris/-/issues/506Introducing a "step-taking" modality2023-02-16T09:40:14ZJonas KastbergIntroducing a "step-taking" modalityIn this issue I propose the introduction of a "step-taking" modality `|~>`, that captures the intuition of
"taking a step in the operational semantics", at the logical level.
The purpose of this is to allow defining ghost theories at an ...In this issue I propose the introduction of a "step-taking" modality `|~>`, that captures the intuition of
"taking a step in the operational semantics", at the logical level.
The purpose of this is to allow defining ghost theories at an abstraction-level above the program logic,
while still getting the benefits of the various later-stripping mechanisms (such as later credits) that have
been introduced in Iris.
A WIP demonstration of the modality can be found in !887.
A tl;dr is:
- Presence of multiple laters can reduce intuition behind ghost theory (and in some cases make them impossible to state (see below))
- Iris has means of stripping such multiple laters during every physical step
- One can capture the intuition of having to taking a physical step via a modality (`|~>`)
- One can then use this modality in ghost rules
Ultimately we would obtain the following:
```
TCEq (to_val e) None → E2 ⊆ E1 →
|~{E1,E2}~> P -∗
WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗
WP e @ s; E1 {{ Φ }}.
```
Ghost theory rules that were usually of the form `P -* |={E}=> Q`
will now simply have the form `P -* |~{E}~> Q`.
Now for a more detailed explanation of the benefits of this, and limitations of existing solutions, see the discussion below.
Since the addition of the later credits (and other similar later-stripping procedures),
it is now possible to strip multiple laters during a single (physical) step of the operational semantics.
This let us build nice abstractions for some ghost abstractions to hide the laters from the user (e.g. nested invariants).
However, some ghost theories are not able to fully benefit from this extension.
Consider the following ghost theory that allows bidirectional transfer of some resources `P`:
- There are two fragments that each track the resource to be transferred `P`.
- There is a context which is indexed by two numbers, that tracks how many copies of `P` is in transit in either direction.
- Resources are transferred from one side by incrementing the respective number.
- Resources are received from one side by decrementing the other number.
- Sending a resource from one side requires stripping an amount of laters corresponding to the number of resources in transit towards you (i.e. from the other side).
The later requirement is simply instrumented here for the sake of the example.
Something more realistic, which has the later requirement is the Actris Ghost Theory (pg. 45 of https://iris-project.org/pdfs/2022-lmcs-actris2-final.pdf).
We can make this concrete with the following definitions and rules:
- There are three resources `my_ctx γ n m`, `my_frag_l γ P`, and `my_frag_r γ P`.
- There are five rules:
```
1. |- |==> ∃ γ, my_ctx γ 0 0 * my_frag_l γ P * my_frag_r γ P
2. |- my_ctx γ n m * my_frag_l γ P * P ==* ▷^m my_ctx (S n) m * my_frag_l γ P
3. |- my_ctx γ n m * my_frag_r γ P * P ==* ▷^n my_ctx n (S m) * my_frag_r γ P
4. |- my_ctx γ n (S m) P * my_frag_l γ P ==* ▷ my_ctx n m * my_frag_l γ P * P
5. |- my_ctx γ (S n) m P * my_frag_r γ P ==* ▷ my_ctx n m * my_frag_r γ P * P
```
Rule 2. and 3. shows how sending a resources requires stripping multiple laters.
It is possible to employ this ghost theory for a program, thanks to the new later-stripping mechanisms.
However, imagine the following.
We build an abstraction on top of the ghost theory, to construct a new ghost theory, in which we _hide_ the context (and thereby the numbers related to how many steps we need to strip).
In the new ghost theory we have the following:
- There is a fragment for either side `my_frag_l' γ n m P` and `my_frag_r' γ n m P`,
that govern how many times a they have sent a resource (n), and how many times they have received one (m).
- There are two additional fragments `my_idx_l γ i`, `my_idx_r γ i` that are duplicable evidence of how many resources have been sent in either direction (in total)
- It is imperative that either fragment does not know about the others counter, as we wish full separation between them.
This ghost theory abstraction is achievable by putting `my_ctx` in an invariant,
that is included inside each new fragment,
along with ghost state to tie the invariant together with the former local fragment.
In this case, we cannot create a ghost theory, as we do not know the number of laters to strip, outside of the invariant!
Imagine the following rule corresponding to rule 2.:
```
my_frag_l' γ n m P * P ==* ▷^??? my_frag_l' γ (S n) m P * my_idx_l γ n
```
In fact, the only possible rule is something like the following (mask and atomicity details omitted):
```
my_frag_l' γ n P -* P -*
WP e { v. (my_frag_l' γ (S n) P * my_idx_l γ n)-* Φ v } -*
WP e { Φ }
```
This is achieved by adding fragments of the later-stripping mechanism to the internal invariant,
which then lets us strip the appropriate amount of laters in the context of a WP.
In particular, the WP lets us access the internal `state_interp`, which in turn includes the authoritative
parts of the later-stripping mechanisms.
However, this rule is very unsatisfactory, as we are now working at the level of the WP, instead of a higher level of abstraction.
As such, I propose the addition of a "step-taking" modality `|~>`.
Essentially, it would frame the later-stripping mechanism governed by the state interpretation,
while guaranteeing that it is updated appropriately.
Intuitively, it captures the notion of "taking a step" in the operational semantics.
As such, the modality would enjoy the following rule (mask and atomicity details omitted):
```
|~> Q -*
WP e { v. Q -* Φ v } -*
WP e { Φ }
```
This would allow the aforementioned ghost theory rule to be expressed as follows:
```
my_frag_l' γ n m P * P -* |~> my_frag_l' γ (S n) m P * my_idx_l γ n
```
This now preserves a higher level of abstraction, by reading as:
"I can give up my resources, _when taking a (physical) step_, to obtain the new resources".
As I do not have a deep understanding of the later credits, I cannot give a precise definition of `|~>`,
although I discussed something similar with @simonspies at the Iris Workshop 2022, who may have a good suggestion.
In the case of the simple later-stripping mechanism in HeapLang,
I have defined and mechanised the lemmas for the following in Coq:
```
|~{E1,E2}~> P ≜
∀ n, steps_auth n ={E1,E2}=∗
(steps_auth n ∗ (|={∅}▷=>^(S n) (steps_auth (S n) -∗
steps_auth (S n) ∗ |={E2,E1}=> P)))
```
For the application level, one can then determine the lower bound of `n` with the local fragments
kept inside the ghost theory, along with the given `steps_auth n`, to conclude that enough laters
can be stripped.
The `steps_auth` fragment can then be given back to resolve the left conjunct.
After the ghost step has been taken, the updated `steps_auth` can be obtained, to reflect its updates
in the local ghost state.
The weakest precondition rule can be proven, as we simply give ownership of the internal `steps_auth n`
to the `P -* |~> Q` assumption, to unify the amount of laters that can be stripped `n`.
Similarly, we give the updated `steps_auth (S n)` to resolve the final update in the step-taking modality.
I managed to prove all of the following lemmas in Coq, given my above definition of the modality:
```
TCEq (to_val e) None → E2 ⊆ E1 →
|~{E1,E2}~> P -∗
WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗
WP e @ s; E1 {{ Φ }}.
```
```
↑N ⊆ E →
my_frag_l' γ n m P -∗ P -∗
step_update E (E ∖ ↑N) (my_frag_l' γ (S n) m P ∗ my_idx_l γ n).
```
This in turn let me derive the above "ghost" rule that worked at the level of the weakest precondition:
```
my_frag_l' γ n P -* P -*
WP e { v. (my_frag_l' γ (S n) P * my_idx_l γ n)-* Φ v } -*
WP e { Φ }
```
EDIT:
Some refactoring, and added a better overview in the top
EDIT:
Added reference to MR
EDIT:
After further looking into the existing lemmas regarding later stripping in HeapLang, a suitable definition of the modality might already be found in https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/program_logic/weakestpre.v#L350
That is:
```
Definition step_update E1 E2 P : iProp Σ :=
∃ n, (∀ σ ns κs nt, state_interp σ ns κs nt ={E1,∅}=∗
⌜n ≤ S (num_laters_per_step ns)⌝) ∧
(|={E1∖E2,∅}=> |={∅}▷=>^n |={∅,E1∖E2}=> P).
```
With this, the aforementioned rule can even be changed to simply use the modality instead of the in-line
proposition.
Proving rules for this definition seems feasible too, and compositionality of the modality should work out.
EDIT: The above is not enough, as it does not capture how the ghost theory may be updated based on the new state of the state interpretation, but it does give an impression of how something like this modality was already in place in Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/505wp_apply Bad error message when framing in spec pattern fails2023-01-11T15:46:28ZRalf Jungjung@mpi-sws.orgwp_apply Bad error message when framing in spec pattern failsConsider this test case:
```
Lemma frame_fail_test e P Q :
(P -∗ WP e {{ _, True }}) -∗
(Q -∗ WP e {{ _, True }}).
Proof.
iIntros "He HP". wp_apply ("He" with "[$HP]").
```
It prints `Error: No applicable tactic.`, which ...Consider this test case:
```
Lemma frame_fail_test e P Q :
(P -∗ WP e {{ _, True }}) -∗
(Q -∗ WP e {{ _, True }}).
Proof.
iIntros "He HP". wp_apply ("He" with "[$HP]").
```
It prints `Error: No applicable tactic.`, which is not a very useful error message. I would expect it to tell me that `HP` could not be framed.https://gitlab.mpi-sws.org/iris/iris/-/issues/504iEval fails in strange ways when tactic creates new goals2023-01-09T15:03:50ZRalf Jungjung@mpi-sws.orgiEval fails in strange ways when tactic creates new goalsUsing `iEval rewrite foo` when this opens new goals with side-conditions fails in very strange ways. The reason is that IPM runs `unfold x; reflexivity` on *all* resulting goals.
The tricky part in resolving this will be figuring out wh...Using `iEval rewrite foo` when this opens new goals with side-conditions fails in very strange ways. The reason is that IPM runs `unfold x; reflexivity` on *all* resulting goals.
The tricky part in resolving this will be figuring out which goal is the "original" one (side-conditions could be added before or after). But at least this simple cases can be improved a lot by checking whether `x` is even present in the goal.https://gitlab.mpi-sws.org/iris/iris/-/issues/500Boolean parameters to `MaybeFrame` and other proofmode classes are hard to read2022-12-07T10:39:07ZIke MulderBoolean parameters to `MaybeFrame` and other proofmode classes are hard to readThe `MaybeFrame` class used by the `iFrame` tactic is defined as follows:
```
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been...The `MaybeFrame` class used by the `iFrame` tactic is defined as follows:
```
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : □?p R ∗ Q ⊢ P.
```
However, as noted in !872, this `progress` argument becomes quite hard to read in instances like
`TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.`
A suggestion was to use a custom two-constructor inductive, something like
`Inductive progress_indicator := DidSomething | DidNothing.`.
Operations like `&&` and `||` would then need to be added for this inductive as well.
(@robbertkrebbers mentioned the `MaybeFrame` instances might be removed someday, so that the `MaybeFrame` class would become obsolete. That would also fix this problem.)https://gitlab.mpi-sws.org/iris/iris/-/issues/499Consistent error messages for internal IPM failures2023-04-12T14:51:54ZIke MulderConsistent error messages for internal IPM failuresThere are a couple of places where an IPM tactic could theoretically fail in strange cases.
The treatment of such cases is not consistent.
When defining a tactic in `ltac_tactics`, sideconditions of a lemma from `coq_tactics` that sho...There are a couple of places where an IPM tactic could theoretically fail in strange cases.
The treatment of such cases is not consistent.
When defining a tactic in `ltac_tactics`, sideconditions of a lemma from `coq_tactics` that should be always be solvable by a single tactic `tac`:
- are sometimes just handled with `tac`
- are sometimes handled as `tac || fail "some error message which might make clear that this should not happen"`
Some examples are in [iInduction](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/ltac_tactics.v#L2307), [iLöb](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/ltac_tactics.v#L2702) and [iPoseProofCoreLem](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/ltac_tactics.v#L869).
As discussed [here](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/872#note_86860), it would be nice if such cases were handled consistently.
A possible fix might look as follows:
```
Ltac iInternalFailMsg :=
idtac "Iris encountered an internal error! This is very bad!";
idtac "Please report a bug at https://gitlab.mpi-sws.org/iris/iris/-/issues ".
Ltac iExampleTac.
let H := constr:(I) in
iInternalFailMsg; fail "iTest: Something with" H "is off"
```
prepending `iInternalFailMsg` to all such `fail` statements.