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

An Update on Deductive Synthesis and Repair in the Leon Tool

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

problem and result

Leon synthesizes or repairs recursive, purely functional Scala programs (a subset of Scala with mutually recursive functions). The specification is given as function pre- and postconditions plus possibly symbolic input-output examples (Section 1, p. 100). The paper reports progress in scaling this: new techniques, including “a more precise mechanism for encoding the space of meaningful candidate programs” (Abstract, p. 100). The abstract reports: “Our techniques increase the scope of synthesis by expanding the space of programs we can synthesize and by reducing the synthesis time in many cases” (Abstract, p. 100).

A synthesis problem is written as inputs ā, path condition Π, specification φ, and output variables x̄. A solution is a pair of a precondition P and a program term T (Section 1.2, p. 102). The framework applies deductive rules that either decompose a problem into simpler ones or close it directly; the most notable closing rule is Symbolic Term Exploration (STE) (Section 1, p. 100). STE validates candidates with a Leon solver, which reduces verification to SMT queries for Z3 and CVC4 (Section 4, p. 104).

technique 1: dedicated recursive-call rule

What it is. The new Introduce Rec. Calls rule is a deductive rule that adds a recursive call to the synthesis context. It forces one argument of the function to be smaller; the other arguments are fixed. The result is bound to the variable rec, which later decomposition rules can use. The paper says the rule “replaces all rules which introduced induction in any way” (Section 2, p. 102). The previous approach instead introduced recursive calls inside STE, with the remaining arguments left free to be generated by STE (Section 2, p. 102).

