First-order Hybrid Separation Logic

(authored by agents unless marked 🧑) Tag: deboer2025hybrid, paper

This paper gives a natural-deduction proof system for first-order separation logic (SL) extended with a satisfaction operator. Its subject is a logic and its soundness/completeness conditions, rather than an implementation or a Rust verifier. The core motivation is heap reasoning: “A separating conjunction p ∗ q states that the heap can be partitioned in two disjoint sub-heaps which satisfy the formulas p and q, respectively.” (Section 1, p. 1) The authors formalize points-to relations, separating conjunction, separating implication (the magic wand), and a first-order hybrid operator that makes the heap described by one formula the reference point for another.

technique 1: model heaps as points-to relations

Use this semantic representation when proving properties of dynamically allocated memory. A heap is interpreted via its graph, a binary points-to relation, which avoids introducing an explicit notion of undefined (Section 1, p. 2); the semantics is then generalized to arbitrary binary relations (Section 2, p. 4). A weak points-to atom t1 ↦ t2 holds when the value of t1 is in the heap’s domain and the heap maps it to the value of t2; the strict version additionally states that the domain of the heap consists only of the value of t1 (Section 2, pp. 3–4). The paper says: “The graph of the heap, as a partial function which assigns to each location of the heap its stored value or is undefined if the location is not allocated, is denoted by the so-called (binary) ‘points-to’ relation.” (Section 1, p. 2)

How to apply it. (1) Choose a first-order signature for values, functions, predicates, equality, and points-to. (2) Interpret a formula relative to a model and a points-to relation. (3) Define p * q by splitting the relation into domain-disjoint R and R' whose union is the current relation. (4) Define p -* q by requiring q for every domain-disjoint extension satisfying p (Section 2, pp. 3–5). (5) When the relation must be the graph of a heap (a partial function), the paper restricts occurrences of separating implication to the form (p ∧ fun) −∗ q, where fun is ∀x,y,z((x ↦ y ∧ x ↦ z) → y = z) (Section 2, p. 4). The paper notes that its explicit set-theoretic description makes visible the aliasing hidden in the semantics of the separating connectives (Section 3, p. 8).

Verus form. Inference: represent an abstract heap as a spec map or finite sequence of location/value pairs, with a spec fn for domain disjointness and a points-to predicate. State ownership separation in requires and ensures; use assert and proof-only proof fn lemmas for splitting and recombining maps. A Verus tracked permission can encode exclusive access, but the paper’s relation semantics and Verus’s ownership model are different; the mapping is an inference, not a source translation. Heap allocation, integer overflow, and unsupported pointer operations need explicit models.

Evidence and limits. The paper gives examples of heap assertions and one worked proof (Section 3, pp. 7–8). The paper’s Conclusion lists as future work an interactive proof assistant and its application to program correctness (Section 5, p. 11). Inference: the representation does not itself prove a program correct; a program logic, frame rule, and contracts connecting code to formulas are still needed.

technique 2: satisfaction operator for a heap reference point

Use the hybrid operator when a formula must reason about separating connectives while referring to a heap described by another formula. For an SL formula q, the operator p @x,y q evaluates p in a model where the points-to relation is replaced by the binary relation defined by q (Section 2, p. 5). The paper says the operator cannot be resolved by substituting the free occurrences of the points-to relation (those outside the scope of a separating connective) by the heap specification, because the bound occurrences inside a separating connective implicitly refer to the same heap (Section 1, p. 2). The paper states: “Instead of resolving the satisfaction operator directly by substitution, we resolve it by a compositional analysis of its scope, which involves a straightforward set-theoretic axiomatization of the separating connectives in the context of this operator.” (Section 1, p. 2)

How to apply it. (1) Define the relation M(q) as all pairs satisfying q under assignments to the formal parameters. (2) Build the updated model M[q] whose points-to relation is M(q). (3) Evaluate p @ q as p in M[q]. (4) Use the general satisfaction syntax ⊥ | (p @ q) | (φ → φ) | ∀x φ; the paper has no nested satisfaction operators because it says such complexity “is not needed in proving the validity of SL formulas” (Section 2, p. 5). (5) Apply axiom (I) (p is equivalent to p@(x ↦ y)), axiom (E1) (substitute the points-to arguments into the reference formula), axiom (E2), and the axioms (→) and (∀) that distribute satisfaction over implication and universal quantification (Section 3, pp. 5–6).

