Prove specs over every input: state graphs, symbolic evaluation, a certifying solver - #8
Merged
Merged
Conversation
added 9 commits
September 23, 2026 14:04
writ.solve.pre brings a formula over integers to clauses of integer inequalities and booleans: mod, quot, abs, max, min and ite name fresh variables with their defining cases, uninterpreted fns and predicates are Ackermann-expanded, and the rest goes through Tseitin. writ.solve.cert rebuilds those clauses and checks a proof tree over them: splits, clauses false on a branch, Chvatal-Gomory cuts and Farkas sums. It searches for nothing.
A from-scratch Dutertre-de Moura simplex over ratios explains an infeasible bound set as a Farkas sum. DPLL with unit propagation calls it at each node, closes integrality with Gomory cuts and then branch-and-bound, and records the search tree as the proof, dropping any split whose subtree never used its literal.
The API over the search and the checker, with tests: known sat and unsat cases, mod and quot against clojure.core, integer-only infeasibility, min monotonicity, EUF, a Game of Life shift, budgets, tampered certificates, and random formulas against brute force.
# Conflicts: # test/writ/test_runner.clj
A search node now starts the simplex from its parent's tableau and only repairs the bounds it adds, and unit propagation looks only at the clauses holding the negation of a literal just made true. The slowest query from the pong spec went from 38s to 2.5s. Certificates are unchanged, so the checker is too.
…space Every spec now declares its state graph. An edge into refinements is an obligation that the step lands in the states it names and never throws; a spec with no graph fails the check. The prover runs non-recursive code on symbolic values, Rosette style: branches merge, data values whose constructor depends on a branch are unions, sets of unknown size are predicates and equal by extensionality. The formula goes to writ.solve, and the checker verifies its certificate. Data variables are split by constructor first, bounded integers are enumerated, and open linear goals go to the solver too. A counter-model from the solver becomes a counterexample, run on the code before it is reported, so bugs no test samples are still found. A proof namespace (proof-of, lemma, hint) holds what the prover needs and the spec should not say; lemmas must be proved and never count as laws. Proof results are cached against the exact sources they came from. Also fixed: a graph state of a compound type crashed the check, an `and` hypothesis was not taken apart, and integer refinements were sampled uniformly, missing the edges of their range.
pong, life and fetch now prove every universal law and every graph edge. life's the-plane-has-no-favoured-place holds for every world, not packed 6x6 samples. pong's tunnel bug is found by the solver where no test finds it. life.fast counts with frequencies, outside the prover, so it is checked with :require :tested.
A won pong game needs its tag and an exact score together, and 200 tries sometimes found none, failing a law at random. Generation now tries 5000 times, and says which refinement starved if it still can't.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Writ used to test most laws and prove few: the life, pong and fetch specs proved none. This makes proof the default path.
refine); an edge into refinements is an obligation that the step lands in the named states and never throws. The graph's own rules (:never,:before,:final, reachability) then hold for every run of the code.(spec ns {:require :proved})fails on anything unproved, and letting a law off needs a stated reason.writ.solve: a pure Clojure solver for linear integer arithmetic and uninterpreted functions, with certificates checked by a small independent checker. The search is never trusted.proof-of,lemma,hint) holds what the prover needs without changing the spec. Lemmas must be proved and never count as laws.In the examples, pong, life and fetch now prove every universal law and graph edge. life's
the-plane-has-no-favoured-placeholds for every world. pong's tunnel bug is found by the solver when no test finds it.Fixed along the way: adequacy sampled all variables of one type with the same seed, so laws relating two of them couldn't reject stand-ins; a graph state of a compound type crashed the check;
andhypotheses weren't taken apart.Not done: the ACL2-style induction heuristics (R4) beyond testing generalised goals, and the BST
holds-a-sorted-setproof (writ-tpr), which still needs a model ofsortanddistinct.life.fastusesfrequencies, which the prover can't handle, so it is only tested.The examples suite is slow on a cold cache: pong alone takes several minutes to prove.