Interpolation in local theory extensions

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

problem and result

The paper studies Craig interpolants for inconsistent ground clauses in a theory extension. Given sets of ground clauses A and B with A ∧ B inconsistent modulo a theory, an interpolant I is a ground formula over symbols common to A and B with A ⊨ I and B ∧ I inconsistent; it “can be regarded as a “local” explanation for the inconsistency of A ∧ B” (Section 1, p. 1). The paper states: “In this paper we study possibilities of obtaining ground interpolants in theory extensions.” (Section 1, p. 1.) Its central result is a hierarchical procedure that reduces interpolation in a local extension T1 = T0 ∪ K to interpolation, entailment and separating-term computation in a base theory T0 (Sections 5–6, Theorem 6.2). The procedure needs: T0 convex, T0 P-interpolating, ground interpolation in T0, and K made of clauses of the special type (5.1) (Introduction, p. 2; Assumptions 1–5, pp. 13–14).

Inference: For Verus, the relevant role is generating a concise explanation or refinement predicate from an unsatisfiable SMT verification condition. The paper is about first-order theories and ground clauses, so using it for Rust requires an encoding of heap, ownership, and contracts into a compatible theory.

technique 1: recognize a local theory extension

What it is. T1 extends T0 with new function symbols and universally quantified clauses K (Section 4, p. 7). Locality means that to refute a ground set G, it suffices to instantiate K only at extension-function terms already occurring in G or K. Definition 4.3 gives the condition (Loc) and its finite-set version (Locf) through weak partial models (pp. 7–8); the paper says it uses (Locf) as its definition of “local”. Informal statement: “An extension T0 ⊆ T0 ∪ K is local if, in order to prove unsatisfiability of a set G of clauses with respect to T0 ∪ K, it is sufficient to use only those instances K[G] of K in which the terms starting with extension functions are in the set st(G, K) of ground terms which already occur in G or K.” (Section 4.1, p. 7.)

When to use it. Inference: use locality when a solver obligation contains extension functions constrained by axioms of the kinds in Theorem 4.6 or Example 5.5 (monotone, bounded, semi-Galois functions, free functions), and when instantiating all universally quantified axioms would be expensive. The paper’s examples do not include array theory; it notes that for arrays “there is no ground interpolant” in some cases (Section 3.2, p. 6).

How to establish it.

1. Specify a base theory T0, extension symbols Σ1, and clauses K (Section 4, p. 7).
2. Restrict candidate instances to the finite term set st(K,G) (Definition 4.3, p. 7).
3. Check that weak partial models of those instances embed into total models. The sufficient condition is (Emb^fd_w): every weak partial model with finite definition domains for the extension functions weakly embeds into a total model of T1 (Section 4.2, p. 8).
4. Ensure terms starting with extension functions are flat and linear (Σ1-flat and Σ1-linear, Definition 4.4); Theorem 4.5 (cited from [15, 17]) then derives (Locf) from (Emb^fd_w) (p. 8).

Verus form. Inference: treat the base as arithmetic and equality facts generated by Verus, and treat selected specification functions as Σ1. Encode each contract axiom as a universally quantified lemma. Verus does not expose partial-model embedding as a user construct; an external instantiation pass could generate only terms occurring in the verification condition, while Verus/Z3 checks the resulting ground obligations. Inference: heap maps and recursive datatypes often violate the flat/linear shape and need a separate locality argument.

Evidence. Theorem 4.6 lists local extensions of posets, totally-ordered sets, semilattices, distributive lattices, Boolean algebras, and real, rational or (a subtheory of) integer arithmetic, with boundedness and guarded boundedness, monotone plus bounded, Leq(f,g) with monotonicity, and semi-Galois (SGc) conditions (pp. 8–9; proof in Appendix B, pp. 27–29). Lipschitz extensions of the reals are listed as local in Section 4.3 (p. 8, from [15]). Example 4.8 applies the criterion to semilattices with monotone f,g satisfying SGc(f,g) (p. 10).

