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

The Relationship between Craig Interpolation and Recursion-Free Horn Clauses

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

scope and results

The report connects interpolation problems used in software model checking with recursion-free Horn-clause fragments. The introduction says, “We systematically examine binary interpolation, inductive interpolant sequences, tree interpolants, restricted DAG interpolants, and disjunctive interpolants, and show the recursion-free Horn clause problems to which they correspond.” (Sec. 1, p. 1), and the paper gives reductions in both directions. Theorem 1 (p. 7) says that, for each line of Table 1, an interpolation problem of the stated form can be polynomially reduced to syntactically solving a set of Horn clauses in the stated fragment, and that syntactically solving Horn clauses in the stated fragment can be polynomially reduced to solving a sequence of interpolation problems of the stated form. The report also gives complexity results for solvability over quantifier-free Presburger arithmetic (Sec. 6, Fig. 6, p. 15: co-NP for tree-like, co-NEXPTIME for general recursion-free; Lemma 3 puts linear clauses in co-NP, Lemma 4 shows head-disjoint clauses co-NEXPTIME-hard; most results come from [27]), and argues that clause sets without infinite resolution derivations are renamable-Horn (Sec. 7, Theorem 2, p. 17). The result is a recipe for turning a verification path or call tree into constraints whose relation predicates are inferred by an interpolation engine.

The paper’s running program computes f(n)=n+1 recursively and asserts res == x+1 (Sec. 3, pp. 2–4). Each control-flow state gets a relation symbol; visible state variables are its arguments, and a function relation summarizes calls. The assertion is represented by a clause with head false; satisfying the clauses therefore proves that the error condition is unreachable. The paper says, “The rest of the clauses are one to one translation of the edges in the control flow graph” (Sec. 3, p. 3). A solution maps every relation symbol to a formula, and replacing symbols by those formulas must make every clause valid (Sec. 3, p. 4).

technique: encode a program as Horn clauses

Use this when a verifier needs procedure summaries or invariant predicates that an SMT interpolation solver can synthesize.

  1. Create one uninterpreted relation r_i for each control-flow state and pass only variables visible at that state (Sec. 3, p. 2). Keep locals out of a function summary’s arguments when callers cannot observe them.
  2. Translate each edge to a clause whose body contains the source relation and edge transfer constraint and whose head is the destination relation (Sec. 3, pp. 2–3). For a call, add the summary relation and connect arguments and return values.
  3. Add a false-headed clause whose body is the asserted error condition (Fig. 2, p. 3). Solving requires that body be false.
  4. Obtain recursion-free clause sets from recursive ones by finite unwinding (Sec. 3, p. 4; examples in Sects. 5.3 and 5.5, where Example 2 duplicates clauses with primed relation symbols). The paper says the recursion-free case “is instrumental for constructing verification procedures operating on Horn clauses”.
  5. Ask the solver for formulas interpreting relation symbols; substitute them and check all clauses.

Inference: in Verus, a spec fn can describe a relation’s mathematical predicate and requires/ensures can express edge transfer and summary contracts. A loop invariant and assert correspond to the synthesized relation and false clause, but Verus requires the proof obligations to be discharged by its SMT backend rather than accepting a Horn relation assignment automatically. Rust ownership and executable code remain; the paper’s uninterpreted state relations are a verification abstraction.

technique: binary Craig interpolation

For an unsatisfiable conjunction A ∧ B, compute I with A |= I, I |= ÂŹB, and only variables shared by A and B. The paper defines this as: “A Craig interpolant is a constraint I such that A |= I and B |= ÂŹI, and such that fv(I) ⊆ fv(A) ∩ fv(B)” (Sec. 4, p. 5).

  1. Compute shared variables x̄ = fv(A) ∩ fv(B) (Sec. 5.1, p. 7).
  2. Introduce fresh relation p(x̄).
  3. Emit A → p(x̄) and B ∧ p(x̄) → false (Sec. 5.1, p. 7).
  4. Solve the two Horn clauses; the interpretation of p is the interpolant.

Inference: a Verus analogue is to state A as a requires fact, prove an intermediate predicate p with assert, and use the postcondition to prove !B; the variable restriction is a design constraint on the predicate’s arguments, not a Verus keyword.

technique: inductive sequences and tree interpolants

Use an inductive sequence for a linear path T1 
 Tn. Introduce p_i with arguments consisting of variables shared by the prefix and suffix, then emit p0, p0 ∧ T1 → p1, 
, pn → false (Sec. 5.2, p. 8). The sequence obeys I0=true, In=false, and I_{i-1} ∧ Ti |= Ii; the report notes that simultaneous solvers can derive the whole sequence (Sec. 5.2, p. 7).

