Diaframe issueshttps://gitlab.mpi-sws.org/iris/diaframe/-/issues2023-10-11T10:56:16Zhttps://gitlab.mpi-sws.org/iris/diaframe/-/issues/18Improving recursive inspection of hypotheses for hint generation2023-10-11T10:56:16ZIke MulderImproving recursive inspection of hypotheses for hint generationCurrently, to generate a good BiAbd/Abduct instance for application, we look beneath literal connectives until we can't.
Then, we start looking for `AtomIntoExist`, `AtomIntoWand`, etc instances.
We could improve this by having one clas...Currently, to generate a good BiAbd/Abduct instance for application, we look beneath literal connectives until we can't.
Then, we start looking for `AtomIntoExist`, `AtomIntoWand`, etc instances.
We could improve this by having one class, `AtomIntoConnective A C : atom_into_connective := A ⊢ C` where `A` should be an atom, and `C` an arbitrary connective. This would give us additional expressive power:
- For one, it allows the following instance: `AtomIntoConnective (if b then P else Q) ((P ∗ (b = true)) ∨ (Q ∗ (b = false))`. This may be very nice for closing atomic updates.
- It also reduces the number of available classes.
- We need to think about how we could still support the extension of proving literal wands, if available.
- In the future, maybe we could write some smart Ltac to autogenerate such recursive inspections for arbitrary user-defined fixpoints.https://gitlab.mpi-sws.org/iris/diaframe/-/issues/13Getting rid of CPS style Mergable classes2022-08-24T14:54:30ZIke MulderGetting rid of CPS style Mergable classesWe currently have CPS-style typeclasses for merging hypotheses: `MergablePersist` and `MergableConsume`,
which are somewhat awkward to write and prove.
They were implemented this way since I initially suspected the naive approach would s...We currently have CPS-style typeclasses for merging hypotheses: `MergablePersist` and `MergableConsume`,
which are somewhat awkward to write and prove.
They were implemented this way since I initially suspected the naive approach would scale badly in larger Iris proof environments.
On second thought, I was not so sure of this anymore, since surely `TCEq`-hacks must be slower than native typeclass stuff.
Additionally, the `TCEq` stuff causes bigger proof terms, which also negatively affects performance.
After trying and investigating in [ci/simplify-merge](../../tree/ci/simplify-merge), we know now the following:
- CPS style indeed has higher constant time cost, which makes a difference of [up to 3% in examples](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=diaframe&var-branch1=ci%2Fsimplify-merge&var-commit1=896ebc8a12bd931759ede054de600256d650f30c&var-config1=build-examples-coq.8.15.1&var-branch2=master&var-commit2=3466a301198a859e59ca819d39967c914b5edf47&var-config2=build-examples-coq.8.15.1&var-metric=instructions&var-group=(.*)).
- CPS style scales __much__ better for larger environments. The main example that encounters this is [rwlock_ticket_bounded](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=diaframe&var-branch1=ci%2Fsimplify-merge&var-commit1=896ebc8a12bd931759ede054de600256d650f30c&var-config1=build-examples-coq.8.15.1&var-branch2=master&var-commit2=3466a301198a859e59ca819d39967c914b5edf47&var-config2=build-examples-coq.8.15.1&var-metric=instructions&var-group=(.*)). This one gets 14% slower with the naive implementation. If one inspects the merging of the auth and frag own tokens in, for example, `acquire_reader_int_spec`, we see that the `solveStep` responsible for this takes `0.7` seconds, and `0.2` seconds if all but the relevant hypothesis are cleared (keeping 1 of 5). In contrast, the CPS style implementation takes `0.3` seconds, `± 0.02` if 4 extra hypotheses are present.
The total build time decreases with 0.6% with the naive implementation. I do not consider this enough to take its bad scaling for granted.
It would be nice to use the naive implementation, or maybe have notation and tactics that allow users to easily provide instances, as if the naive implementation was used.
Alternatively, one could delve in Coq's source code and investigate why typeclass resolution gets slow in this example. One of the strange things is that
`first [ simple apply instance_1 | ... | simple apply instance_n]` is also much slower than `iSolveTC`. What causes this slowdown?https://gitlab.mpi-sws.org/iris/diaframe/-/issues/12Consistent variable and hypothesis naming2022-03-29T11:23:53ZIke MulderConsistent variable and hypothesis namingChanges in the implementation and in the available hints can cause changes in variable names, which is unwanted.
Different versions of Iris have also sometimes caused different hypotheses names, also unwanted.
Idea to get consistent hyp...Changes in the implementation and in the available hints can cause changes in variable names, which is unwanted.
Different versions of Iris have also sometimes caused different hypotheses names, also unwanted.
Idea to get consistent hypotheses names: don't use the IPM environment, instead use a custom list environment, and change back to the IPM env after a tactic finishes.
Idea to get consistent variable names: look at how IPM does it for foralls. Otherwise try typeclasses to generate 'good' default names..?https://gitlab.mpi-sws.org/iris/diaframe/-/issues/11Performance improvements2022-02-16T10:38:34ZIke MulderPerformance improvementsSome points where I think performance can still be improved:
- *`AsSolveGoal` TC search is slow.* this is now improved
- *Definitions like `IntroduceHyp` are not sealed off.* Seems to have no effect on performance though:
[with sealed...Some points where I think performance can still be improved:
- *`AsSolveGoal` TC search is slow.* this is now improved
- *Definitions like `IntroduceHyp` are not sealed off.* Seems to have no effect on performance though:
[with sealed definitions](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170877) vs [without sealed definitions](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170827).
- Stripping `□` of persistent hypothesis on introduction is slow?
- *Dedicated typeclass for `∀.. (tt: TT), ...`* Has no effect on performance:
[with dedicated typeclass](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170928) vs [without dedicated typeclass](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170827). But TC search debug output is more readable.
Continued: in the end there was a (small) performance improvement, just a bit later: [this](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170937) vs [this](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170941). But quite possibly this was due to `rewrite /term` being slower than `unfold term`.https://gitlab.mpi-sws.org/iris/diaframe/-/issues/9Replace FindLocalUpdate with something better2021-06-25T08:18:09ZIke MulderReplace FindLocalUpdate with something betterIt would be nice if we can get some stronger guarantees when performing an update from `•a·○b` to `•a'·○b'`.
Right now `FindLocalUpdate` does not attempt anything of that sort: it takes the `○b` as an additional input to compute the `○b'...It would be nice if we can get some stronger guarantees when performing an update from `•a·○b` to `•a'·○b'`.
Right now `FindLocalUpdate` does not attempt anything of that sort: it takes the `○b` as an additional input to compute the `○b'` from. However, it should be possible to compute a `○b` that is minimal in some way! Some scratches of attempts:
```
Class CmraBiAbd {A : cmra} (x x' y y' : A) (φ : Prop) := {
cmra_biabd_valid : φ → x ⋅ y ~~> x' ⋅ y';
(* y is the minimum or there is no minimum *)
cmra_biabd_req_1 : φ → ∀ z z', x ⋅ z ~~> x' ⋅ z' → ((z ≼ y → y ≼ z) ∨ ∃ k k', k ≼ z ∧ x ⋅ k ~~> x ⋅ k');
(* y' is the maximum for y *)
cmra_biabd_req_2 : φ → x ⋅ y ~~> x' ⋅ y' → ∀ z', x ⋅ y ~~> x' ⋅ z' → y' ≼ z' → z' ≼ y';
}.
(* not sure if cmra_biabd_req_2 is provable, but the first two we can prove for the following lemma: *)
Lemma auth_subtract_l {A : ucmra} (x y r : A) φ :
UcmraSubtract y x φ r →
CmraBiAbd (● x) (● y) ε (◯ r) (φ ∧ ✓ y).
Proof.
```https://gitlab.mpi-sws.org/iris/diaframe/-/issues/7Typeclasses for simplifying ✓2021-06-23T09:40:51ZIke MulderTypeclasses for simplifying ✓It would be nice to have a typeclass which simplifies ✓ x for x in a given RA into its most basic representation.
- Should this live in BI..?It would be nice to have a typeclass which simplifies ✓ x for x in a given RA into its most basic representation.
- Should this live in BI..?https://gitlab.mpi-sws.org/iris/diaframe/-/issues/5Remove & replace older experiments2022-02-11T15:53:53ZIke MulderRemove & replace older experiments- [x] Replace `delay_choice.made_choice` with some dedicated `DestructHint` type or similar.
- [x] Change `ReductionStep`s to no longer rely on lists: we don't use that anymore.
- [ ] Remove `proofstep` stuff?- [x] Replace `delay_choice.made_choice` with some dedicated `DestructHint` type or similar.
- [x] Change `ReductionStep`s to no longer rely on lists: we don't use that anymore.
- [ ] Remove `proofstep` stuff?