Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2024-03-24T14:54:23Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/569Add some sort of rule for `own ∧ own`2024-03-24T14:54:23ZRalf Jungjung@mpi-sws.orgAdd some sort of rule for `own ∧ own`The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v)...The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v).)
Amin suggested [something similar](https://mattermost.mpi-sws.org/iris/pl/tcsex43cn7d5ij5qwkk39ftd7h) a long time ago.
Not sure which formulation works best, but we should have something like that. :)
Whatever the rule is, it should be strong enough to prove things like
```
Lemma pointsto_and_sep (l1 l2:loc) (v1 v2:val) :
l1 ≠ l2 ->
l1 ↦ v1 ∧ l2 ↦ v2 -∗
l1 ↦ v1 ∗ l2 ↦ v2.
Lemma pointsto_and_eq l x y :
l ↦ x ∧ l ↦ y -∗ ⌜x = y⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/567[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-19T16:06:15ZRomain Tetley[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.0`.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
7c5ce0d556f4e03f27ddc6463462bf4040f5103d on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/405https://gitlab.mpi-sws.org/iris/iris/-/issues/568[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-18T16:04:50ZRomain Tetley[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.0`.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/405https://gitlab.mpi-sws.org/iris/iris/-/issues/566Frame instance for multiset union can interact badly with instantiating exist...2024-03-06T12:32:05ZIke MulderFrame instance for multiset union can interact badly with instantiating existential quantifiersThis is problematic:
```coq
From iris.proofmode Require Import proofmode.
Section test.
Context {PROP : bi}.
Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
Proof.
iIntros "HP".
Fail ...This is problematic:
```coq
From iris.proofmode Require Import proofmode.
Section test.
Context {PROP : bi}.
Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
Proof.
iIntros "HP".
Fail Timeout 2 iFrame "HP".
Abort.
End test.
```
This happens because there is the following frame instance for framing inside a multiset union:
```coq
Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
```
In our `multiset_problem` example, this instance will instantiate the evar `?X` with a union `?X1 ⊎ ?X2`. After two more steps, we encounter almost the same goal, and `Frame` instance search will loop.
The instances for `[∗ list]` do not suffer from this problem, since they are guarded by an `IsCons` or `IsApp` typeclass with proper `Hint Mode`s.
To fix this, we could use the same approach: guard `frame_big_sepMS_disj_union` with a new class `IsUnion`.
Encountered by @janno @lepigrehttps://gitlab.mpi-sws.org/iris/iris/-/issues/565Unsound instantiation of existentials by `iFrame` on persistent facts2024-03-05T17:01:36ZRodolphe LepigreUnsound instantiation of existentials by `iFrame` on persistent facts@janno and I found that the new support for existential instantiation in `iFrame` (from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1017) can sometimes instantiate existential quantifiers too eagerly for persistent facts.
Repr...@janno and I found that the new support for existential instantiation in `iFrame` (from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1017) can sometimes instantiate existential quantifiers too eagerly for persistent facts.
Reproducing example:
```coq
Require Import iris.bi.interface.
Require Import iris.proofmode.proofmode.
Goal ∀ (PROP : bi) (P : nat -> PROP),
□ P 0 ⊢ P 0 ∗ (∀ n : nat, P n -∗ ∃ n, P n ∗ ⌜n = 1⌝).
Proof.
iIntros (??) "#$".
(*
PROP : bi
P : nat → PROP
============================
_ : P 0
--------------------------------------□
∀ x : nat, P x -∗ ⌜0 = 1⌝
*)
Abort.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/563Add QuickPersistent and use it in frame_impl (and maybe elsewhere)2024-03-02T09:13:20ZRalf Jungjung@mpi-sws.orgAdd QuickPersistent and use it in frame_impl (and maybe elsewhere)Generally in framing we try to avoid typeclasses that walk the entire term, like `Affine` or `Absorbing`. We have `Quick*` variants of these typeclasses instead.
However, we don't have `QuickPersistent`, and `frame_impl` uses `Persisten...Generally in framing we try to avoid typeclasses that walk the entire term, like `Affine` or `Absorbing`. We have `Quick*` variants of these typeclasses instead.
However, we don't have `QuickPersistent`, and `frame_impl` uses `Persistent`. We should fix that.https://gitlab.mpi-sws.org/iris/iris/-/issues/457"-" in selection patterns2024-02-26T16:06:50ZRalf Jungjung@mpi-sws.org"-" in selection patternsIt would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.It would be really useful to support "-" in selection patterns, such that one can do `iClear "- H1 H2 H3"`, like one can with regular Coq `clear`.https://gitlab.mpi-sws.org/iris/iris/-/issues/564Make iFrame also instantiate telescopic existential quantifiers2024-02-19T09:40:25ZIke MulderMake iFrame also instantiate telescopic existential quantifiersFollow up on !1017: it should be possible to extend the technique for instantiating existential quantifiers to also work on telescopic quantifications `∃.. x`.
The initial attempt worked partly:
```
Global Instance frame_texist {TT : t...Follow up on !1017: it should be possible to extend the technique for instantiating existential quantifiers to also work on telescopic quantifications `∃.. x`.
The initial attempt worked partly:
```
Global Instance frame_texist {TT : tele@{bi.Quant}} p R (Φ : TT → PROP)
(C : tele@{bi.Quant}) (g : C → TT) (Ψ : C → PROP) Q :
(∀ c, FrameExistRequirements p R Φ (g c) (Ψ c)) →
TCCbnSimplTele (∃.. c, Ψ c)%I Q →
Frame p R (∃.. x, Φ x) Q.
Proof.
move=> H HQ. rewrite /FrameTExists /Frame (bi_texist_exist Φ).
by eapply frame_exist.
Qed.
```
but this turns a telescopic quantifier into a regular one whenever things get framed beneath it.
We did not yet figure out a nice way to fix this.https://gitlab.mpi-sws.org/iris/iris/-/issues/551`iSpecialize` fails on `bi_forall` without eta expansion2024-02-16T16:30:51ZRobbert Krebbers`iSpecialize` fails on `bi_forall` without eta expansion```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- wit...```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- without eta expansion *)
Lemma bar {PROP : bi} {A} (P : A → PROP) x :
bi_forall P ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
(* Tactic failure: iSpecialize: cannot instantiate (∀ y, P y)%I with x. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/562Repeatedly failing `Affine` typeclass search can slow down `iFrame`2024-02-14T15:06:17ZIke MulderRepeatedly failing `Affine` typeclass search can slow down `iFrame`During patching iron for !1017, I ran into a situation similar to this (exaggerated to make effect more visible):
```
Lemma test_iFrame_affinely_3 P Q :
let i := 50 in (* controls amount of [Affine] searches *)
let j := 50 in (* con...During patching iron for !1017, I ran into a situation similar to this (exaggerated to make effect more visible):
```
Lemma test_iFrame_affinely_3 P Q :
let i := 50 in (* controls amount of [Affine] searches *)
let j := 50 in (* controls hardness of an individual [Affine] search*)
let rep :=
fun n R T =>
([∗ list] P ∈ ((repeat R n) ++ [T]), P)%I
in
rep j (<affine> Q) Q ⊢ rep i (<affine> P) (<affine> P) ∗ rep j (<affine> Q) Q.
Proof.
iIntros (i j rep) "Hrep".
time iFrame "Hrep". (* 3.2 seconds *)
Undo 1.
time (iSplitR; last iFrame). (* 0.005 seconds *)
Abort.
```
The problematic `Frame` instance is [`frame_affinely`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/class_instances_frame.v?ref_type=heads#L202), which attempts to show that the framed hypothesis is `Affine` whenever the `<affine>` modality occurs in the goal. One possible solution is to replace the `Affine` condition with `QuickAffine` in `frame_affinely`:
```
Lemma frame_affinely_alt p R P Q Q' :
TCOr (TCEq p true) (classes_make.QuickAffine R) →
Frame p R P Q → classes_make.MakeAffinely Q Q' →
Frame p R (<affine> P) Q'. (* Default cost > 1 *)
Proof.
rewrite /classes_make.QuickAffine.
case; apply _.
Qed.
Remove Hints class_instances_frame.frame_affinely : typeclass_instances.
Existing Instance frame_affinely_alt.
(* speeds up the first iFrame to 0.3 seconds *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/560Fix the future-coercion-class-field warnings2024-02-06T08:38:06ZRalf Jungjung@mpi-sws.orgFix the future-coercion-class-field warningsWe are getting tons of these, and I expect even more in our reverse dependencies. It might be worth having a script for that.
The following little script by Tej that we used to add all the missing `Global` might be a good starting point...We are getting tons of these, and I expect even more in our reverse dependencies. It might be worth having a script for that.
The following little script by Tej that we used to add all the missing `Global` might be a good starting point:
```
#!/usr/bin/env python3
import sys
import re
error_re = re.compile(r"""^File "(?P<file>[^"]*)", line (?P<line>[0-9]+), characters .*:""")
for line in map(str.rstrip, sys.stdin):
m = error_re.match(line)
if m:
file, line = m.group("file"), m.group("line")
print(f"sed -i '{line}s/^/Global /' '{file}'")
```https://gitlab.mpi-sws.org/iris/iris/-/issues/561Use `#[local] field ::` to make `inG` instances local2024-02-05T17:23:10ZRobbert KrebbersUse `#[local] field ::` to make `inG` instances localNow that support for Coq 8.17 has been dropped, we can make use of `#[local] field ::` in `Class` declarations ~~which by default appears to be `Local`~~. This would be a better fix for https://gitlab.mpi-sws.org/iris/iris/-/merge_reques...Now that support for Coq 8.17 has been dropped, we can make use of `#[local] field ::` in `Class` declarations ~~which by default appears to be `Local`~~. This would be a better fix for https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/780
See also https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1030https://gitlab.mpi-sws.org/iris/iris/-/issues/559iApply applies lemmas without resolving typeclass constraints2024-01-10T15:37:42ZRalf Jungjung@mpi-sws.orgiApply applies lemmas without resolving typeclass constraintsConsider this example:
```
From iris.algebra Require Import excl.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import lib.iprop lib.own.
From iris.prelude Require Import options.
Class spin_lockG Σ := LockG...Consider this example:
```
From iris.algebra Require Import excl.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import lib.iprop lib.own.
From iris.prelude Require Import options.
Class spin_lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
Local Existing Instance lock_tokG.
Definition spin_lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Global Instance subG_spin_lockΣ {Σ} : subG spin_lockΣ Σ → spin_lockG Σ.
Proof. solve_inG. Qed.
Lemma test `{!spin_lockG Σ} (P Q : iProp Σ) :
P -∗ P -∗ Q.
Proof. Admitted.
Lemma test2 {Σ} (P Q : iProp Σ) :
P -∗ Q.
Proof.
iIntros "HP".
iApply (test with "HP").
```
I would expect the `iApply` to fail, since the `test` lemma needs `spin_lockG` which is not present. Instead, it succeeds and creates a shelved goal. This is a pretty bad user experience since the shelved goal is easy to miss, so it is likely that one will continue in this proof not realizing that one has applied an impossible lemma. This can also cause very strange follow-on effects since the unresolved evar can cause unification failures and other hard-to-diagnose issues.https://gitlab.mpi-sws.org/iris/iris/-/issues/558wp_apply: bad errors when the term is not found or the lemma is used wrong2024-01-09T12:16:04ZRalf Jungjung@mpi-sws.orgwp_apply: bad errors when the term is not found or the lemma is used wrongConsider this test case:
```
From iris.algebra Require Import excl frac_auth numbers.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import lib.token lib.inva...Consider this test case:
```
From iris.algebra Require Import excl frac_auth numbers.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import lib.token lib.invariants lib.own.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation adequacy lib.par.
From iris.prelude Require Import options.
Definition newlock : val. Admitted.
Definition acquire : val. Admitted.
Definition release : val. Admitted.
Section test.
Context `{!heapGS_gen hlc Σ}.
Notation iProp := (iProp Σ).
Context (newlock_spec : ∀ R, {{{ R }}} newlock #() {{{ RET #(); True }}}).
Context (acquire_spec : ∀ R, {{{ R }}} acquire #() {{{ RET #(); True }}}).
Lemma test (P : iProp) :
P -∗ WP newlock #() {{ _, True }}.
Proof.
iIntros "HP".
Fail wp_apply acquire_spec.
Fail wp_apply (newlock_spec True%I with "HP").
```
Both of these `wp_apply` fail by just saying "No applicable tactic", which is a pretty bad user experience.
The first should fail saying something about "acquire" not having been found in the goal.
The second should fail the same way `iApply (newlock_spec True%I with "HP")` fails in that situation:
> `iSpecialize: cannot instantiate (True -∗ ▷ (True -∗ ?Goal #()) -∗ WP newlock #() {{ v, ?Goal v }})%I with P.`https://gitlab.mpi-sws.org/iris/iris/-/issues/554This is a test2023-11-20T13:53:59ZRalf Jungjung@mpi-sws.orgThis is a testjust ignore mejust ignore mehttps://gitlab.mpi-sws.org/iris/iris/-/issues/553This is a test2023-11-20T13:53:23ZRalf Jungjung@mpi-sws.orgThis is a testjust ignore mejust ignore mehttps://gitlab.mpi-sws.org/iris/iris/-/issues/552Consider merging "examples" into this repository2023-11-20T13:53:20ZRalf Jungjung@mpi-sws.orgConsider merging "examples" into this repositoryWe now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one reposito...We now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one repository less that Robbert and me have to port changes to.
- People trying to fix Coq CI have one repository less to worry about.
Downsides:
- `make` will require Autosubst to fully work
- `make` in Iris will take quite a bit longer
- CI will take longer before a package is published in opam
I don't have a very strong opinion on this. Very rarely I make changes that break something in iris/examples in subtle ways and debugging that would be much easier in a mono repo. But most of the time the overhead from having two repositories is not so bad, and it's nice that people don't have to install Autosubst to make `make` work.https://gitlab.mpi-sws.org/iris/iris/-/issues/550Prevent iFrame from unfolding definitions?2023-11-13T10:09:58ZRalf Jungjung@mpi-sws.orgPrevent iFrame from unfolding definitions?Currently, iFrame unfolds at least some definitions. One can opt-out of that by making the definitions typeclasses opaque or adding `tc_opaque`, but many people don't know to do that and experience large `iFrame` slowdowns when piling up...Currently, iFrame unfolds at least some definitions. One can opt-out of that by making the definitions typeclasses opaque or adding `tc_opaque`, but many people don't know to do that and experience large `iFrame` slowdowns when piling up abstractions.
It'd be good to investigate whether we can somehow make definition-unfolding for `iFrame` be opt-in rather than opt-out.
One possibility is to use `Hint Extern`, [like `SetUnfold`](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/sets.v#L145). However, that does not allow users to opt-in.
Another possibility would be to use a different hint database where constants are by default opaque.
Either way this is a massive breaking change and would have to be carefully evaluated.https://gitlab.mpi-sws.org/iris/iris/-/issues/549Seal HeapLang points-to2023-11-11T09:36:07ZRobbert KrebbersSeal HeapLang points-toHeapLang defines a notation for the `gen_heap` points-to. This notation has two purposes (1) use `Some` for the value and (2) fix the arguments to the HeapLang `val` so that type inference and scopes work better.
It's currently quite ea...HeapLang defines a notation for the `gen_heap` points-to. This notation has two purposes (1) use `Some` for the value and (2) fix the arguments to the HeapLang `val` so that type inference and scopes work better.
It's currently quite easy to accidentally break abstraction. It's also easy to forget to lift a `gen_heap` lemma because it might work accidentally for the notation.
We thus should make the HeapLang points-to a definition and seal it.
See also the discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/960#note_98626https://gitlab.mpi-sws.org/iris/iris/-/issues/438Use HB.lock(-like) sealing2023-11-10T15:51:29ZRalf Jungjung@mpi-sws.orgUse HB.lock(-like) sealinghierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a dif...hierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a difference in practice.
Quoting from https://github.com/math-comp/hierarchy-builder/wiki/Locking:
```
HB.lock Definition new_concept := 999999.
Lemma test x : new_concept ^ x ^ new_concept = x ^ new_concept ^ new_concept.
Proof.
Time Fail reflexivity. (* takes 0s *)
rewrite new_concept.unlock.
Time Fail reflexivity. (* takes 7s, the original body is restored *)
Abort.
```
This is exactly the kind of locking API I always wanted: just adding a keyword in front of the `Definition`, done. This would make it a no-brainer to seal basically every `iProp` that our reusable libraries export.
TODO:
- Check if this actually works in Iris
- Decide if we want to do this, and how -- are we okay with a dependency on hierarchy-builder?