h t t p s : / / p e o p l e . c s a i l . m i t . e d u / a s o l a r / p a p e r s / a s p l o s 0 6 - f i n a l . p d f

Ingest: Combinatorial Sketching for Finite Programs

Type: types/ingest-report.md

Classification

This is a peer-reviewed conference paper (ASPLOS 2006) that presents a language, a formal semantics for it, a synthesis algorithm, and benchmark timings, so it is a scientific paper. Authors: Solar-Lezama, Tancau, Bodik, Saraswat, and Seshia (UC Berkeley and IBM T.J. Watson). The paper is the origin of the SKETCH system. Later surveys credit its synthesize-verify loop as the origin of counterexample-guided inductive synthesis (CEGIS). The authors built and evaluated their own system, and all timings are their own runs.

Summary

The programmer writes two things: an executable specification (a clear, slow reference implementation) and a sketch, which is a partial implementation whose hard fragments are replaced by holes (??). The synthesizer fills the holes with constants so the completed sketch is equivalent to the specification on every input. The paper contrasts this with its predecessor StreamBit, which derived implementations by domain-specific rewrite rules. Those rules were incomplete and so hard to write that only one author could write non-trivial sketches. SKETCH instead relies on a verifier to filter out incorrect completions, which lets it search every completion rather than only rule-derivable ones. For finite programs (bounded input, bounded operation count), synthesis is a 2QBF problem, ∃c ∀x P(x) = S(x, c). The solver alternates two SAT solvers. The synthesizer finds hole values c that match the specification on a finite set of inputs. The verifier checks c against all inputs. Each counterexample the verifier returns is added to the synthesizer's input set, and the loop repeats. When no hole values fit, the sketch is reported as buggy. When a loop-unrolling or hole-range bound is too small, an inserted assertion fails and the sketch is re-translated with a larger bound. Benchmarks (bit manipulation, CRC, Karatsuba, polynomial division) complete in seconds to minutes. An AES round needed 655 iterations and about an hour, and the generated code ran within 10% of OpenSSL. The completeness and correctness guarantees hold only for the finite instance checked: for Karatsuba, the paper verifies N = 12 and leaves correctness for other sizes to the programmer.

Quotes

No source quotes have been retained yet.

Connections Found

For the occasion, this paper is the anchor case for a propose-and-counterexample loop whose repairs cannot weaken the target. Four things stay fixed while candidates change. The specification is a separate program that the loop reads but never edits. The verifier checks each candidate against that specification on all inputs, not against the candidate's own account of itself. The sketch fixes the hole space, so a candidate can change only hole values. The counterexample set only grows, so a later candidate must also pass every earlier refutation. When no candidate fits, the loop reports "buggy sketch" instead of returning a weaker result. When a bound is too small, an assertion fails and the bound is raised; the specification is never loosened. Reading these four fixed elements as the requirement a review/revise loop lacks when it drifts toward empty claims is our transfer, not the paper's claim. The paper does not discuss drift, and in a KB review loop the claim often plays both roles, as the specification and as the candidate being revised.

For the general KB, the paper is pre-LLM, formal evidence for several oracle-theory notes. It is a clean mechanistic case for the boundary of automation is the boundary of verification: an exact, affordable equivalence check is what turns code writing inside the hole space into automation, and that note currently has no program-synthesis evidence. Its completeness guarantee is scoped to the domain where equivalence is decidable, as warranted autonomy is bounded by oracle domain predicts. Bound failures surface as assertion failures rather than silent acceptance. The division of labour matches improvements outside the admitted formal language need a pre-formal stage somewhere: the programmer chooses the admitted candidate space at design time, and the solver chooses among its members by counterexample. "Complete" means complete relative to that human-chosen space. The same point instantiates learning inside a fixed decomposition inherits its mistakes: when the sketch's structure is wrong, the best the synthesizer can produce is a proof that no completion exists, and restructuring stays with the programmer.

The counterexample set bears on oracle accumulation improves selection for later candidates in its maintained domain, with a channel qualification. Each retained counterexample is enforced on every later candidate, which is the note's "check" behaviour. But the counterexamples constrain the proposer (the synthesizing solver), while the verifier stays fixed and still checks every candidate on all inputs. The accumulated set therefore works as a cheap, exhaustively applied pre-filter inside one run, not as a maintained check across later tasks. The note's split between a proposal-side lesson and a selection-side check does not map cleanly onto this design.

FunSearch compares on the axis of a human-authored program skeleton that bounds machine search. SKETCH fills constant holes under an exact equivalence check against a reference specification. FunSearch evolves one function body with an LLM proposer under a graded score. Both keep the skeleton and the evaluator outside the search. The Gulwani, Polozov, and Singh survey is companion reading: it places this paper among constraint-based methods and credits it with sketching and CEGIS.

Learning Claims (our opinion)

On its own terms, SKETCH adapts within one synthesis run. Each failed candidate yields a counterexample input. That input becomes a new constraint on every later candidate, so the proposal side improves as refutations accumulate. The paper reports that the number of iterations tracks the number of control bits, not the size of the input space. Nothing is retained across runs: each sketch is solved from an empty counterexample set, apart from one random seed input.

Against the theory-builder conditions, three hold inside a run. Each candidate completion is a stated conjecture that "these hole values make the sketch equal the specification" (condition 1). It determines what the verifier checks (condition 2). A counterexample is a test of a stated consequence that refutes it, and the retained counterexample constrains every later candidate (condition 3). Condition 4 (iteration) is also met: each refutation is kept and shapes the next candidate, and a new candidate is a new conjecture tested again. One run is therefore a theory builder at a low persistence grade, across the rounds of one run, like a single refinement run; nothing persists to the next sketch. The case is best read as exact-oracle search with retained refutations. Its value for the KB is as a limiting contrast: this is what revision looks like when the criticism is guaranteed sound and the target cannot be moved.

Under learning inside a fixed decomposition, the effective update space is only the hole values. The specification, the sketch structure, the hole kinds and bit widths, and the unrolling and inlining semantics are fixed outside it. The loop can enlarge hole ranges and unroll factors, but it cannot rewrite the sketch. The evaluation shows that this configuration completes the tested sketches. The pop-count experiment varies how much hole information the user supplies, so it shows that user-fixed structure strongly affects solve time (Table 2: 1594 s with all holes open versus under 3 s with the loop bound and shift fixed and the two masks tied to one value). It does not compare alternative sketch structures for the same task.

Extractable Value

  1. Keep the specification outside the revise step's write scope -- the loop can refute a candidate but can never edit P. A failing search therefore ends in "buggy sketch", not in a weaker target. This is the concrete mechanism behind the occasion: in a review/revise loop, drift toward empty claims means the revise step is effectively editing the specification. The transferable requirement is a reference the reviser cannot rewrite, such as the claim's stated commitments or the occasion, against which revisions are checked. The paper supports the mechanism in the exact-oracle case. That a KB loop can hold an equivalent fixed reference is our conjecture. [experiment]
  2. Retain every refutation as a regression constraint on later revisions -- each counterexample is re-imposed on every later candidate, so a revision cannot fix one failure by reintroducing an earlier one. The KB analogue is to carry earlier review findings forward as checks the next revision must still pass. Our transfer; the paper's version works because counterexamples are exact inputs with checkable outputs. [experiment]
  3. "No valid completion" is a legitimate, reportable outcome -- the system distinguishes a buggy sketch (the hole space lacks an answer) from an insufficient bound (the space must be enlarged), and it signals both explicitly. A review loop that has no "cannot be repaired within this claim" exit will tend to repair by weakening. This bears directly on the occasion and on the learning-inside-a-fixed-decomposition note's point that the fix lies outside the update space. [quick-win]
  4. A program-synthesis evidence item for the verification-bounds-automation cluster -- the verifier-as-filter design, completeness scoped to the decidable domain, and assertion-signalled bound failures are evidence for the boundary of automation is the boundary of verification and warranted autonomy is bounded by oracle domain, from a pre-LLM, formal setting independent of their current evidence. [quick-win]
  5. The canonical "choosing among candidates by counterexample" example -- improvements outside the admitted formal language need a pre-formal stage somewhere uses automata learning and model grammars for this; SKETCH is the program-synthesis instance, with the sketch as the design-time pre-formal stage. [quick-win]
  6. User-supplied structure dominates solve cost -- in the pop-count experiment, partial information about shift amounts cut solve time by more than an order of magnitude, more than fixing the loop bound did. This is context-bound evidence about one small benchmark, useful as a data point that fixing more of the candidate space trades generality for search cost. [just-a-reference]

Limitations (our opinion)

The guarantee is exact only because the domain is finite and the specification is executable. KB claims have neither property: there is no complete reference implementation of what a note should say, and review verdicts are fallible. The paper therefore supports the design principle (keep the target outside the revise step, retain refutations) only in its exact-oracle limit. It does not show that the principle survives a soft oracle, where a "counterexample" can itself be wrong and retaining it can lock in an error. The simpler account of SKETCH's honesty is that its checker is a proof procedure. Much of what transfers may be the separation of roles rather than the retention mechanism.

The evaluation is narrow: small kernels plus one AES case study, all authored by the system's builders, run on one machine, with no comparison against StreamBit or another synthesizer on the same tasks. Iteration counts and timings are the authors' own runs. The "few SAT instances" claim holds on these benchmarks; the AES round needed 655 iterations. Karatsuba and CRC depend on finite restrictions or refactoring (N = 12; CRC's outer loop factored out), and correctness for other sizes is left to the programmer. The paper reports only successes, so it gives no data on how often sketches are buggy or how programmers repair them, which is the part of the loop most relevant to the occasion.

The pdftotext capture scrambles parts of the paper: Figure 2 (Karatsuba sketch) is interleaved with Section 4's text, the Figure 3 partial-evaluation rules lose their layout, Figure 4 (the counterexample-driven algorithm) is mostly unreadable glyphs, and Tables 1 and 2 are split into columns. This report relies on the prose description of the algorithm in Section 5.4 rather than Figure 4, and cites table values only where the column alignment is unambiguous.

Review learning inside a fixed decomposition inherits its mistakes or the KB note that will treat review/revise drift, and add one bounded paragraph citing this ingest: SKETCH keeps its repairs honest because the specification is outside the revise step's write scope, every counterexample is re-imposed on later candidates, and "no completion exists" is an explicit outcome rather than a trigger to weaken the target. State that this is the exact-oracle limiting case and that transfer to fallible natural-language review is the note's conjecture.

Relevant Notes: