WIP: Step Update modality demonstration

Implementation of the step-taking modality discussed in #506.

The modality is used in the following MR of the Actris development: actris!30

mentioned in issue #506

added 41 commits

• 072e75c0...243a22e9 - 40 commits from branch iris:master
• ee6958e5 - WIP: Step Update modality demonstration

Compare with previous version

added 1 commit

• a2ef967c - Generalised the step update modality to work for all program logics

Compare with previous version

mentioned in merge request actris!30

changed the description

added 1 commit

• 1cc547f4 - WIP: Proofmode support

Compare with previous version

added 1 commit

• 7a83b45d - Made instances global and proved a weakening rule

Compare with previous version

added 1 commit

• 32cc4434 - Removed view shifts from step mod, improved proofmode, and cleanup

Compare with previous version

added 1 commit

• 9afe85b3 - Better definition of step modality

Compare with previous version

@jihgfee this feels like something that can be a third-party library. As we discussed ;) I am not convinced that this is a sufficiently general abstraction that it needs to live in core Iris.

So I think we should close this MR -- sorry.

I agree that it's probably best to close this.

One of the applications is the Actris ghost theory. But once you apply that in the context of logically atomic triples (as the OOPSLA paper with Thomas), I don't think you want the Actris interface with step update modalities because logically atomic triples don't contain step update modalities (and likely never will).

closed