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.