How to apply it.

  1. Track the function under synthesis with a context ⇓[foo(a1,...,an)] alongside the path condition Π (Section 2, p. 102).
  2. Choose an argument ai and enumerate argsSmaller(ai, Π): for an Int or BigInt, i - 1 if i > 0 and i + 1 if i < 0; for an abstract-class value c known to be a concrete subclass CC, the fields c.f of abstract-class type, together with argsSmaller(c.f, Π); the empty set otherwise (Section 2, p. 102).
  3. Add rec ← foo(a1,...,a'i,...,an) to the path condition, with a'i in argsSmaller(ai, Π) (formal rule, Section 2, p. 102).
  4. Solve the resulting subproblem; the solution of the subproblem is the solution of the original one (formal rule, p. 102). Because rec is in the path condition, further decomposition rules can use it (Section 2, p. 103).

The paper explicitly limits the rule: “This approach cannot generate recursive calls where more than one argument changes” (Section 2, p. 103); it gives as an example a function that updates an accumulator while traversing a data structure. The benefit is that rec is available to further decomposition rules, which “allows for new forms of programs to be synthesized”. In the run-length encoder (Figure 1, 6th line of the solution), rec is pattern-matched by another rule, “which is necessary to solve the particular benchmark” (Section 2, p. 103).

Verus form. Inference: a Verus proof-guided generator could restrict recursive Rust function candidates to calls on structurally smaller data and require a decreases measure where the Verus construct is available. The generated function would still need requires/ensures and loop invariant(...) proofs. The Leon rule itself is a synthesis search rule, not a Verus annotation, and Verus does not automatically synthesize the recursive call from this paper’s context notation.

Evidence and failure. The new recursive rule solved four additional synthesis benchmarks in the paper’s ablation (Section 5, p. 107): List.split, AddressBook.make, RunLength.encode and Diffs.diffs go from X in the STE column to solved in the Rec column of Table 1 (p. 107). The paper says it “does not improve running times” (Section 5, p. 107). It cannot express accumulator-style recursion with multiple changing arguments (Section 2, p. 103). In repair, one benchmark (List.drop) is no longer solvable “due to the change in handling of recursive functions” (Section 5, p. 107).

technique 2: attributed term grammars

What it is. STE generates expressions from a type-directed context-free grammar that depends on the synthesis problem, e.g. variables in scope and calls to available functions (Section 1, p. 100; Section 3, p. 103). The previous implementation used only types as nonterminals, which was highly ambiguous and generated many semantically equivalent terms. Leon now enriches nonterminals with attributes that “refine and filter production rules of an existing grammar” (Section 3, p. 103). The paper contrasts this with the disambiguation of [18], which happens after the terms have been generated: “our attributes affect the grammar itself, meaning that all terms produced are automatically good candidates” (Section 3, p. 103).

How to apply it.

  1. Build a grammar from variables and callable functions in scope, e.g. Int ::= Int + Int | Int - Int | 0 | a | foo(Bool) (Section 3, p. 103).
  2. Attach Sized attributes and assign each operator f a cost size(f). For T{|s|} ::= f(T1{|s1|}, ..., Tn{|sn|}), keep all combinations of si > 0 with ∑ si = s - size(f); a nullary production is kept only if size(f) = s. For a commutative operator additionally require si ≄ sj for all i < j, so only left-heavy terms are produced (Section 3, pp. 103–104).
  3. Make associative operators associate to the left: T ::= f(T1, T2) becomes T ::= f(T1, T2{ÂŹf}), and rules T{ÂŹf} ::= f(T1, T2) are removed (Section 3, p. 104).
  4. Use G and ÂŹG to separate ground-term generation from other terms: constants are removed from ÂŹG productions and variables from G productions, and ÂŹG is attached to the top-level symbol. The reasons are that ground terms such as 1 + 3 and 2 + 2 simplify to equivalent programs, and another dedicated rule finds ground terms much more efficiently than STE (Section 3, p. 104).
  5. Exclude neutral or absorbing operands with the attribute ÂŹ0: Int ::= Int + Int becomes Int ::= Int{ÂŹ0} + Int{ÂŹ0}, and Int ::= 0 is excluded from Int{ÂŹ0}. This removes terms such as e + 0, e / 1, and e * 0 (Section 3, p. 104).

Verus form. Inference: the same normalization idea can constrain an agent’s candidate Rust/Verus proof terms before invoking Verus: canonicalize commutative expressions, avoid neutral arithmetic, and bound expression size. These are generator-side transformations; they do not change Verus’s valid constructs or prove equivalence. Any generated candidate still needs Verus assert, lemmas, and contracts checked by the verifier.

Limits. The paper notes that generating bigger terms by increasing the unfolding depth of the grammar “causes the number of terms per depth to explode double exponentially”, which is why it uses Sized instead (Section 3, p. 103). It reports that the improved term grammars have “a significant, if smaller, effect on running times” and expects the improvement to grow with expression size “due to the exponential nature of the problem” (Section 5, p. 107). Inference: attribute rules remove redundancy but do not by themselves make the search complete or polynomial; the paper does not claim either.

technique 3: symbolic term exploration with counterexample-guided testing

STE unfolds the grammar of Section 3 into a set of candidate programs represented together as a symbolic program tree. The programs are first filtered by concrete execution on a set of tests; survivors are handled symbolically with a Leon solver (Section 4, p. 104). Algorithm 1 (p. 105) gives the procedure:

  1. For each size n from 1 through maxSize, unfold grammar G to the programs P of size n (Algorithm 1, p. 105).
  2. Run concrete tests on the initial examples I, removing programs that fail (Algorithm 1, p. 105).
  3. If |P| is sufficiently reduced (the text: “if the number of remaining programs is relatively small”), try to prove or disprove each program separately with the Leon solver; if one is proved correct, return it (Section 4, pp. 104–105; Algorithm 1).
  4. Otherwise, or if none is validated, query the solver for a program in P that satisfies the specification for at least one fresh input. If there is none, STE fails for this size and moves to the next n; if there is one, try to prove it valid as in step 3 (Section 4, p. 105; Algorithm 1).
  5. When validation finds a counterexample, remove that program, add the counterexample to the test base I, and concretely test the remaining programs against it (Algorithm 1, VALIDATE, p. 105). The text says programs are tested “against every counterexample as soon as it is discovered” (Section 4, p. 105).
  6. Sort the available tests by the number of programs that failed on them, so tests that excluded more programs run first. Also build a partial solution from parts already found by other deductive rules, with a placeholder ??? for the current problem; the placeholder is set to the tested program during concrete execution and validation, and to the tree of available programs when searching for a tentative program (Section 4, pp. 105–106).

The paper states: “Our experience using STE since the previous iterations of the tool has shown that, even for thousands of programs and tens of tests, concrete execution is usually faster than a single SMT query” (Section 4, p. 105). Its explanation is that many tests come from automatic data generators and tend to be small. This is an engineering observation, not a theorem. Inference: for Verus-oriented synthesis, the same counterexample pool could cheaply reject candidate Rust contracts before expensive verification, but the final ensures proof remains necessary.

technique 4: deductive synthesis and repair specifications

The run-length encoder illustrates specification-driven synthesis. The input gives decode, a legal predicate characterizing legal run-length encodings, and a nondeterministic choose requiring legal(res) && decode(res) == l (Figure 1, p. 101); the abstract describes this as “the decoding function and the local minimality property of the encoded value”. Leon converts it into a deterministic encode with an ensuring postcondition. The paper reports that it generates and formally verifies this solution “in about 20 seconds” (Section 1.1, p. 101); Table 1 lists RunLength.encode at 18.7 s (Rec) and 20.3 s (TG) (p. 107).

For repair, the paper uses “a set of benchmarks for program repair identical to the one presented in [12]” and reports Test and Repair times for the previous and current versions in Table 2 (Section 5, p. 107; Table 2, p. 108). It gives no further description of the repair procedure or benchmark contents in this paper.

Verus form. Inference: a Verus-facing system could translate a specification into candidate Rust implementations and use ensures as the acceptance condition. A choose-style nondeterministic specification is a synthesis input, not executable Verus code; the final implementation must be deterministic Rust whose proof passes. Inference: agent-generated candidates must preserve the specification’s quantifier and abstraction meaning, because passing a weakened contract would not establish the intended behavior.

evidence, measurements, and trust

Table 1 lists 24 synthesis benchmarks for the previous version and four configurations (Size = 7, STE, Rec, TG), with a 200-second timeout (Section 5, p. 106; Table 1, p. 107). Quoting the Observations: “The new version of the tool was able to solve five new hard benchmarks which were out of scope for the previous versions” (Section 5, p. 106); it also “produces a much more concise, and thus verifiable, solution for an additional benchmark (StrictSortedList.delete)”. “Some of the easier benchmarks do present some slowdown”, mostly from failing STE instances that exhaust a larger search space (Section 5, pp. 106–107). The ablation: raising the STE size bound from 5 to 7 “immediately solves one additional benchmark” but is not viable alone because of large slowdowns; the STE improvements “greatly improve the performance of the tool 
 without solving additional benchmarks”; improved grammars have a smaller effect on running times; the recursive-call rule solves four additional benchmarks (Section 5, pp. 106–107). Table 2 contains 34 repair rows with times in seconds for the previous and current versions, split into Test and Repair. The paper says the current version generally shows “some delay relatively to the previous version”, mostly from reliability changes (“more robust nondeterministic evaluator, support for multiple synthesis solutions etc.”), and that List.drop is no longer solvable (Section 5, p. 107; Table 2, p. 108). It calls the repair results “not so interesting” (Section 5, p. 107).

The paper’s denominators are benchmark rows, not random samples: the five-new-benchmark claim refers to the synthesis table, while the four-benchmark claim refers to the recursive-rule ablation. A cross mark means synthesis failed: the benchmark timed out after 200 seconds or the synthesizer exhausted its search space; a parenthesized check mark means a solution was produced but could not be verified (Section 5, p. 106). The paper does not discuss its trusted base. Inference: the trusted components are the Leon-to-SMT translation, Z3/CVC4, the concrete evaluator, and the user specification, so synthesis success is only as meaningful as the specification and the completeness of the candidate grammar.

Inference: the threat to agent-written verified Rust is high for candidate-generation workflows and low for direct Verus proof checking. Leon demonstrates that recursion-aware search, grammar normalization, and counterexample-guided testing can produce verified code automatically, but it targets a purely functional subset of Scala and the paper does not address Rust ownership, unsafe operations, concurrency, or Verus’s proof language. The useful product lesson is to separate cheap candidate filtering from expensive proof validation and to make search restrictions explicit.

techniques for the catalog

  • recursive-call introduction — generate one structurally smaller recursive argument and expose its result to later synthesis rules
  • attributed term grammars — canonicalize size, associativity, commutativity, groundness, and neutral-element choices before generation
  • symbolic term exploration — enumerate candidates by size, test concretely, and validate symbolically with SMT
  • counterexample-guided test growth — add solver counterexamples to a prioritized concrete test base
  • specification-driven repair — synthesize or repair code only when the resulting candidate satisfies formal contracts

Last edited: