Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Completeness for a First-order Abstract Separation Logic

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

Page numbers below are PDF page numbers of the arXiv v1 file (28 pages; main text pp. 1-17, appendices pp. 20-27).

result

Hou and Tiu define first-order abstract separation logic (FOASL), a labelled sequent calculus LSFOASL, and a theorem prover. FOASL weakens concrete points-to: an abstract points-to term denotes the heap returned by a total function and need not be a singleton heap. The paper’s reason for the weakening is the incompleteness result of Calcagno et al. [10] for concrete SL, which it says would recur if the interpretation were restricted to singleton heaps by a finite theory. Theories added as assumptions then approximate concrete models. The abstract states: “We prove that FOASL is sound and complete with respect to an abstract semantics, of which the standard SL semantics is an instance.”

technique 1: abstract the heap, retain separation structure

Use a separation algebra (H, ◦, ϵ), with ◦ a partial function, satisfying identity, commutativity, associativity, cancellativity, indivisible unit, disjointness, and cross-split (Section 2, p. 5). Interpret an n-ary abstract points-to predicate with a total function f_n : D^n → H; the formula t1 ↦ t2, …, tk is true at world h exactly when f_k(t1, …, tk) = h (Table 1, p. 5). Keep separation conjunction *, magic wand −*, the multiplicative unit ⊤* (true iff h = ϵ), first-order quantification, and the modality ♦ (true at h iff the body is true at some world). A * B splits the current world into h1 ◦ h2 = h; A −* B quantifies over all h1, h2 with h ◦ h1 = h2 (Table 1, p. 5). The paper lists two consequences of the interpretation: injectivity (the same term tuple holds in at most one heap) and totality (some heap exists for every tuple) (p. 6).

To apply it, choose a model, define f_n, then reason with labelled worlds. Reynolds heaps are an instance when D is the integers, H is finite partial maps from integers to integers, and f2(a,b) is the singleton heap [a ↦ b] (Example 1, Section 2, p. 7). The paper adds that allowing infinite heaps still gives a separation algebra, so non-standard interpretations are admitted (p. 7). The abstraction is deliberate: “we do not assume that the constructed heap from a tuple is a singleton heap” (Section 1, p. 3). The paper also does not assume an invalid address nil; nil ↦ t is satisfiable, not valid, and can be made unsatisfiable by adding a theory (p. 6).

Verus form (Inference): Verus’s ownership and Map/sequence specifications can model a heap fragment and separating resources as ghost predicates, but Verus does not provide FOASL’s * or magic wand (I did not check this against Verus documentation). One would encode disjointness and frame facts as spec fn predicates and prove split/merge lemmas with requires and ensures; this is an encoding, not a native logic translation.

Represent a sequent as G; Γ ⊢ Δ, where G is a set of relational atoms (h1,h2 ⊲ h3) meaning h1 ◦ h2 = h3, and Γ/Δ are sets of labelled formulas h : A (Section 3, p. 7). To prove F, start from ⊢ h : F with an arbitrary label h ≠ ϵ and apply rules backwards; a derivation is closed when every branch ends in a rule with no premises (p. 8). Logical rules (Figure 1, p. 8) split *, introduce −*, instantiate ∃, and move between worlds for ♦; equality rules for terms (=1, =2) and labels (∼1, ∼2) replace equal terms or labels. Two points-to rules, ↦1 and ↦2, capture totality and injectivity respectively. The paper states: “These rules allow one to replace a term (label) with its equal anywhere in the sequent.” (Section 3, p. 7).

Structural rules (Figure 2, p. 9) are E (commutativity), D (disjointness: (h1,h1 ⊲ h2) gives h1 ∼ ϵ), A (associativity), P (partial determinism), C (cancellativity), and CS (cross-split). Soundness: if ⊢ h : F is derivable for any label h, then F is valid (Theorem 1, Section 3, p. 8). The proof is in Appendix A (p. 20): it shows only the rules ∃L, ∃R, ♦L, ♦R, ↦1, ↦2 and says the other rules are analogous to LSPASL [16]. For the implementation, Section 6 replaces =2 and ∼2 with substitution-oriented =′2 and ∼′2. The paper says deriving =′2, ∼′2 is straightforward; the converse needs closure of the primed system under term and label substitutions (Lemmas 6–7, Section 6, p. 15), which it says (p. 16) “require induction on the height of derivations, and routine checks confirm that they both hold” (no proof is given).

Verus form (Inference): each labelled formula can be a ghost proposition over a resource state; relational atoms become lemmas describing map disjoint-union. Backward proof search itself is an external tactic or generated Rust proof, while individual rule soundness can be encoded as Verus proof fn lemmas with requires/ensures. Do not write proof fn calls into executable code.

technique 3: completeness by Hintikka saturation and countermodel

For an unprovable formula, fix a fair schedule (every rule instance occurs infinitely often, Definition 2, p. 11) and construct a series of finite sequents starting from G1 = Γ1 = ∅, Δ1 = a1 : F (Definition 3, p. 11). At step i, the scheduled rule instance is applied: for example ∗L adds a relational atom and two labelled formulas with fresh labels, ∃ on the left adds an instance with a fresh term, and for → or −* the construction picks the side that is not derivable. The limit sequent is the union of all of them (Definition 4, p. 12). Lemma 2 (p. 12) states that every sequent in the series has no derivation. Lemma 3 (p. 12) says the limit sequent is a Hintikka sequent; its proof in Appendix B shows only a few conditions (∗R, 11, 12) and says “The other conditions can be shown similarly.” (p. 26). A Hintikka sequent must satisfy 26 conditions (Definition 1, pp. 9–10), covering connective decomposition, quantifier witnesses, modality worlds, equality substitution, ∼ as an equivalence and congruence, and separation-algebra closure.

Construct a countermodel from a Hintikka sequent (Lemma 1, p. 10; proof in Appendix B, pp. 21–23):

  1. take the closed terms as the Herbrand domain D, with c^I = c; t1 = t2 is true iff h : t1 = t2 ∈ Γ for some h
  2. partition labels into equivalence classes [h]_G under ∼ in G
  3. H is the set of classes; [h1] ◦ [h2] = [h0] iff matching relational atoms and ∼ facts are in G; ϵ = [ϵ]; ρ(h) = [h]
  4. define each abstract points-to function by f_n(t1,…,tn) = [h] iff h' : t1 ↦ t2,…,tn ∈ Γ and h ∼ h' ∈ G; Conditions 22 and 23 make it total
  5. interpret each ordinary relation R at [h] iff h' : R(…) ∈ Γ with h ∼ h'
  6. check the separation-algebra laws against Conditions 17, 19, 20, 21, 24, 25, 26, then prove by induction on the size of the sentence that Γ is true and Δ false (the appendix shows the ∃ and ♦ cases and refers to [16] for the propositional connectives)

The paper’s key statement is: “The completeness proof is done via a counter-model construction similar to that in [20,16] for the propositional case, but our proof is significantly more complicated”, because of the first-order language and the model of the points-to predicate, which “requires a novel proof technique” (Section 1, pp. 3–4). Theorem 2 concludes that every FOASL-valid formula is derivable (Section 4, p. 12; proof in Appendix B, p. 26). The counter-model may be infinite (Section 4, p. 12). The Conclusion states: “The completeness of the finite calculus implies that our logic is recursively enumerable.” (Section 7, p. 17). Inference: this is a meta-theoretic completeness result, not a claim that proof search terminates on every input.

Verus form (Inference): a finite instance can be represented with ghost sets of labels and an explicit equivalence relation, then proved closed under each rule. The infinite fair schedule and quotient model are outside ordinary executable Rust; use them as a specification-level argument or a separate trusted meta-theory.

technique 4: theories approximate concrete separation logics

Instead of adding a new inference rule for each concrete points-to property, add formulas as assumptions. For Reynolds’s semantics the paper gives six formulas (Section 5.1, p. 13), written here with ↦ for the paper’s concrete points-to and ⇢ for the abstract one:

  1. ∀e1,e2. (e1 ↦ e2) ∧ ⊤* → ⊥ (a points-to heap is not empty)
  2. ∀e1,e2. (e1 ↦ e2) → ¬(¬⊤* * ¬⊤*) (it is not a composition of two nonempty heaps)
  3. (e1 ↦ e2) * (e3 ↦ e4) → ¬(e1 = e3) (separated cells have distinct addresses)
  4. (e1 ↦ e2) ∧ (e3 ↦ e4) → (e1 = e3) ∧ (e2 = e4) (injectivity)
  5. ∃e1 ∀e2. ¬((e1 ↦ e2) −* ⊥) (a fresh-address property; it simulates the rule HE)
  6. (e1 ↦ e2) → (e1 ⇢ e2) (concrete points-to implies abstract; the converse does not hold, since ⇢ is weaker)

Formulas 1–5 simulate the LSSL rules ↦L1, ↦L2, ↦L3, ↦L4, and HE; ↦L5 is derived using Formula 6 and an abstract points-to rule. Lemma 4 states the Figure 3 rules are admissible in LSFOASL when Formulas 1–6 are assumed true; Lemma 5 states the formulas are valid in Reynolds’s semantics (p. 13). The paper says validity is “easy to check” and gives no proof. The two-premise rule HC is not handled; the paper says it “seems to require more expressiveness than our logic” (p. 14).

Theory 7, ∀e1,e2. ♦(e1 ↦ e2), is for Vafeiadis–Parkinson’s “total addressability”; Formulas 1–6 are also valid there (Section 5.2, p. 14). Theory 8, ∀e1,e2. ♦(e1 ↦ e2) → ¬(∃e3. ¬(e2 = e3) ∧ ♦(e1 ↦ e3)), captures the compatibility behavior suggested by the −*Disj rule of Lee et al.; the paper notes that there is no formal definition of their non-standard semantics (Section 5.3, p. 14). For Thakur et al.’s acyclic-list semantics, define path(e1,e2) ≡ e1 ↦ e2 ∨ ∃e3.(e1 ↦ e3) * path(e3,e2) and add Theory 9, path(e1,e2) → e1 ≠ e2. The paper states: “Note that since our proof system does not support inductive definitions, we cannot force the interpretation of path to be the least fixed point of its definition.” (Section 5.4, p. 15). Section 6 adds Theory 10, ∀~e. (nil ↦ ~e) → ⊥ (p. 16).

Verus form (Inference): encode each chosen theory as a spec fn or axiom-like trusted interface only when its model has been separately justified; prove concrete map properties as lemmas. A theory assumption is trusted specification input, not evidence that arbitrary Rust heaps satisfy it.

implementation evidence and limits

The prover extends the authors’ earlier Reynolds-SL prover [17] with (non-inductive) predicates and modalities, and builds in linked-list and binary-tree rules inherited from it (Section 6, pp. 15–16). It leaves the HC rule out of proof search. Table 2 (p. 16) lists 12 formulae with times: formulas 1–4 <0.001s, formula 5 0.9s, formula 6 <0.001s, formula 7 0.0015s, formulas 8–10 <0.001s, formula 11 <0.001s, formula 12 0.0025s. The table is titled “Experiment on selected formulae”; the paper gives no hardware, no repeated-run method, and no comparison timings. Formulas 1–4 come from Galmiche and Méry’s work, 5–7 are overlaid-structure and composite-heap properties, 8–10 are septraction properties, and 11–12 use Theories 7 and 8 added as assumptions. The authors claim: “To our knowledge most existing provers for SL cannot prove the formulae in Table 2.” This is an unmeasured claim by the authors; the paper reports no comparison runs.

What the paper proves: soundness (Appendix A, with only six rule cases shown) and completeness (Appendix B, with only some Hintikka conditions shown) for FOASL semantics. It states admissibility of the Figure 3 rules (Lemma 4) and validity of Formulas 1–6 in Reynolds’s model (Lemma 5), and gives selected automated derivations. Inference: what stays trusted by anyone using it is the model choice, the added theories, the prover implementation, and any translation from Rust ownership to separation algebra.

techniques for the catalog

  • abstract points-to semantics — replace singleton heaps with total heap-valued functions to regain completeness
  • labelled separation calculus — reason about worlds, splits, magic wand, quantifiers, and modalities with sequents
  • Hintikka countermodel construction — fairly saturate unprovable sequents and build a falsifying quotient model
  • model theories as assumptions — approximate concrete points-to behavior by formulas instead of new proof rules

Last edited: