In !595 (merged) the Iris program logic was extended with capability for stripping an amount of laters per step relative to the amount of steps taking thus far.
This was, however, never ported to HeapLang. It was instead instantiated with the constant function
λ _, 0,
retaining the original functionality of the language.
This MR seeks to add this functionality by:
steps_lb 0 in the presence of any wp (via
steps_lb n to
steps_lb (S n) when taking a step (via
P guarded under a number of laters relative to an existing lower bound
steps_lb n (via
The following formal rules summarises the idea in Hoare Triple notation (OBS: lemma names differ): The usefulness of this functionality is illustrated here: actris!26 (merged)
In particular, we previously had to use a
skipN instruction within a lock to
strip an amount of laters relative to the physical state.
With this change we can instead track this amount in the logic, and strip all of the necessary laters.
The change seems entirely non-invasive, seeing that all user-level specifications remain intact.
EDIT: Thanks to @lgaeher for suggesting the more general theorem for total adequacy, which let me bump the total adequacy theorem of HeapLang