Two for the Price of One: Lifting Separation Logic Assertions

Recently, data abstraction has been studied in the context of separationlogic, with noticeable practical successes: the developed logics have enabledclean proofs of tricky challenging programs, such as subject-observer patterns,and they have become the basis of efficient verification tools for Java(jStar), C (VeriFast) and Hoare Type Theory (Ynot). In this paper, we give anew semantic analysis of such logic-based approaches using Reynolds'srelational parametricity. The core of the analysis is our lifting theorems,which give a sound and complete condition for when a true implication betweenassertions in the standard interpretation entails that the same implicationholds in a relational interpretation. Using these theorems, we provide analgorithm for identifying abstraction-respecting client-side proofs; the proofsensure that clients cannot distinguish two appropriately-related moduleimplementations