# Added capability for stripping multiple laters per step in HeapLang

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:

- Adding a monotonically increasing number to the state interpretation (and ghost functor) of HeapLang
- Adding non-invasive lemmas that lets the user interact with this number by
- Obtaining a new lower bound
`steps_lb 0`

in the presence of any wp (via`wp_lb_init`

) - Incrementing an existing lower bound
`steps_lb n`

to`steps_lb (S n)`

when taking a step (via`wp_lb_update`

) - Derive propositions
`P`

guarded under a number of laters relative to an existing lower bound`steps_lb n`

(via`wp_step_fupdN_lb`

).

- Obtaining a new lower bound

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