Use tree interpolation when procedure calls branch; the paper says the tree structure corresponds to part of a program’s call graph (Sec. 5.3, p. 8). Label each tree node with its constraint, set the root interpolant to false, require each node’s label plus its children’s interpolants to entail its interpolant, and restrict variables to those occurring both in the node’s subtree labels and in labels outside the subtree (Sec. 5.3, p. 8). The clauses are p_0 → false and, for each node v, φ(v) ∧ (conjunction of p_w over children w) → p_v (Sec. 5.3, p. 10). The paper states, “Tree interpolants strictly generalise inductive sequences of interpolants” (Sec. 5.3, p. 8). For a constraint language with the interpolation property, a tree interpolant exists if and only if the conjunction of all node labels is unsatisfiable; the proof computes interpolants one node at a time (children before parents) by repeated binary interpolation (Lemma 1, p. 9). The paper also states that symmetric interpolants [23] are tree interpolants with a flat tree (p. 10).

Inference: Verus can encode each I_i as a ghost predicate or lemma postcondition and each tree edge as a lemma call. invariant is written on a loop, not called as a function; relation symbols become predicates or proof functions. The paper’s simultaneous interpolation is solver functionality that Verus does not expose directly.

technique: restricted DAG and disjunctive interpolation

Use restricted DAG interpolation to reason about multiple program paths simultaneously (Sec. 5.4, p. 11). For each node, allow variables occurring in both incoming and outgoing edge labels; require entry true, exit false, and for each edge I(v) ∧ LV(v) ∧ LE(v,w) |= I(w) ∧ LV(w) (Sec. 5.4, p. 11). For each edge the encoding emits a linear clause LV(v) ∧ LE(v,w) ∧ p_v → p_w and a second clause LV(v) ∧ ¬LV(w) ∧ LE(v,w) ∧ p_v → false, plus true → p_en and p_ex → false (Sec. 5.4, p. 12). The paper says DAG interpolants are incomparable in expressiveness to tree interpolation, and that they can be reduced to tree interpolants only “at the cost of a potentially exponential growth in the number of clauses” (Sec. 5.4, pp. 11–12). Footnote 4 (p. 11) says the paper assumes the definition in [1, Def. 4] contains a mistake and uses a corrected variable condition.

Disjunctive interpolants are a generalisation of tree interpolants in which the tree is an and/or-tree: and-branching is a clause with several body literals, or-branching is several clauses with the same head symbol (Sec. 5.5, p. 13). Solving body-disjoint clauses reduces to solving the maximal tree-like subsets (Lemma 2, p. 13); the proof sketch combines the subset solutions by a positive Boolean combination for each relation symbol, as in Example 2 (p. 14), where disjunctions are used for r9 and rf and a conjunction for r2. The paper’s taxonomy maps “Disjunctive interpolants [27]” to “Body disjoint Horn clauses” (Table 1, p. 6). Inference: a Verus implementation can share a ghost predicate across branches and prove each branch’s transition lemma, but exponential path splitting and quantifier/aliasing limits remain assumptions.

evidence, trust, limits, and product relevance

The evidence is mathematical: Theorem 1 gives the polynomial reductions stated above (the Horn-to-interpolation direction reduces to a sequence of interpolation problems), and the running example has a concrete relation assignment (Figs. 2–5, pp. 3–12). The paper mentions that its tool Eldarica found the solution in Fig. 3. No benchmark denominator or runtime table is reported in this report. Trusted components are the underlying constraint theory, interpolation procedure, and the soundness of the Horn encoding; the report does not prove a particular SMT implementation correct. Recursion-free acyclicity is required for the reductions; the paper handles recursive programs only by noting that recursion-free sets are usually extracted by finite unwinding (Sec. 3, p. 4). Lemma 1 holds only for constraint languages with the interpolation property, and the paper gives no implementation or evaluation of the reductions. Inference: these techniques threaten a verified-Rust product mainly by making invariant and procedure-summary synthesis more automatic; they do not replace Rust type/ownership reasoning or establish end-to-end trust in generated proof scripts.

techniques for the catalog

  • horn encoding: map control-flow states and calls to relation-symbol clauses, with assertion errors as false heads
  • binary interpolation: synthesize a shared-variable predicate from two clauses A → p and B ∧ p → false
  • inductive and tree interpolation: derive path or call-tree invariants by composing transfer constraints and child predicates
  • dag/disjunctive interpolation: share predicates across paths or combine body-disjoint Horn clauses

Last edited: