Flexible number of logical steps per physical step

[Note about citing this MR]

This MR has been implemented for RustHornBelt, and is described in the related paper. Hence, the proper citation for this is the RustHornBelt paper:

Matsushita, Y., Denis, X., Jourdan, J. H., & Dreyer, D. (2022, June). RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 841-856).

[/Note about citing this MR]

This is the first part of the implementation of @shiatsumat idea for making it possible to consume an "unbounded" number of logical steps for each physical steps. The remaining of the implementation will be a use case : I plan to use this in the current version of lambdarust in order to remove the pattern of "delayed sharing" by consuming the necessary number of logical steps for a "skip" instruction associated with turning a mutable borrow into a shared borrow. This will be useful for the formalization of RustHorn in Iris, where we have laters which are nested arbitrarily deep which we need to eat.

The main ideas of this PR are:

1- decide in advance how many logical steps are going to be consumed for each of the physical step. The important point here is that this number can actually depends on the physical step. I.e., typically, at the beginning of the program, we consume few steps, and we consume more and more steps while the program executes. This makes it possible to eat more and more later in the proof's representation predicates as long as the data structures built by the program grow. This variable number of steps is represented in the formalization by the steps_per_step function of type nat -> nat (the nat parameter being the number of physical steps already executed by the program).

2- make the state interpretation aware of the number of steps already executed, so that the user of the logic knows the number of logical steps available for the current physical step. Typically, one would use Auth (MaxNat), so that owning ◯ n witnesses that we have executed at least n steps and that therefore some number of logical steps can be consumed for the current physical step.

This makes it possible to prove the following new property of WP:

Lemma wp_step_fupdN n s E1 E2 e P Φ :
  TCEq (to_val e) None → E2 ⊆ E1 →
  (∀ σ stepcnt κs n',
      state_interp σ stepcnt κs n' ={E1,∅}=∗ ⌜n ≤ S (steps_per_step stepcnt)⌝) -∗
  (|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗
  WP e @ s; E1 {{ Φ }}.

That is, we can run an update that takes n steps in parallel with WP as soon as the current state interpretation allows us to prove that the current physical step consumes at least n logical steps.

A few things that we may want to discuss:

• Even though developments depending of Iris can be rather easily adapted to this change, they will all need some adaptations, since it changes the irisG class, the type of state interpretation, the lifting lemmas and the adequacy theorems.

• I needed to strengthen the soundness lemma for fancy updates: in the previous lemma, we assumed that invariants were closed at every (logical) step, which is not necessarily true if we allow to consume several logical steps for each atomic physical step. The new lemma does not require to close any invariant at any time. I proved that it is actually stronger than the current one:

Lemma step_fupdN_strong_soundness `{!invPreG Σ} φ n :
  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
  φ.

Should we replace the old lemma by this one? Give a new name for this stronger version (this will be the 3rd version included in fancy_updates.v)?

• In order to keep nice lifting lemmas for pure steps (where the state interpretation does not appear), I needed to require state interpretation to be somehow monotonous wrt. the step counter:

  state_interp_stepcnt_mono σ stepcnt κs n:
    state_interp σ stepcnt κs n ={∅}=∗ state_interp σ (S stepcnt) κs n

I don't expect this statement to be difficult to prove in practice (especially in the backward compatible case where state_interp does not depend on stepcnt). However, this makes the irisG class to be a dependent type, which we may consider as unacceptable (especially since these proof terms appears in the statements of adequacy).

The alternative is to add this as a separate hypothesis for the pure lifting lemmas, but I wanted to keep these lemmas as simple as possible.

• The way masks are used in the wp_step_fupdN lemma is surprising, since it requires that the inner masks be empty. The reason is that I made the choice of letting the user open invariants for several logical steps, so that the masks used within WP are empty. I believe this is the most expressive way of stating the lemma, even though it may be a little bit unusual.

TODO

• Make lambdarust use this
• Changelog
• Update the doc

Cc @jung, @shiatsumat, @xldenis.

Another point to discuss: this PR makes use of the step_fupdN modality in a pervasive manner. Should we add support for it in the proofmode?

added 1 commit

• c19f892d - A version of wp_step_fupdN which lets use and keep a non-persistent resource...

Compare with previous version

added 1 commit

• 52d7636c - Minimal support for step_fupdN in the proofmode.

Compare with previous version

added 1 commit

• d11bb7e7 - 1- Prove step_fupdN_combine

Compare with previous version

added 1 commit

• e15ec18b - More powerful from_modal_step_fupdN instance.

Compare with previous version

changed the description

Without having read the details -- this is super cool!

That is, we can run an update that takes n steps in parallel with WP as soon as the current state interpretation allows us to prove that the current physical step consumes at least n logical steps.

The theorem actually says n ≤ S ...; why the extra S? Seems like you always actually take one more step than what the function says, to ensure at least one (logical) step is taken? That makes sense but should be called out explicitly in the docs for this function and the PR description.

I plan to use this in the current version of lambdarust in order to remove the pattern of "delayed sharing" by consuming the necessary number of logical steps for a "skip" instruction associated with turning a mutable borrow into a shared borrow.

So this will mean that we now need a Skip where none was needed before? I am not sure if I like this... the experiment is certainly worth doing though as preparation for RustHorn; we can discuss later if that is something we want to merge into master.

The way masks are used in the wp_step_fupdN lemma is surprising, since it requires that the inner masks be empty. The reason is that I made the choice of letting the user open invariants for several logical steps, so that the masks used within WP are empty. I believe this is the most expressive way of stating the lemma, even though it may be a little bit unusual.

I agree, empty mask here should imply any other mask.

The theorem actually says n ≤ S ...; why the extra S? Seems like you always actually take one more step than what the function says, to ensure at least one (logical) step is taken? That makes sense but should be called out explicitly in the docs for this function and the PR description.

Yes. This is mainly to make sure at least one step is taken, both for backward compatibility and to make sure the wp tactics that remove the laters keep working. We can write this explicitly in the docs, but note that consuming more steps usually costs nothing.

So this will mean that we now need a Skip where none was needed before? I am not sure if I like this... the experiment is certainly worth doing though as preparation for RustHorn; we can discuss later if that is something we want to merge into master.

Agreed. The model is going to be more complex anyway, so this is probably not a good idea to merge, but a good first step for RustHorn.

We can write this explicitly in the docs, but note that consuming more steps usually costs nothing.

Sure, it cost nothing, but it is confusing to document steps_per_step as "Number of additional logical steps per physical step" when actually there's one more step being taken. And it's confusing when the lemma statement you give in the MR description contains an S that the surrounding text just ignores.

That's why I used "additional": that's the number of steps which are added compared to the default, which is 1. But I agree that this is confusing, I will reword.

Btw, the MR title is really confusing (and that presentation is part of what threw me off initially): the step-indexing is not controlled by ghosts. It is controlled by this new function which can only depend on physical information, on things present in the trace. The ghost just reflects that information into the logic.

added 1 commit

• 94d26232 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

changed title from WIP: Step indexing controlled by the ghosts to WIP: Extended step indexing reflected by the ghosts

changed title from WIP: Extended step indexing reflected by the ghosts to WIP: Dynamic number of logical steps per physical step

changed title from WIP: Dynamic number of logical steps per physical step to WIP: Flexible number of logical steps per physical step

mentioned in issue #392

added 1 commit

• e1094286 - A version of wp_step_fupdN which lets use and keep a non-persistent resource...

Compare with previous version

added 1 commit

• 52d78ac7 - A version of wp_step_fupdN which lets use and keep a non-persistent resource...

Compare with previous version