Limits and assumptions. Theorem 4.5 is a sufficient condition and requires flatness, linearity, and finite-domain embeddability. Inference: locality is a property of the axioms and base theory; it is not automatic for arbitrary quantified contracts, so a Verus project must prove these conditions for each encoded specification family or conservatively fall back to ordinary quantifier instantiation.

technique 2: hierarchical satisfiability reduction

What it is. Given a ground clause set G, locality reduces satisfiability in T1 to a base-theory problem by instantiating, flattening, purifying, and adding congruence constraints (Section 4.4, p. 9, “for details cf. [15]”). Theorem 4.7 (cited from [15]) states the equivalence among: T0 ∧ K ∧ G has a model; T0 ∧ K[G] ∧ G has a weak partial model where all terms in st(K,G) are defined; the purified version has such a weak partial model; and T0 ∧ K0 ∧ G0 ∧ Con[D]0 has a total Σ0-model.

How to do it.

1. Use locality to form K[G]; retain only instances whose extension terms occur in G or K (Section 4.4, Step 1, p. 9).
2. Flatten and purify every extension term. Introduce constants for arguments and for each term t = f(g1,…,gn), with definitions ct ≈ t; obtain K0 ∧ G0 ∧ D, where D contains unit definitions f(c1,…,cn) ≈ c (Step 2, p. 9).
3. Add congruence instances Con[D]0: c_i ≈ d_i for all i implies c ≈ d for matching extension applications (Theorem 4.7, p. 9).
4. Ask the base solver whether T0 ∧ K0 ∧ G0 ∧ Con[D]0 has a total model (Step 3 and Theorem 4.7, p. 9).

Verus form. Inference: this resembles a preprocessing pass over Verus/Z3 verification conditions: name each non-base term with a ghost constant, emit defining equalities, and add congruence lemmas. Verus’s assert and lemma can discharge the resulting base facts; the flattening transformation itself is outside Rust. Inference: preserving ownership-sensitive aliases requires including the alias relation in D, otherwise the reduction can be unsound for memory state.

Evidence. Example 4.8 carries out all three steps for A: d ≤ g(a) ∧ a ≤ c and B: b ≤ d ∧ f(b) ≰ c; the reduced semilattice clauses derive b ≤ a1, then b1 ≤ a, contradicting a ≤ c and b1 ≰ c (p. 10). Theorem 4.7 gives the formal equivalence.

Limits. Inference: the reduction is finite only because G is finite and locality bounds instantiation; the base solver is trusted for the resulting satisfiability result; and this is a solver architecture, not a proof that an arbitrary SMT encoding has a finite local closure.

technique 3: separate mixed clauses with shared terms

What it is. The paper says Theorem 4.7 cannot be used directly to generate an interpolant, among other reasons because “The clauses in K[DA ∧ DB] and the instances of congruence axioms (and therefore the clauses in K0 ∧ Con[DA ∧ DB]0) may contain combinations of constants and extension functions from A and B.” (Section 5, p. 11.) Such mixed clauses are separated into an A-part and a B-part using a term composed only of symbols common to both sides. Assumption 2 (P-interpolation) guarantees a shared term t with A ∧ B ⊨ aRt ∧ tRb for related endpoints a (in A) and b (in B); strong P-interpolation additionally gives A ⊨ aRt and B ⊨ tRb (Section 5.2, p. 13). The paper also considers only sets A, B of unit clauses, saying general clauses are handled by standard methods (p. 13).

How to do it.

1. Partition purified clauses and congruence constraints into A-only, B-only, and mixed sets (Section 5.2 and Remark 5.6, pp. 14–15).
2. Pick a clause of H whose premises are all entailed by A0 ∧ B0 (found using convexity). If it is mixed, for each premise c_i R_i d_i use P-interpolation to find common terms t_i with A0 ∧ B0 ⊨ c_i R_i t_i ∧ t_i R_i d_i (proof of Proposition 5.7, Case 2b, p. 16).
3. Introduce a fresh shared constant cf(t1,…,tn) for the extension term f(t1,…,tn) (Proposition 5.7, p. 16).
4. Replace the mixed rule with an A-side monotonicity rule deriving c R cf(t) and a B-side extension rule deriving cf(t) R d; transitivity of R preserves the original conclusion (Proposition 5.7, pp. 16–17).
5. Repeat on the remaining clauses (induction on the number of clauses in H); the resulting separated conjunction is unsatisfiable in T0 (Proposition 5.7(1), p. 15; Lemma 6.1, p. 18).

The paper’s worked example uses t=d and concludes with the interpolant f(d) ≤ c (Example 5.3, p. 12). Its explicit steps include replacing b ≤ g(a) → f(b) ≤ a with b ≤ d → f(b) ≤ f(d) and d ≤ g(a) → f(d) ≤ a. In that example f and g are both treated as shared because they occur together in SGc (relation f ∼ g, pp. 11–12).

Verus form. Inference: a Verus diagnostic could compute shared ghost terms from the common state variables of two path conditions, introduce a ghost value for each f(t) and prove the two monotonicity/contract halves separately. Verus has no built-in Craig interpolation or fresh-symbol separation procedure; this must be implemented in a VC postprocessor or as generated lemmas. Inference: shared terms should denote immutable mathematical state, not mutable references whose identity differs between paths.

Evidence. Proposition 5.7 (pp. 15–17) proves by induction that the separation exists and preserves unsatisfiability; Example 5.3 demonstrates the transformation and the reconstruction of I = f(d) ≤ c (p. 12).

Limits and assumptions. The method requires convexity, P-interpolation, ground interpolation in T0, a local extension in which every variable of every clause in K occurs below an extension function, and extension clauses of shape (5.1) (Assumptions 1–5, pp. 13–14). Clauses of other shapes are outside Assumption 5; footnote 4 (p. 14) says more general clauses are “not discussed here”.

technique 4: compute the interpolant hierarchically

The procedure is in Figure 1 (p. 19). The paper states, “The method is hierarchical: the problem of finding interpolants in T1 is reduced to that of finding interpolants in the base theory T0.” (Section 1, p. 2.) The paper gives no implementation of this exact procedure; Section 8 says an earlier implementation for linear arithmetic with free function symbols [11] “differs a bit from the one presented here” (p. 24).

1. Purify using locality, flattening and purification; obtain base formulae H ∧ A0 ∧ B0 with H = K0 ∧ Con[DA ∧ DB]0, and set Δ := T (Figure 1, Step 1).
2. Repeat as long as possible: choose a clause C ∈ H whose premise is entailed by A0 ∧ B0 ∧ Δ. If C is mixed, compute terms t_i separating its premises, replace it with an instance of monotonicity and an instance of a clause in K, remove C from H, add the two instances to Hsep and their conclusions to Δ; otherwise move C to Hsep and add its conclusion (Figure 1, Step 2).
3. Compute a base interpolant I0 in T0 for the separated formula (Figure 1, Step 3).
4. Replace every fresh separation constant ct recursively by the term t it denotes, yielding I in the original extension (Figure 1, Step 4; Corollary 5.9(2), p. 17).

Termination: “at every execution of the loop in Step 2, the number of mixed clauses decreases” (proof of Theorem 6.2, p. 19); this also needs separating terms t_i to be effectively computable (Assumption 2 in Theorem 6.2). Correctness follows from Lemma 6.1 and Corollary 5.9 (pp. 17–20). Theorem 6.2 states that under Assumptions 1–5 the procedure terminates and computes an interpolant for every inconsistent conjunction of ground unit clauses A ∧ B (pp. 18–20). Complexity: assume interpolants in T0 take time g(n), P-interpolating terms h(n), entailment k(n); the paper states that “The size n of the set of clauses obtained after the preprocessing phase is quadratic in the size of the input” and that the procedure runs “in time of order n · (k(n)+h(n))+g(n)” (p. 20).

Verus form. Inference: run this algorithm on a split verification condition to generate an abstraction predicate, then add the predicate to a subsequent requires/invariant and re-run Verus. The base interpolant may be encoded as a spec fn or a Boolean ghost expression; executable Rust does not carry it. Inference: the n in the complexity claim is the number of preprocessed clauses, not Rust lines, solver calls, or proof obligations.

applications and evidence

The paper also records the practical motivation: “Interpolants provide information about which new predicates need to be used for refining the abstraction.” (Section 2.2, p. 4.)

The paper motivates abstraction refinement with a water-level controller (Section 2.2, pp. 4–5): an abstract path of length 2 to overflow is checked in the concrete model, and with h, g, k, in, out as free functions the conjunction is satisfiable so spuriousness is not detected; with the axioms K it is unsatisfiable. Section 7.3 (pp. 23–24) computes the interpolant l′ < Loverflow for this path and says “The abstraction defined in Section 2.2 can then be refined by introducing another predicate L′ < Loverflow.” Section 7.2 (p. 22) computes the interpolant substance ∧ catalyzes(reaction) ≤ inorganic for the inconsistent chemistry database, and Section 7.1 (pp. 21–22, Theorem 7.1) shows that for local combinations of theories over a common base with ground interpolation, ground interpolants over shared constants exist. Example 6.4 (pp. 20–21) lists extensions with ground interpolation (free functions, monotone, Leq, SGc, bounded, and Lipschitz extensions, under the stated base theories).

This paper reports no benchmark numbers. The only empirical remark is in Section 8 (p. 24), about the special case of linear arithmetic with free function symbols implemented in [11]: “First tests suggest that the performance of our method is of the same order of magnitude as the methods which construct interpolants from proofs, and considerably faster on many examples.” Otherwise the evidence is formal theorems, worked symbolic examples, and the stated complexity bound.

Inference: the threat to agent-written verified Rust is moderate and indirect. Interpolant-guided refinement could reduce manual invariant discovery, but encoding ownership, heap shape, and nonlinear control flow into local extensions is a substantial engineering and soundness obligation. Inference: this paper’s specific contribution relative to ordinary SMT counterexamples is a structured, shared-symbol interpolant with a termination argument under stronger theory assumptions.

proved, trusted, and limitations

Proved in the paper: Lemma 5.1 (flattening and purification preserve interpolants), Theorem 4.6 (Appendix B) and Theorem 5.4 (Appendix C) for the example theories, separation of mixed Horn clauses (Proposition 5.7), Corollary 5.9 and Lemma 6.1, and terminating/correct hierarchical interpolation (Theorem 6.2). Cited from earlier work, not reproved here: Theorem 4.5 [15, 17] and Theorem 4.7 [15]. Treated as black boxes by the paper: the base-theory interpolation procedure, the entailment checks, and the computation of P-interpolating terms (assumptions (a)–(c) of the complexity paragraph, p. 20). Inference: a Verus deployment must also trust the VC translation, heap model, and reconstruction of fresh constants.

techniques for the catalog

• local theory extension — bound quantified instantiation to extension terms already present in the ground obligation
• hierarchical satisfiability reduction — flatten and purify extension terms, then solve congruence-augmented clauses in the base theory
• mixed-clause separation — split each mixed Horn rule through shared interpolating terms and fresh shared extension values
• hierarchical interpolant procedure — iterate separation, interpolate the pure base problem, and substitute fresh constants back to original terms
• abstraction-refinement use — turn an interpolant for a spurious counterexample into predicates that refine the next abstract-state check

Last edited: 2026-10-17