  Relational Hoare logics extend the applicability of modular, deductive
verification to encompass important 2-run properties including dependency
requirements such as confidentiality and program relations such as equivalence
or similarity between program versions. A considerable number of recent works
introduce different relational Hoare logics without yet converging on a core
set of proof rules. This paper looks backwards to little known early work. This
brings to light some principles that clarify and organize the rules as well as
suggesting a new rule and a new notion of completeness.
