Skip to content

New notion of local updates.

Robbert Krebbers requested to merge robbert/local_updates into master

This Merge Request proposes a new notion of local updates that is more usable for proving frame preserving updates of auth.

Definitions

The new notion of local updates is:

Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
  ✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
Infix "~l~>" := local_update (at level 70).

The corresponding frame preserving update for auth is:

Lemma auth_update a b a' b' :
  (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.

PS1: I am using tuples so that I can declare it as a PreOrder (i.e. reflexive and transitive relation).

PS2: One cannot define the local update in terms of ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b' because that requires a unit. My definition of local updates works for CMRAs without units, and that is important, since we often consider compound CMRAs build using auxiliary constructs that do not have units (like fractions, excl, dec_agree, and so on).

Motivation

The old frame preserving update for auth, namely:

Lemma auth_update a af b :
  a ~l~> b @ Some af → ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.

is very difficult to use. It requires the authoritative element to be of the shape ● (a ⋅ af), which is generally not the case when writing invariants like:

∃ x, own γ (● (f x)) ∧ P x

So, one needs to use validity of ● a ⋅ ◯ b first, so as to obtain b ≼ a. The new local updates are much more syntax directed.

In principle, the program_logic/auth construction took care of some of these issues, but in practice it is not so useful, because:

  • It can only be used for auth over discrete CMRAs.
  • It cannot be used when auth is used as part of another monoid, for example, a product.
  • One cannot include ownership of fragments in the auth invariant (see for example Zhen's ticket lock proof).

Also, when looking at heap, for example, use was required to define a function from ghost heaps to physical states and visa versa. This is quite cumbersome, in the new version, only a function from physical states to heaps is needed, and the amount of boilerplate is reduced drastically.

Credits

Thanks to @amintimany for discussions that lead to this definition.

Todo

Local updates for lists.

Merge request reports