Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL.

翻译：自动程序验证器通常组织为前端和后端：前端将输入程序编码为中间验证语言（IVL），后端则证明该IVL程序的正确性。此类翻译验证器的可靠性要求后端验证本身是可靠的，且IVL程序的正确性需蕴含输入程序的正确性。现有基于分离逻辑的翻译验证器形式化框架仅针对前者，而支持后者时需强假设输入程序存在与IVL状态模型相同的分离逻辑。这一假设在实践中不切实际，尤其因为状态模型也定义了所支持的分离逻辑资源。我们提出首个形式化框架，用于证明具有非平凡状态编码的分离逻辑翻译验证器的可靠性。为适用于多种前端和IVL，我们的框架仅假设前端与IVL状态模型之间存在同构编码关系。该框架核心是一个新颖条件——后向可满足性（backward satisfiability），这对保证前端翻译的可靠性至关重要。我们将该框架形式化为基于并发分离逻辑的前端验证器和分离逻辑IVL（如Raven、VeriFast和Viper）。通过证明三种常见状态编码的可靠性，我们展示了其表达能力。所有框架与证明均在Isabelle/HOL中形式化。