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

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

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

purpose and result

The paper introduces symbolic automatic relations (SARs), a finite automaton representation for relations over integer-labelled words, and uses them as a compositional language (closed under Boolean operations, with decidable emptiness) for recursive list properties. Satisfiability of formulas over SARs is undecidable in general. The central engineering result is a translation from a fragment of SAR formulas (the existential fragment, ÎŁÂč_sar) to constrained Horn clauses (CHCs) over integers. A CHC solver then supplies an automated, sound but incomplete satisfiability checker. The paper also gives an ICE-learning application: SAR formulas are candidate models for CHCs over lists, and the SAR checker is the teacher that checks candidates. The learner that would propose candidates is not implemented in the paper.

The authors state the problem directly: “reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers” (abstract, p. 1). Their claimed contribution is a checker “by a reduction to CHC solving” (abstract, p. 1), with effectiveness measured on three benchmark families. This is a backend technique rather than a Rust-language proof system.

technique 1: represent recursive relations as symbolic synchronous automata

What it is. A symbolic synchronous nondeterministic finite automaton (ss-NFA) reads several list words in lockstep. A transition has a source state, a destination state, and a label formula over the current letters and parameter variables (Definition 2, p. 6; the labels must form a decidable set to be “effective”). In all benchmarks the labels are quantifier-free linear integer arithmetic (Section 6, p. 18). The accepted convolutions of the input words define a symbolic automatic relation (SAR). SARs inherit Boolean closure and have decidable emptiness when the underlying label theory is decidable. The paper emphasizes: “Symbolic automatic relations (SARs) inherit good properties of automatic relations and symbolic automata: SARs are closed under Boolean operations” (Section 1, p. 2).

When to use it. Use an SAR when a relation compares corresponding positions of one or more recursively defined lists, while each local comparison is expressible in linear integer arithmetic. Examples include sortedness, list equality with a shift, nth, and the graph of insertion sort’s insert function. Limits stated by the paper: the “append” relation cannot be expressed (Section 1, p. 2), the paper treats lists of integers only (trees are left as an expected extension, Remark 3), and satisfiability of SAR formulas is undecidable in general (Theorem 1, Section 4, pp. 11–12), so the checker is sound but incomplete.

How to do it.

  1. Define the list relation as a synchronized automaton. Give states, initial and final states, and one transition for each recursive case. Put local arithmetic conditions on transitions. Example 1’s automata use labels such as l0 = l1 + 1 and l2 = x (Example 1, Section 3.1, p. 7).
  2. Encode list constructors and destructors as synchronized input tracks. A shifted track represents tail(X); padding symbols mark the end of a shorter word. The convolution operation is defined before the SAR definition (Definitions 4–5, Section 3.2, p. 8).
  3. Build higher predicates from the automaton. The paper expresses sorted(X) as R_M1(X, tail(X)), and defines nth(i,x,X) existentially using R_M2(x) and a constructed list (Example 2, p. 9).
  4. Combine predicates under Boolean operations (Proposition 3, p. 9: Δ⁰_sar and ΔÂč_sar formulas are closed under Boolean operations). The checker takes ΔÂč_sar formulas; if a predicate is defined with existential quantifiers, both the definition of the predicate and of its negation must be provided, and the tool itself translates inputs into the normal form of Section 5 (Section 6, pp. 17–18).

Verus form. Inference (not from the paper; I did not check Verus documentation): encode an executable Rust list as a ghost Seq<int> or a recursively defined mathematical sequence, and define a spec fn for each transition relation. A Verus spec fn can express the local arithmetic relation; requires and ensures on a proof function can connect the executable list operation to that relation. For a finite automaton, represent states as an integer or an enum in specifications and prove a transition invariant with a proof fn. The paper’s automata are mathematical and do not carry over as a Verus solver primitive: the automaton-to-CHC compiler and CHC backend would remain an external tool or would have to be reimplemented as ghost definitions and lemmas.

Evidence. The implementation accepts ss-NFAs and ΔÂč_sar formulas and automatically converts inputs to normal form. On 87 total instances, Ours-Eldarica solved 85 (72 valid, 13 invalid, and 2 instances not solved by the other tools), while Ours-HoIce solved 80 (67/13/1) and Ours-Spacer 59 (46/13/0) (Table 1, p. 19). These are solved-instance counts, not proof percentages; 85/87 is 97.7% for Ours-Eldarica. Average times over solved instances were 4.006 s for Ours-Eldarica, 5.275 s for Ours-HoIce, and 0.942 s for Ours-Spacer (Table 1, p. 19).

