New notion of local updates.
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.