Skip to content

Make auth_update_core_id work with fractional authority

Simon Friis Vindum requested to merge simonfv/iris:core-id-local-update into master

This MR does the following:

  • Adds a new lemma to_agree_includedN
  • Generalizes auth_update_core_id to only require a fractional authority.

A few remarks/potential points of discussion:

  • I've removed the lemma core_id_local_update. It can't be used to prove the generalized auth_update_core_id and it doesn't seem useful for anything else.
  • Instead of changing auth_update_core_id one could instead have added a new lemma. That would be consistent with auth_both_op and auth_both_frac_op. But, to me it seems like such a simple generalization/specialization is not worth two lemmas.
  • The proof of auth_update_core_id contains a bit of duplication in the two branches. I was not able to cut down on it (my attempts only resulted in larger proofs), but maybe someone else can 😄
Edited by Ralf Jung

Merge request reports