Failure and assumptions. The underlying transition labels are quantifier-free linear integer arithmetic in all benchmarks (Section 6, p. 18). Ours-Eldarica solved all instances except two. Of those, “one of them needs non-linear properties on integers such as x ≄ y × z”, so “the reduced CHC problem cannot be proved by the underlying CHC solvers used in the experiments”; the other is solved by Ours-HoIce (Section 6, p. 19). Appendix B adds that the only instance not verified by the paper’s tool with any backend is “sumfold-gte” (p. 29). The procedure is sound but incomplete, and the general satisfiability problem is undecidable (abstract, p. 1; Section 4, pp. 11–12). Inference: a Verus port inherits solver incompleteness and additionally depends on the correctness of the generated ghost specification.

technique 2: normalize SAR arguments and reduce them to CHCs

What it is. Section 5 says the reduction works for the ÎŁÂč_sar-formulas (p. 12) and targets CHCs “whose constraint theory is mere integer arithmetic”. The translation itself (Definition 9) is defined for normal formulas: list arguments cons-free and gap-free, integer arguments variables. A normal formula uses only nil or tail^n(X) list terms, includes every intermediate tail, and has integer variables as scalar terms (Definitions 8–9, pp. 13–14). For each automaton state q, create an integer CHC predicate q(...) describing possible next letters and parameters. Translate transitions, initial states, and final states into clauses. The result preserves satisfiability by making acceptance equivalent to deriving false: “We construct a set of CHCs Π such that M ⊹ ∃x∃X.nth(i, x, X) iff Π is unsatisfiable” (Section 5.1, p. 13).

When to use it. Use this reduction when the SAR formula is in the ÎŁÂč_sar fragment and can be normalized (Section 5, p. 12). The paper’s motivation is that “solving CHCs without data structures is easier in practice” (Remark 2, p. 11). Inference: the reduction does not apply unchanged to universal or higher SAR fragments, since the paper defines it only for ÎŁÂč_sar, and it is not a complete decision procedure (Theorem 1).

How to do it.

  1. Normalize list terms. Add ignored automaton tracks to make the set of tails gap-free. Rewrite scalar terms into automaton parameters. The paper calls both “easy” and treats cons-freeness as “the only nontrivial condition” (Section 5.2, p. 15).
  2. Eliminate cons by unrolling the automaton and passing the consed value as a parameter. The paper’s example replaces R_M2(x)(cons(1,cons(t,Y)),cons(0,Y),X,x) with R_M'2(x,y)(cons(1,Y),cons(0,tail(Y)),X,x,t) and preserves satisfiability (Lemma 1 example, p. 15).
  3. Introduce one CHC predicate per automaton state. For every transition p —φ→ q, emit a clause whose body includes the transition label, the shift relation between adjacent tails, padding constraints, and a not-at-end condition (Definition 9, p. 14).
  4. Add initial clauses. For each initial state q, emit q(v, x) ⇐ φ_nil ∧ φ_tail(nil) ∧ x = y: tracks whose term is nil must read padding, a padded tail^m(X) track forces a padded tail^(m+1)(X) track, and the automaton parameters are bound to the integer arguments (Definition 9, p. 14).
  5. Add acceptance clauses. For each final state emit ⊄ ← q(...) ∧ φ_end, so false is derived exactly when a final state is reached after all input is consumed (Definition 9, p. 14).
  6. Run the CHC solver. Theorem 2 states that a normal R_M(T, y) is satisfiable iff the translated CHCs are unsatisfiable (Section 5.3, p. 16); the proof associates a derivation of false with an accepting run and vice versa.

Verus form. Inference: represent each state predicate as a spec fn q(...) -> bool over integer indices and sequence values. Use requires to state list-shape conditions and ensures to state that a transition preserves the state predicate. Encode φ_shift, φ_pad, and φ_end as Boolean spec functions, then prove each generated clause as a Verus proof fn. Since I did not check what Verus offers, assume it has no CHC clause construct; the reduction would then become a collection of lemmas whose quantified postconditions simulate the clauses. Keep the acceptance contradiction as an assert(false) reached under a proof precondition, rather than attempting to execute proof code.

Evidence. Theorem 2 is the paper’s formal correctness evidence (Section 5.3, pp. 16–17). The body gives only a proof sketch; the detailed proof in Appendix A.2 (pp. 27–28) omits the “only if” direction, which the authors judge “not that difficult”, and relies on the completeness of SLD resolution. Lemma 1 (cons elimination) is proved in Appendix A.1 (pp. 25–27). The experiment’s 85/87 Ours-Eldarica result is the end-to-end evidence under the stated machine and 60-second timeout (Section 6, p. 18; Table 1, p. 19). The paper reports that SMT recursive-function translations solved only 38/87 (Z3) and 40/87 (CVC4), and assertion translations solved 30/87 and 28/87 respectively (Table 1, p. 19). These denominators include all three benchmark families: 15 IsaPlanner, 60 SAR SMT, and 12 CHC instances.