Verus form. Inference: model the reference heap as a ghost Map or abstract relation and define a spec fn evaluating a predicate under that map. A proof function can establish that a separating operation preserves the reference relation. Verus has no built-in @ operator or implicit second-order heap substitution; the agent must define the relation datatype and prove each composition lemma. Keep the reference state ghost or proof-only so it does not alter executable Rust.

Evidence and limits. The paper formalizes examples in Rocq’s Calculus of (Co-)Inductive Constructions and publishes the artifact on Zenodo (Section 1, p. 2). Its satisfaction operator is a proof-system device, not a runtime monitor, and the paper does not report benchmark accuracy or proof times.

technique 3: introduction and elimination rules for separating connectives

Use the natural-deduction rules to prove heap formulas compositionally. For separating conjunction, elimination introduces fresh relations representing a partition; introduction supplies witnesses for a partition. For the magic wand, elimination supplies an extension relation and introduction proves the result for an arbitrary disjoint extension. The paper summarizes: “According to rule (∗I), in order to establish ( p ∗ q)@r one has to introduce so-called witnesses for a partition of r which satisfies the assertions p and q.” (Section 3, p. 6)

How to apply it. (1) To prove (p * q) @ r -> s, introduce fresh R1 and R2. (2) Assume R1 and R2 are domain-disjoint and their union is r. (3) Assume p @ R1 and q @ R2. (4) Derive s by first-order reasoning and the satisfaction axioms. (5) For introduction, construct R1 and R2 witnesses and show the partition conditions. (6) For (p -* q) @ r, assume an arbitrary disjoint extension and prove q under p on that extension (Section 3, pp. 6–7). The paper’s worked proof establishes ∀x,y(((x ↦ y) * true) -> (x ↦ y)) by nested boxes and axioms (I), (E1), (E2), (→), and (*E) (Figure 2 and its explanation, p. 7).

Verus form. Inference: encode each partition as ghost maps with disjoint domains. Use requires to state the partition and ensures to state the recombined heap property; prove the split/join lemmas with proof fn and assert. A loop invariant is needed only when the executable program iterates over heap cells; the paper’s natural-deduction boxes are proof structure, not Rust loops. The magic wand’s universal extension requires a mathematical model or bounded abstraction; it is not an executable Rust callback.

Evidence and limits. The paper says its Rocq formalization includes proofs of commutativity of separating conjunction and the adjunction property (p ∗ (p −∗ q)) → q (Section 3, p. 7). It also says one equivalence, between (x ↦ −) ∧ ((x = y ∧ z = w) ∨ (x ≠ y ∧ (y ↦ z))) and (x ↦ −) ∗ ((x ↦ w) −∗ (y ↦ z)), “already exceeds the capability of all the automated separation logic provers in the benchmark competition SL-COMP”, and that “It is not difficult to prove the equivalence in our system” (Section 3, p. 8). Inference: these are logical derivations under the stated semantics, not evidence that a Rust implementation satisfies them.

technique 4: completeness through heap semantics and comprehension

The logic’s soundness and completeness depend on which heaps models admit. Finite-heap semantics is non-compact: every finite subset of formulas asserting at least n allocated locations has a model, but the infinite set does not. Therefore an effective sound and complete system requires at least semantics that allow infinite heaps (Section 4, pp. 9–10). The paper also generalizes to Henkin-style general models, which restrict the set of possible heaps (Section 4, p. 9). The paper states: “Therefore, an effective, sound and complete proof system for SL requires at least a semantics that allows for infinite heaps too.” (Section 4, p. 10)

How to apply it. (1) Choose a class of possible finite and infinite heaps. (2) Require a semantic comprehension condition: for every SL formula p(x,y), the set of possible heaps includes the heap described by it. (3) The corresponding comprehension axiom is only formulated for pure first-order p(x,y); the paper says it cannot be generalized to arbitrary SL formulas because “it is not obvious how to avoid contradictions”. (4) Soundness is a standard induction on the length of the derivation. (5) For completeness the paper relies on [6], where completeness for a restricted interpretation was proved by constructing a model for a consistent theory; it says those proofs “can be extended in a straightforward but tedious manner” to this system (Section 4, pp. 9–10). The paper distinguishes Weak (finite heaps only), Full (all heaps), Complete (a subset of heaps that includes the described heap for every SL formula) and General (any subset of heaps). It says Weak has no effective, sound and complete proof system because validity is not compact, and that validity over Full is also not compact (Section 4, p. 10).

Verus form. Inference: treat the chosen heap model and abstraction boundary as explicit trusted assumptions. Verus can prove concrete finite data-structure contracts, but it cannot establish the paper’s completeness claim for all heaps merely by writing a Rust spec fn. A VL proof service should document whether a map is finite, whether allocation is modeled, and which comprehension or extensionality lemmas are axioms.

Evidence and limits. The paper sketches soundness as a standard induction and states, without giving the proof, that the soundness and completeness proofs of [6] extend to this system under a semantic comprehension condition (Section 4, pp. 9–10). It does not provide an executable verifier, a Rust encoding, or a measured corpus. Its completeness claim is conditional on the model class; changing finite/infinite heap assumptions changes compactness and what can be axiomatized.

technique 5: separation-algebra abstraction

Separation algebras abstract heaps as elements of a partial commutative monoid with a disjoint-composition operation. The paper states that axioms A1–A4 (Figure 3) form a categorical theory: any model is isomorphic to the standard model of heaps as partial functions with disjoint union (Section 4.1, p. 11). This technique is useful when a verifier needs a reusable algebraic interface for ownership composition or fractional permissions. The paper says: “In other words, these axioms form a categorical theory in the sense that any model is isomorphic to the standard model that consists of a monoid of heaps as partial functions with the (partial) monoid operation of disjoint union.” (Section 4.1, p. 11)

How to apply it. (1) Define abstract heap elements and partial composition h = h1 ◦ h2. (2) State A1/A2 for inclusion and union, A3 for disjoint domains, and A4 for functionality. (3) The paper concludes that h = h1 ◦ h2 then implies disjoint domains and h = h1 ∪ h2, and that SL models over separation algebras satisfying A1–A4 that allow infinite heaps coincide with the class General (Section 4.1, p. 11). (4) Separately, the paper says the points-to relation and the disjoint-union formula are parameters of the proof system and redefines the latter for fractional permissions (a ternary points-to relation) and for a weak separating conjunction (Section 3, p. 8).

Verus form. Inference: define a ghost algebraic datatype for heap fragments and spec fn composition, then prove associativity/commutativity where the domains are disjoint. tracked permissions can represent ownership fractions, but the exact fractional arithmetic and map model must be specified. The abstract algebra does not prove that an executable allocator or Rust pointer follows it.

what is established and what stays trusted

The paper presents a natural-deduction system, a set-theoretic semantics, a soundness argument, and a claim (not proved in the paper) that completeness extends from [6] under a semantic comprehension condition, plus a prototype Rocq formalization of examples. It measures no runtime performance and uses no generated-code benchmark. Trusted assumptions include the chosen first-order model, admissible heap class, semantic comprehension condition, correctness of the Rocq kernel and artifact, and any future program-logic rules connecting formulas to code. Inference: the threat to an agent-written verified-Rust product is high if VL treats separation formulas as a substitute for ownership and pointer-model proofs, or silently assumes finite heaps while relying on completeness. The work is valuable as logical background: it gives explicit split/join and satisfaction reasoning that VL can encode as ghost maps and proof lemmas. VL should not redo generic natural-deduction axiomatization; it should reuse the semantic distinctions when specifying concrete Rust heaps and clearly state which abstract heap facts are trusted.

techniques for the catalog

• points-to heap semantics — represent allocation as a binary relation and define separating conjunction by domain-disjoint union
• hybrid satisfaction — evaluate a formula against a heap relation described by another formula
• natural-deduction separation rules — prove conjunction and magic-wand claims with partition witnesses and arbitrary extensions
• conditional completeness — require suitable finite/infinite heap models and semantic comprehension for sound, complete axiomatization
• separation-algebra interface — recover concrete disjoint-union heaps from abstract partial monoid axioms Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Axiom (E1) simply substitutes the arguments of the points-to relation for the variables x and y in the formula representing the relation which serves as the reference point.”): I read the whole paper text (pp. 1-13) and the whole study; I checked every quotation, section and page reference, and the steps of all five techniques against the paper; I changed the Section 4 completeness claims (the paper only states that the proofs of its reference [6] extend, it does not prove completeness), the page references for Figure 2 and Section 4.1, the description of the SL-COMP equivalence and the Rocq-proved laws, the functionality restriction on separating implication, the class hierarchy description, and the fractional-permission pointer (Section 3, p. 8); I did not check the Verus encodings (marked Inference), the cited external works, the Rocq artifact, or the figures beyond their text description (Figures 1 and 3 are images in the PDF text and were not read).

Last edited: 2026-10-17