the previous assertion trivially holds in the case where $k$ does not exist by letting $\phi_1 = \text{emp}$. Thus Condition 6 holds.

*   **Spatial Formula.** We now prove that the spatial formula $\phi_1'$ is of the required form and fulfills Condition 7. The formula $\phi_1'$ may be written as $\phi_2 * \phi_3 * \phi_4$, where:

- $\text{alloc}(\phi_2) \subseteq (V^* \cup \text{alloc}(\psi'))$,

- $\text{alloc}(\phi_3) \subseteq \mathcal{V}(\phi) \setminus (V^* \cup \text{alloc}(\psi'))$,

- $\text{alloc}(\phi_4) \cap (\mathcal{V}(\phi) \cup V^* \cup \text{alloc}(\psi')) = \emptyset$.

If $\phi_2$ contains two atoms with the same root then $\phi'$ is heap-unsatisfiable and $S'$ is an axiom. Thus $\text{len}(\phi_2) \le \text{card}(V^*) + 1 \le \kappa + 1$ and Condition 7 holds.

The only rule that can add new predicate symbols to a premise is U, replacing an atom $\alpha'$ by a formula $\lambda$ such that $\alpha' \Leftarrow \mathfrak{R} \ \lambda$. Since the rules in $\mathfrak{R}$ are P-rules, the root of every predicate atom in $\lambda$ must be a fresh variable $y$, not occurring in $\mathcal{V}(\phi)$. If $y \in \text{dom}(\sigma)$ then $y$ is eventually replaced by some variable in $V^*$, hence the corresponding predicate atom from $\phi_1'$ is in $\phi_2$. If $y \notin \text{dom}(\sigma)$, then since this variable is never replaced, the corresponding atom must occur in $\phi_4$ by construction. This entails that all the atoms in $\phi_3$ must be obtained from atoms in $\phi$ after application of the substitution $\sigma$, i.e., that $\phi\sigma = \phi_3 * \eta$ for some formula $\eta$, up to AC. The formula $\eta$ can be written as $\eta_1 * \eta_2$ where $\text{alloc}(\eta_1) \subseteq \mathcal{V}(\psi') \cup V^*$ and $\text{alloc}(\eta_2) \cap (\mathcal{V}(\psi') \cup V^*) = \emptyset$. This entails that $\text{len}(\eta_1) \le 2 \cdot \kappa$, since $\text{card}(\mathcal{V}(\psi')) \le \kappa$ and $\text{card}(V^*) \le \kappa$.

We prove that necessarily $\phi_4 = \text{emp}$. Assume for the sake of contradiction that $\phi_4$ contains an atom $\alpha'$, and let $u = \text{root}(\alpha')$. By definition of $\phi_4$, $u \notin \mathcal{V}(\phi) \cup V^* \cup \text{alloc}(\psi')$. The variable $u$ must have been introduced by an application of rule U on some sequent $S_m$, as U is the only rule that can introduce new variables to the left-hand side of a sequent. By Proposition 5.7, $S_{m+1}$ is quasi-I-reducible, and we must have $m \ne k$ (if $k$ exists), since otherwise $\alpha'$ would occur in $\phi_1\sigma$. Since the rules in $\mathfrak{R}$ are P-rules, we have $u \in \mathcal{V} \mapsto (S_{m+1})$. Since $m \ne k$, by Corollary 5.8, there exists $m'$ such that $m < m'$ and $S_{m'}$ is I-reducible, i.e., rule I is applied on $S_{m'}$. Let $m'$ be the minimal number satisfying this property. The path $S_{m+1}, \dots, S_{m'}$ only contains applications of W, V and C, and $u \in \mathcal{V} \mapsto (S_{m'})$ by Proposition 5.6. Note that if $k$ exists then necessarily $m' < k$, moreover, none of these rules can introduce new variables to the right-hand side of a sequent. In particular, variable $u$, which is a fresh variable that does not occur in $\gamma_m$, cannot occur on the right-hand side $\gamma_{m'}$ of $S_{m'}$. Let $\theta$ denote the substitution used in the application of I on $S_{m'}$. As $u \in \mathcal{V} \mapsto (S_{m'})$, there exists a variable $z \in \text{dom}(\theta)$ such that $z\theta = u$. Since the rules in $\mathfrak{R}$ are P-rules, this entails that $u \in \text{alloc}(\gamma_{m'+1})$. Consequently, $u \in \text{alloc}(\lambda_{m'+1}) \cap \text{alloc}(\gamma_{m'+1})$ and by (repeatedly) applying Proposition 5.25, we deduce that $u \in \text{alloc}(\psi')$ (since by hypothesis $u \in \text{alloc}(\phi_4) \subseteq \text{alloc}(\phi')$), which contradicts the definition of $\phi_4$.

*   **Reachability Conditions.** Finally, we show that Condition 9 holds, i.e., that $\eta_2$ contains exactly the atoms $\beta$ in $\phi_3 * \eta_2$ such that $\text{root}(\psi') \nrightarrow_{\phi_1\sigma * \phi_2 * \phi_3 * \eta_2} \text{root}(\beta)$. Assume that $\phi_3$ contains an atom $\beta$ such that $\text{root}(\psi') \nrightarrow_{\phi_1\sigma * \phi_2 * \phi_3 * \eta_2} \text{root}(\beta)$. Since $\phi' = \phi_1\sigma * \phi_2 * \phi_3$, we get $\text{root}(\psi') \nrightarrow_{\phi'} \text{root}(\beta)$, $\text{root}(\beta) \in \text{alloc}(\phi')$ and $\text{root}(\beta) \notin \text{alloc}(\psi')$ (because $\text{root}(\beta) \ne \text{root}(\psi')$ and $\text{alloc}(\psi') = \{\text{root}(\psi')\}$), thus $S'$ is an anti-axiom. Conversely, assume that $\eta_2$
contains an atom $\beta$ such that $\mathrm{root}(\psi') \to_{\phi_1\sigma*\phi_2*\phi_3*\eta_2} \mathrm{root}(\beta)$. Note that $\mathrm{root}(\beta) \notin \mathcal{V}(\psi') \cup V^*$, by definition of $\eta_2$, which entails that $\mathrm{root}(\beta) \notin \mathrm{codom}(\sigma)$. If $\mathrm{root}(\beta) \notin \mathrm{alloc}(\phi')$, then by considering the first variable $y \notin \mathrm{alloc}(\phi') = \mathrm{alloc}(\phi_1\sigma * \phi_2 * \phi_3)$ along the path from $\mathrm{root}(\psi')$ to $\mathrm{root}(\beta)$, we have $y \in \mathcal{V}(\phi')$, $y \notin \mathrm{alloc}(\phi')$ and $y \in \mathrm{alloc}(\eta_2)$, hence $y \notin \mathcal{V}(\psi')$. Thus $S'$ is an anti-axiom, contradicting our hypothesis. Therefore, $\mathrm{root}(\beta) \in \mathrm{alloc}(\phi') = \mathrm{alloc}(\phi_1\sigma) \cup \mathrm{alloc}(\phi_2) \cup \mathrm{alloc}(\phi_3)$. We distinguish the three cases:

- Assume that $\mathrm{root}(\beta) \in \mathrm{alloc}(\phi_1\sigma)$ i.e., that $k$ exists, $\phi_1 \neq \mathrm{emp}$ and $\alpha \Leftarrow \mathfrak{R} \ \phi_1 \wedge \chi$. Since $\mathrm{root}(\beta) \notin \mathrm{codom}(\sigma)$, we also have $\mathrm{root}(\beta) \in \mathrm{alloc}(\phi_1)$. Since the rules in $\mathfrak{R}$ are P-rules, the variables in $\mathrm{alloc}(\phi_1)$ are either the root of $\alpha$ or fresh variables. Now $\mathrm{root}(\alpha)\sigma$ must be distinct from $\mathrm{root}(\beta)$, since $\mathrm{root}(\beta) \notin \mathcal{V}(\psi')$ and $\mathrm{root}(\alpha)\sigma = \mathrm{root}(\psi')$. Furthermore, all fresh variables are necessarily distinct from $\mathrm{root}(\beta)$. Indeed, they cannot occur in $\phi$, by definition, and $\mathrm{root}(\beta) \subseteq \mathrm{alloc}(\phi)$, as $\mathrm{root}(\beta) \subseteq \mathrm{alloc}(\eta_2) \subseteq \mathrm{alloc}(\eta) \subseteq \mathrm{alloc}(\phi\sigma)$ and $\mathrm{root}(\beta) \notin \mathrm{codom}(\sigma)$. Thus this case cannot occur.

- If $\mathrm{root}(\beta) \in \mathrm{alloc}(\phi_2)$, then $\mathrm{root}(\beta) \in V^* \cup \mathrm{alloc}(\psi')$ (by definition of $\phi_2$), which contradicts the fact that $\mathrm{root}(\beta) \notin \mathcal{V}(\psi') \cup V^*$.

- If $\mathrm{root}(\beta) \in \mathrm{alloc}(\phi_3)$, then $\mathrm{root}(\beta)$ occurs twice in $\mathrm{alloc}(\phi\sigma)$ because $\phi\sigma = \phi_3 * \eta_1 * \eta_2$; hence, it also occurs twice in $\mathrm{alloc}(\phi)$ because $\mathrm{root}(\beta) \notin \mathrm{codom}(\sigma)$. This entails that $\phi$ is heap-unsatisfiable, a contradiction.

Thus we get a contradiction, which entails that Condition 9 in Definition 4.31 is satisfied. □

We now introduce a restricted form of variable renaming$^4$. The definition is useful to straightforwardly detect cycles in a proof tree, which is essential for efficiency. For each sort $s$, we consider infinite (fixed) sequences of pairwise distinct variables of sort $s$: $x_i^s$, with $i \in \mathbb{N}$ (not occurring in the root sequent). A sequent $S'$ occurring in a proof tree with root $S$ is *normalized* if, for every variable $y$ of sort $s$ occurring in $\mathcal{V}(S') \setminus \mathcal{V}(S)$, there exists $i \le |S'|$ such that $y = x_i^s$. It is clear that every sequent $S'$ can be reduced in polynomial time to a normalized sequent. Indeed, it suffices to rename all the variables $y_1, \dots, y_n$ of sorts $s_1, \dots, s_n$ occurring in $S'$ but not in $S$ by the variables $x_1^{s_1}, \dots, x_n^{s_n}$, respectively. As $n$ cannot be greater than the size of $S'$, the obtained sequent is normalized. Such an operation is called a *normalization*.

**Lemma 5.27.** Assume that $\mathrm{ar}_{max}(\mathfrak{R}) \le \kappa$, for some fixed $\kappa \in \mathbb{N}$. For every sequent $S$, the number of sequents occurring in a proof tree with root $S$ is polynomial w.r.t. $|S| + |\mathfrak{R}|$, up to normalization.

**Proof:**

By definition, every descendant of $S$ is either an I-free descendant of $S$ or an I-free descendant of some I-reducible sequent $S'$. By Condition 6 in Definition 4.31, $\mathbb{R}$ applies with the highest priority on $S$, eventually yielding a (unique) sequent equality-free $S''$ of the form $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \zeta$, with $|S''| \le |S|$ and $\mathcal{V}(\phi) \subseteq \mathcal{V}(S)$. By Lemma 5.26, every I-free sequent $S'$ is a companion of of $\phi \wedge \xi$.

<footnote>$^4$Note that we cannot assume that sequents are taken modulo variable renaming, since identity would then be difficult to test (it would be equivalent to the well-known graph isomorphism problem).</footnote>
By Lemma 5.24, the number of such sequents $S'$, after normalization (w.r.t. $S''$), is polynomial w.r.t. $|\phi| + |\mathfrak{R}|$ (hence w.r.t. $|S| + |\mathfrak{R}|$). Indeed, it is clear that the normalized form of $S'$ is also a companion of $\phi \wedge \xi$ and by definition it only contains variables in $\mathcal{V}(S'') \cup \{x_i^s \mid i \le |S'|\}$. Furthermore, $|S'|$ is polynomial w.r.t. $|S| + |\mathfrak{R}|$, thus the same property holds for $\text{card}(\mathcal{V}(S'))$. Then the proof follows immediately from Lemma 5.12. □

Putting everything together, we derive the main result of the paper:

**Theorem 5.28.** The validity problem for sequents $\lambda \vdash_{\mathfrak{R}}^V \gamma$, where $\mathfrak{R}$ is a loc-deterministic set of P-rules with $\text{ar}_{\text{max}}(\mathfrak{R}) \le \kappa$ and $\text{record}_{\text{max}}(\mathfrak{R}) \le \kappa$, for some fixed number $\kappa$, is in PTIME.

**Proof:**

By Theorems 5.13 and 5.22, $\lambda \vdash_{\mathfrak{R}}^V \gamma$ is valid iff it admits a fully expanded proof tree. We first apply inductively the inference rules in all possible ways, starting with the initial sequent $\lambda \vdash_{\mathfrak{R}}^V \gamma$ and proceeding with all the descendants of $\lambda \vdash_{\mathfrak{R}}^V \gamma$, until we obtain either an axiom or a sequent that has already been considered, up to normalization. By Lemma 5.27, the number of such descendants (up to normalization) is polynomial w.r.t. $|S| + |\mathfrak{R}|$, thus it suffices to show that each inference step can be performed in polynomial time. This can be established by an inspection of the rules. We first observe that the set of all possible rule applications can be computed in polynomial time w.r.t. the size of the conclusion (in particular, both the number of premises and their size are always polynomial w.r.t. the size of the conclusion): this is straightforward to check for all rules except for S, for which the result stems from Proposition 4.34. Also, it is straightforward to verify that the application conditions of the rules can be tested in polynomial time.

Afterwards, it suffices to compute the set of provable sequents among those that are reachable from the initial one and check whether $\lambda \vdash_{\mathfrak{R}}^V \gamma$ occurs in this set. Since infinite proof trees are allowed, we actually compute the complement of this set, i.e., the set of sequents that are *not* provable. This can be done in polynomial time, using a straightforward fixpoint algorithm, by computing the least set of sequents $S$ such that, for all rule applications with conclusion $S$, at least one of the premises is not provable. More precisely, a sequent is not provable if it has no successor (no rule can be applied on it), or more generally, if for all possible rule applications, at least one of the premises is not provable.

Note that, in order to apply rule S on a sequent that is not narrow, it is necessary to check that the left premise is valid, and this must be done by recursively applying the proof procedure. This is feasible because the left premise is always narrow (since its right-hand side is a predicate atom). Consequently, the computation of valid sequents must be performed in two steps, first for narrow sequents, then for those that are not narrow, as the application of the rules on non narrow sequents depends on the validity of narrow sequents. By Proposition 4.32 all the descendants of narrow sequents are also narrow, hence the converse does not hold, and the procedure is well-founded. □

# 6. Conclusion

A proof procedure has been devised for checking entailments between Separation Logic formulas with spatial predicates denoting recursive data structures, for a new class of inductive rules, called loc-deterministic. The soundness and completeness of the calculus have been established. The conditions
imposed on the data structures are stronger than those considered in [13, 14] but on the other hand the procedure terminates in polynomial time, provided the arity of the predicates is bounded. Both the considered fragment and the proof procedure are very different from previously known polynomial-time decision procedures for testing entailments [7, 5]. In particular, the considered formulas may contain several non-built-in and non-compositional predicates (in the sense of [11]), and the structures may contain unallocated nodes, denoting data (with no predicate other than equality). In addition, several lower bounds have been established for the entailment problem, showing that any relaxing of the proposed conditions makes the problem untractable.

Future work includes the implementation of the procedure and the evaluation of its practical performance. The combination with theory reasoning (to reason on data stored inside the structures) will also be considered. In particular, it would be interesting to define a fragment that encompasses both the loc-deterministic P-rules considered in the present paper and the SHLIDe fragment defined in [18], as the conditions defining both classes of rules are very different and non comparable, as evidenced by the examples and explanations given in the introduction of the paper.

## References

[1] Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, *Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures*, volume 4111 of LNCS, pages 115-137. Springer, 2005.

[2] Josh Berdine, Byron Cook, and Samin Ishtiaq. Slayer: Memory safety for systems-level code. In Ganesh Gopalakrishnan and Shaz Qadeer, editor, *Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings*, volume 6806 of LNCS, pages 178-183. Springer, 2011.

[3] Cristiano Calcagno and Dino Distefano. Infer: An automatic program verifier for memory safety of C programs. In Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, *NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings*, volume 6617 of LNCS, pages 459-465. Springer, 2011.

[4] Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In *22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings*, pages 366-378. IEEE Computer Society, 2007. doi:10.1109/LICS.2007.30.

[5] Taolue Chen, Fu Song, and Zhilin Wu. Tractability of separation logic with inductive definitions: Beyond lists. In Roland Meyer and Uwe Nestmann, editors, *28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany*, volume 85 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.

[6] H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata, 2007. release October, 12th 2007.

[7] B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In *Proc. of CONCUR'11*, volume 6901 of LNCS. Springer, 2011.
[8] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment checking in separation logic with inductive definitions is 2-exptime hard. In Elvira Albert and Laura Kovács, editors, *LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020*, volume 73 of *EPiC Series in Computing*, pages 191–211. EasyChair, 2020.

[9] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable entailments in separation logic with inductive definitions: Beyond establishment. In *CSL 2021: 29th International Conference on Computer Science Logic*, EPiC Series in Computing. EasyChair, 2021.

[10] Mnacho Echenim and Nicolas Peltier. A proof procedure for separation logic with inductive definitions and data. *J. Autom. Reason.*, 67(3):30, 2023.

[11] Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. Compositional entailment checking for a fragment of separation logic. *Formal Methods Syst. Des.*, 51(3):575–607, 2017.

[12] Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. On automated lemma generation for separation logic with inductive definitions. In *ATVA 2015, Proceedings*, pages 80–96, 2015.

[13] Radu Iosif, Adam Rogalewicz, and Jiri Simacek. The tree width of separation logic with recursive definitions. In *Proc. of CADE-24*, volume 7898 of LNCS, 2013.

[14] Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. Deciding entailments in inductive separation logic with tree automata. In Franck Cassez and Jean-François Raskin, editors, *ATVA 2014, Proceedings*, volume 8837 of LNCS, pages 201–218. Springer, 2014.

[15] Samin S Ishtiaq and Peter W O'Hearn. Bi as an assertion language for mutable data structures. In *ACM SIGPLAN Notices*, volume 36, pages 14–26, 2001.

[16] Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. *J. Funct. Program.*, 28:e20, 2018.

[17] Jens Katelaan and Florian Zuleger. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In Elvira Albert and Laura Kovács, editors, *LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020*, volume 73 of *EPiC Series in Computing*, pages 390–408. EasyChair, 2020.

[18] Quang Loc Le and Xuan-Bach D. Le. An efficient cyclic entailment procedure in a fragment of separation logic. In Orna Kupferman and Pawel Sobocinski, editors, *Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings*, volume 13992 of LNCS, pages 477–497. Springer, 2023.

[19] Christoph Matheja, Jens Pagel, and Florian Zuleger. A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. *ACM Trans. Comput. Log.*, 24(1):1:1–1:76, 2023. doi:10.1145/3534927.

[20] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In *17th IEEE Symposium on Logic in Computer Science (LICS 2002)*, 22-25 July 2002, *Copenhagen, Denmark, Proceedings*, pages 55–74. IEEE Computer Society, 2002.

[21] The Coq Development Team. *The Coq Proof Assistant Reference Manual V7.1*. INRIA-Rocquencourt, CNRS-ENS Lyon (France), October 2001. http://coq.inria.fr/doc/main.html.