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

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification

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

scope and result

The paper reduces sorting-program properties to constrained Horn clause (CHC) satisfiability. Its case study covers insertion sort, selection sort, quicksort, and mergesort, with permutation, orderedness, length, and sum properties. The central obstacle is inductive lists: the paper states, “Unfortunately, when the properties to be verified refer to programs that act on inductively defined data structures, such as lists or trees, then the satisfiability proofs via CHC solvers becomes much harder, or even impossible, because those solvers do not natively incorporate induction principles relative to those data structures.” (Introduction, p. 48). The proposed response is a two-phase transformation: remove lists by fold/unfold elimination and difference predicates, then solve the resulting linear-integer-arithmetic (LIA) and Boolean CHCs with Eldarica. The paper explicitly says, “The verification is done into two phases.” (Introduction, p. 49).

technique: translate a functional property to CHCs

Use this when the program is a terminating functional program over an inductive datatype and the desired property can be stated as a relation between input and output values (Inference: the paper’s correctness hypothesis, Section 4, p. 60, is that the initial predicates “define total functional relations”, which holds “in the case when those predicates are the CHC translation of functional programs that terminate for all inputs”). The paper says the transformations in Sections 2 and 3 “are done by an interactive system” (Section 2, p. 49), not by a fully automated tool.

  1. Encode each function as a relational CHC predicate. For insertion sort, the paper gives ins, insertionSort, and count clauses for list constructors and recursive cases (Section 2, pp. 49–50).
  2. Encode violation of the target property as a false clause. For permutation, the paper uses false :- N1=\=N2, insertionSort(L,S), count(X,L,N1), count(X,S,N2). (Section 2, p. 50).
  3. Establish that the translation preserves the program meaning. The paper states, “The translation ensures that (i) ins(X,L,L1), (ii) insertionSort(L,S), and (iii) count(X,L,N) hold iff (i) ins X L = L1, (ii) insertionSort L = S, and (iii) count X L = N, respectively, hold in the program InsertionSort.” (Section 2, p. 50).
  4. Ask a CHC solver to prove satisfiability. For the insertion-sort permutation clauses the paper says, “state-of-the-art CHC solvers, such as Eldarica or Z3, fail to prove satisfiability of those clauses, because these solvers do not incorporate any induction principle on lists” (Section 2, p. 50). The Appendix reports a 120-second timeout for Eldarica on all direct clause sets (Appendix, p. 64); it reports no Z3 run.

Inference: In Verus, the executable Rust sorting function would remain ordinary code, while a spec fn can describe the mathematical list or sequence result and a proof fn can establish the contract. The CHC relation becomes a Verus requires/ensures contract plus lemmas over Seq; the paper’s OCaml and Prolog syntax does not carry over. The contract itself and termination assumptions remain trusted inputs to the proof.

technique: eliminate inductive data with fold/unfold and difference predicates

Use this when direct CHC solving cannot reason by induction over lists or trees, especially when recursive calls produce mismatched intermediate values that prevent ordinary folding.

  1. Introduce an auxiliary predicate whose arguments are the non-list variables in the property body. The insertion-sort example defines new1(X,N1,N2) :- insertionSort(L,S), count(X,L,N1), count(X,S,N2) and folds the error clause to false :- N1=\=N2, new1(X,N1,N2) (Section 2, p. 51).
  2. Unfold new1 using program clauses. The paper obtains base and recursive clauses 12–14; clauses 13 and 14 cannot be folded because list variables such as S and S1 mismatch (Section 2, p. 51).
  3. Apply the six-step difference-predicate procedure. The paper’s steps are: “Step 1. Embed”; “Step 2. Rename”; “Step 3. Match”; “Step 4. Introduce a Difference Predicate”; “Step 5. Replace”; and “Step 6. Fold.” (Section 2, pp. 51–53).
  4. In Embed, identify body atoms that are variants of atoms in the folding clause. In Rename, make fresh variables. In Match, compute the consistent substitution and mark the unmatched conjunction. These operations are shown for clauses 13 and 10 (Section 2, pp. 51–52).
  5. In Introduce, define a predicate relating the non-list outputs of the removed and added conjunctions. The paper defines diff1(X, N2a, N2) : - ins(X, S1, S), count(X, S, N2), †† count(X, S1, N2a)., where the marker †† separates the atoms to remove from the clause being folded (left) from the atoms to add (right) (Section 2, p. 52). It says, “This atom addition is required for preserving satisfiability of the derived clauses.” (Section 2, p. 52).
  6. Replace the mismatching conjunction of the clause to be folded with the mismatching conjunction of the folding clause plus the head of the difference predicate (Step 5), then fold (Step 6). Clause 13 becomes new1(X,N1,N2) :- N1=N+1, new1(X,N,N2a), diff1(X,N2a,N2) (clause 13f, Section 2, p. 52). The paper says “It can be shown that the above Steps 1–6 preserve satisfiability of clauses” and that “A detailed proof of this fact is outside the scope of the present paper” (p. 52).
  7. Continue elimination until all list arguments disappear. For insertion sort no new difference predicates are needed at this stage; the resulting clauses use only LIA and Boolean constraints, and Eldarica constructs a model, including new1(A,B,C) :- ((B = C), (B >= 0))., which shows property IS Perm (Section 2, p. 53).
  8. Read the model as an inductive lemma. Substituting the model of diff1 into clause 15 gives the lemma ∀ X, S1, S, N2, N2a. ins(X,S1,S) ∧ count(X,S,N2) ∧ count(X,S1,N2a) → (N2 = N2a + 1 ∧ N2a >= 0), i.e. inserting X raises its count by one; the paper says there is “a tight correspondence between the definition of the difference predicates and the lemmata which are needed for making the inductive proofs” (Section 2, pp. 53–54).

Inference: In Verus, the closest form is a ghost proof fn lemma that relates the result of inserting an element into a sequence to the old count, with ensures expressing the relation. A Verus Seq/Map model can replace list CHCs; assert and explicitly triggered lemmas can expose the arithmetic fact to the SMT solver. The paper’s fold, unfold, new1, and diff1 are transformation-level concepts, not Verus keywords. This mapping is an inference from the paper’s logical role for the predicates.

technique: scale the same construction to branching recursion

For quicksort, the paper repeats the six steps while handling two recursive calls. It creates two renamed copies of the new1 definition (clauses 9a and 9b), matches each quicksort call, and introduces diff1 for the partition/count atoms and diff2 for the append/count atoms (Section 3, pp. 56–58). The paper groups the mismatching atoms “by keeping together only the atoms that share common list variables” and adds the constraint X=Y to the bodies; it notes that a single combined difference predicate “would have allowed the elimination of lists” too (Section 3, pp. 57–58). Its satisfiability-preservation claim for Step 5 is conditional: “if the values of K and N which are arguments of the difference predicates diff1 and diff2, are functions of (X,Y,Ma,Mb) and (X,Y,Na,Nb), respectively” (p. 58), and its proof is “outside the scope of this paper”. The final list-free clauses 10, 11, 17, 18, and 21–34 are solved by Eldarica, which computes a model “expressible in LIA (see Appendix)”, proving QS Perm; QS Sum is proved with the same technique (Section 3, p. 59). MergeSort’s sum property MS Sum is also proved; its CHCs, transformed CHCs and model appear only in the Appendix (6.10, pp. 73–75), with Section 3 (p. 60) giving just the property.

Inference: A Verus proof for branching recursion needs separate lemmas for each recursive result and a lemma connecting partition/append to the multiset or sum specification. The paper supplies the decomposition pattern; exact Rust proof code is not in the paper.

evidence, trust, and limits

The appendix lists ten program/property pairs: four insertion-sort properties, three selection-sort properties, two quicksort properties, and one mergesort property (Appendix, p. 64). Eldarica was invoked with $eldarica -horn -hsmt -sol filename; every direct, pre-transformation set failed to yield a model within a 120-second timeout, while transformed sets were solved (Appendix, p. 64). The reported hardware was an Intel Core i7-8550U at 1.80 GHz × 4 cores (8 threads) with 16 GB RAM (Appendix, p. 64). No aggregate success percentage or per-property runtime denominator is reported, so a broader performance claim would be unsupported.

The correctness discussion assumes initial predicates define total functional relations, guaranteed for terminating functional programs, and requires functionality of introduced difference predicates; the latter can be checked in the solver model (Section 4, p. 60). Even without difference-predicate functionality, the paper says satisfiability of derived clauses implies satisfiability of initial clauses, which can suffice for some verification goals (Section 4, p. 60). Mechanization of difference-predicate introduction is not complete: “At the time of writing we have made some initial steps towards an implementation of the extended Elimination Algorithm”, and Step 3 (Matching) “seems to be the most critical one” (Section 4, p. 60). The paper also leaves “a thorough experimental evaluation” to future work (Section 3, p. 60) and calls itself “ongoing work” (Section 4, p. 61).

techniques for the catalog

  • CHC relational encoding — translate recursive functional code and a negated property into constrained Horn clauses
  • inductive-data elimination — use fold/unfold transformations to remove list or tree arguments before SMT solving
  • difference-predicate lemma generation — add predicates relating mismatched intermediate outputs so folding preserves satisfiability
  • model-to-lemma extraction — interpret the solver’s LIA model as the arithmetic lemma needed by an inductive proof
  • branching-recursion decomposition — rename the folding clause once per recursive call, group the mismatching atoms by shared list variables, give each group a difference predicate, and fold once per recursive call

Last edited: