Proofs for Adaptive Linear-Space Renaming

The paper Adaptive Linear-Space Renaming by Delporte-Gallet, Fauconnier, Gafni, and Lamport appeared in Proceedings of the 27th International Symposium on Distributed Computing (DISC 2013).   Its algorithms were written in PlusCal and specified in PlusCal and TLA+.   Formal TLA+ proofs of their safety properties were written.   They were completely checked by TLAPS, the TLA+ Proof System. except that:

• TLAPS did not yet do temporal reason when the paper was written, so a couple of trivial temporal-logic deductions were not checked.
• Because there was not yet a TLAPS library of facts about finite sets and cardinality, nine such facts were assumed.   The facts are obviouly true, and their TLA+ statements were checked by the TLC model checker.

The proofs are best read hierarchically using the TLA Toolbox.

Stephan Merz aided in writing the TLAPS proofs.