Failure and assumptions. The translation’s correctness theorem assumes a normal formula (Theorem 2).

technique 3: use SARs as ICE-learning teacher certificates

What it is. In ICE learning, a learner proposes interpretations for unknown CHC predicates and a teacher checks whether the candidate is a model. The paper maps list-valued predicate candidates to ΔÂč_sar formulas and checks the candidate by the SAR satisfiability procedure. In Example 4, a model maps P(X) to sorted(X) and Q(X) to hasZero(X) (Section 3.4, pp. 10–11). The paper argues that SARs “serve as certificates of the satisfiability of CHCs” (Remark 2, p. 11). Inference: this works because the candidate is a finite automaton representation that can be checked independently of how it was found.

When to use it. Use this arrangement when a verifier synthesizes invariants or predicate interpretations over recursive data. Inference: the learner may remain heuristic; the teacher must be sound. In the paper the learner does not exist yet: in Example 4 it is “yet to be implemented” (p. 11), and the conclusion says “We plan to implement an ICE-based CHC solver” (p. 21). The candidate language is limited to relations expressible by SARs, so a valid model outside that language will not be found.

How to do it.

  1. Convert each list CHC candidate predicate into a SAR formula. For predicates defined by recursion, build an ss-NFA for the relation and provide its negation when existential quantification requires it (Section 6, p. 18).
  2. Construct the CHC model-checking query by substituting candidate formulas for predicate variables.
  3. Normalize and reduce each resulting ΔÂč_sar query to integer CHCs using Technique 2.
  4. Ask the backend solver whether the resulting obligations are satisfiable/unsatisfiable. Reject a candidate when any CHC has a counterexample; accept it only when all obligations pass.
  5. Counterexamples would be fed back to the learner in the ICE protocol (Section 3.4, p. 10). The paper does not do this: the tool outputs no witness, and “The formalization and the implementation of this counterexample generation process are left for future work” (Section 5.3, p. 17). The SAR checker is described as the “teacher” part of ICE-based CHC solving (Section 3.4, p. 10; Section 6, p. 18).

Verus form. Inference: model the learner’s candidate as a ghost map from predicate identifiers to spec fn relations, or generate one fixed Verus spec relation per candidate. Prove a proof fn for every CHC clause showing that the candidate preconditions imply the candidate postcondition. Counterexamples can be represented as failing proof obligations or concrete test inputs; Verus itself does not provide the ICE learner, so candidate generation remains external.

Evidence. The CHC benchmark contains 12 instances (all valid), and Ours-Eldarica solved all 12, Ours-HoIce 11, and Ours-Spacer 8 (Table 1, p. 19). The benchmark also includes CHCs reduced from refinement-type checking (Section 6, p. 18). The paper’s claim that SARs “serve as certificates of the satisfiability of CHCs” is an argument (Remark 2, p. 11), not an experimental result. The CHC benchmark instances come with candidate models given as input (Section 6, p. 18); no learner is run.

Failure and assumptions. A certificate proves only the encoded CHC model under the arithmetic theory and automaton semantics. There is no learner, so nothing is established about candidate search.

what is proved, measured, and trusted

The paper states closure of ss-NFAs under Boolean operations (Proposition 1, attributed to [29]) and proves that Δ⁰_sar and ΔÂč_sar formulas are closed under Boolean operations (Proposition 3), proves undecidability of SAR satisfiability by reduction from two-counter machines (Theorem 1), and proves correctness of the translation for normal formulas (Theorem 2, with Lemma 1 for normalization). It gives no proof that the implementation is correct. It measures solved-instance counts and average time on 87 instances, with AMD Ryzen 9 5900X at 3.7 GHz, 32 GB memory, and a 60-second timeout (Section 6, p. 18). It does not measure proof-construction effort, solver memory, robustness under benchmark changes, or the cost of translating real Verus specifications.

Inference: the trusted base includes the automaton and formula parser, the reduction implementation, the CHC solvers Spacer/HoIce/Eldarica, and the arithmetic semantics. The paper’s checker reports only SAT, UNSAT, or TIMEOUT and “does not provide any witness of the satisfiability” (Section 6, p. 18). Inference: for agent-written verified Rust, the main product threat is specification mismatch and solver incompleteness around recursive state; SARs can reduce backend blind spots but do not validate that the modeled list relation is the intended API behavior.

techniques for the catalog

  • symbolic synchronous automata: encode recursive list relations as ss-NFAs whose transition labels are linear integer formulas
  • SAR-to-CHC reduction: normalize list terms and emit state, transition, initial, and acceptance CHCs over integers
  • ICE teacher certificates: use SAR formulas as finite candidate models and check every CHC obligation with the reduction

Last edited: