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

Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML

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

result and problem

The paper builds a formally verified checker for propagation-redundancy (PR) unsatisfiability proofs. Its concrete artifact, cake_lpr, accepts a compact Linear PR (LPR) format, is implemented and verified in CakeML/HOL4, and is extracted to binary code through the verified CakeML compiler. A second format lets a large proof be split into independently checked ranges. The abstract states: “This article describes the first approach to formally verify PR proofs on a succinct representation.” (Abstract, p. 167)

Inference: The transferable lesson for VeruLaw is proof-carrying checking: make an untrusted producer emit a certificate, then verify a small checker whose executable path is itself tied to a proved semantics. This is a checker architecture, not a method for proving arbitrary Rust applications.

technique: enrich propagation redundancy into LPR

What it is and when to use it. A clause C is propagation redundant (PR) with respect to a formula F if some assignment omega satisfies C and F restricted to the smallest assignment alpha falsifying C implies F restricted to omega by unit propagation; intuitively, any satisfying assignment of F that does not already satisfy C can be modified, using omega, into one satisfying F and C (Definition 2 and following paragraph, p. 170). The paper says PR is efficiently checkable in polynomial time using the witness, and that checking RAT “requires a significant amount of proof search to find the unit clauses necessary” (Section 3, p. 171), which complicates verification and slows verified checkers; LRAT-style hints avoid that search. LPR adds those hints while retaining the PR witness. The paper explains: “The LPR format extends the PR format by adding, for each clause reduced by the witness, a list of all unit clause hints required for showing the implied-by-unit-propagation property.” (Section 3, p. 171)

How to do it. (1) Represent each proof addition as a clause and a witness assignment; deletions retain the LRAT syntax (Section 3). (2) For an added clause C, compute the smallest assignment alpha that falsifies C and choose a witness omega satisfying C (Definition 2, p. 170). (3) For each formula clause reduced by omega, find the unit clauses that prove the required implication by propagation (Section 3). (4) Emit the line in the Figure 1 grammar: the clause index, the clause, the witness (which starts at the second occurrence of the clause’s first literal), a 0, the unit-hint indices for the clause itself, then for each clause reduced by the witness a negative clause index followed by its hint indices, and a final 0 (Figure 1 and Section 3, p. 171). (5) Run the checker, which uses omega instead of LRAT’s first literal in its Step 4 and skips clauses satisfied by omega in Step 5.1 (Section 3, p. 171). (6) Accept only if every addition is PR-valid and the last addition is the empty clause (Section 2.2, p. 170).

The paper’s concrete example is a 4-pigeon/3-hole unsatisfiable formula. Figure 2 shows a 12-line PR proof in LPR; the same proof converted to RAT is 264 lines, and the authors say that to their knowledge no short RAT proofs are known for these problems that introduce no new variables and reuse no eliminated variables (footnote 2, p. 171; Figure 2, p. 172).

Verus form. Inference: Define clauses, assignments, propagation, and the accumulated formula as Rust mathematical datatypes in spec functions. Define a proof-checking function with requires that the input is well formed and ensures that Ok implies each addition preserves satisfiability and the final clause is empty. Use assert and proof functions for the propagation lemmas. The executable checker can use arrays and integer literals, but every conversion to the abstract set model needs a proved correspondence lemma.

Evidence and limits. The paper states that LPR is backwards compatible with LRAT (Abstract). On the SaDiCaL PR benchmarks, generating and checking LPR proofs took 1-2.5x the solving time (excluding mchess, where it was much faster than solving), whereas the PR-to-DRAT-to-LRAT route was 5-60x slower than solving (Section 6.1, p. 179, Tables 2-3, p. 180). A witness or hint is an input certificate; it does not prove that the SAT solver generated a semantically correct formula. Inference: a malformed parser, unsound assumption about clause indices, or incorrect proof-to-model lifting would invalidate the result unless covered by the checker contract.

technique: generate hints and shrink witnesses with DPR-trim

What it is and when to use it. Existing PR proofs often lack the hints required by LPR. The authors extend DPR-trim to enrich a PR proof and optionally shrink witnesses. They state: “Our extension to DPR-trim enriches input PR proofs by finding and adding all required unit clause hints to produce LPR proofs.” (Section 3, p. 171)

How to do it. (1) Run DPR-trim on a PR proof. (2) For each addition carrying a witness, perform the PR redundancy check; if no witness is supplied, retain the DRAT-trim RAT fallback (Section 3). (3) Find every clause reduced by the witness and append the complete unit-hint list. (4) Shrink the witness by removing every literal in omega ∩ alpha and any literal in omega that is implied by unit propagation from F|alpha; the paper says this shrinking was shown correct in earlier work but not previously implemented, and that SaDiCaL witnesses can be substantially compressed this way (Section 3, p. 171). (5) Output LPR (the -L option, footnote 1, p. 170). The paper says deletion steps are not validated by DPR-trim (Section 3, p. 171).

Verus form. Inference: Treat DPR-trim as an untrusted certificate compiler and verify only its LPR output. A Verus checker can accept a witness and hint arrays and prove that the hints establish propagation; it should not trust the hint generator’s control flow. If a shrinker is used, prove that the reduced witness preserves the PR predicate before emitting it.

Evidence and limits. The paper reports no independent percentage for successful hint generation. The PR-to-LPR conversion is an engineering preprocessing step; its correctness relies on the verified checker rejecting invalid output. Inference: this split allows fast, complex generation to remain outside the trusted core, but increases proof-file production cost.

technique: compositional proof checking

What it is and when to use it. A top-level proof is divided into ranges, and each range is justified by an underlying clausal proof. If ranges cover all instructions, transitivity of satisfiability implication yields a whole-proof result. The paper states: “The underlying proofs can be checked separately, in any order, and in parallel by running multiple instances of proof checkers on several machines.” (Section 4.1, p. 173)

How to do it. (1) Represent top-level additions as clauses without witnesses and retain deletion instructions (Section 4.1). (2) Choose indices 0 = i0 <= i1 <= ... <= ik = n covering every top-level instruction; the paper says tools may choose them arbitrarily as long as they cover all steps (Section 4.1, p. 173). (3) For each range (i,j), provide an underlying clausal proof showing that accumulated formula Fi implies Fj in satisfiability; the Figure 5 algorithm returns NO if i > j or j > n, runs the proof checker on the underlying proof and Fi, and returns NO if Fj is not a subset of the resulting formula (Figure 5, p. 173). (4) Run one checker instance per range, independently and in any order. (5) Concatenate successful outputs with input-file and proof-file hashes. (6) Invoke option 5 to check that the output file contains the correct hashes and that the ranges cover the entire compositional proof; coverage (e.g., that 0-2, 4-8, 2-4, 8-12 string together to 0-12) is checked by reusing a verified reachability function from the CakeML compiler (Section 5.1, pp. 175-176). (7) Conclude unsatisfiability when the final accumulated formula contains the empty clause (Section 4.1).

The checker emits s VERIFIED RANGE md5(DIMACS) md5(COMP) i-j for each successful range, and option 5 checks the concatenated records and coverage (Section 5.1, pp. 175–176). The paper warns that users must correctly set up separate executions; the paper calls option 5 “a simple layer of protection against user error” (Section 5.1, p. 175).

Verus form. Inference: Model a range certificate as a proof object with start and end indices, a hash or exact file identity, and a lemma that its underlying proof preserves the abstract formula. Prove a separate coverage predicate over sorted ranges; use a concurrency protocol or a sequential fold to combine range results. A cryptographic hash should be treated as an identity check unless its collision resistance is part of the specification.

Evidence and limits. The compositional theorem guarantees implication only when every range succeeds and coverage is established (Section 5.2). The paper explicitly retains a trusted foreign-function-interface model and target-machine assumptions (Section 5.2, p. 177). Inference: parallelism reduces wall time but introduces an orchestration boundary that needs its own checked coverage invariant.

technique: generate compositional proofs from cube-and-conquer

What it is and when to use it. Cube-and-conquer partitions a formula F into F ∧ Gi subproblems whose cubes cover all assignments. Each unsatisfiable subproblem supplies one underlying proof. The paper states: “Thus, if every subproblem F ∧ Gi is unsatisfiable, then F is unsatisfiable.” (Section 4.2, p. 174)

How to do it. (1) Use a cube-and-conquer solver to produce cubes G1 ... Gn whose disjunction is a tautology (Section 4.2). (2) Solve each F ∧ Gi under assumptions, preferably with an incremental solver. (3) Extract a smaller unsatisfiable core Hi ⊆ Gi when the solver supports it. (4) Convert each DRAT proof into an LRAT proof ending with ¬Hi using a modified DRAT-trim (Section 4.2, p. 174). (5) Add ¬Hi clauses to the top-level proof, then add the empty clause with a final underlying proof. (6) Check each range in parallel and check the final coverage file (Sections 4.1–4.2).

Verus form. Inference: This is analogous to partitioning a Rust verification obligation into disjoint cases, then proving each case and a coverage lemma. Verus can encode the partition and case proofs as ghost predicates; it cannot infer that a set of cases covers all inputs without an explicit lemma.

Evidence and limits. For the Erdős discrepancy benchmark, the top-level proof had 5,226 lines, while underlying proofs totaled 20 million clause-addition lines and ranged from 88 bytes to 110 MB, with the cube-and-conquer proof generated by iGlucose (Section 6.4, p. 181). These are proof-size denominators for one benchmark, not a general bound. The method assumes the cube disjunction is tautological and that all subproblem proofs and the final partition proof are checked.

technique: three-step refinement to verified binary code

What it is and when to use it. CakeML separates abstract mathematical correctness from concrete data structures and I/O. The paper says: “The development of cake_lpr proceeds in three refinement steps, where each step progressively produces a more concrete and performant implementation of the proof checker.” (Section 5.1, p. 175)

How to do it. (1) Formalize CNF, unsatisfiability, PR, and abstract proof validity over sets (Step 1, Section 5.1). (2) Implement the LPR checker over concrete lists and integer literals and prove it refines the abstract checker (Step 2). (3) Add arrays, exceptions, parsing, file I/O, and command-line behavior; prove the source implementation with the proof-producing translator and characteristic-formula framework (Step 3). (4) Compile with the verified CakeML compiler, composing the source correctness theorem with compiler correctness to obtain a binary theorem (Section 5.1). (5) Expose five command-line modes: parse DIMACS, check LPR, check a DIMACS transformation, check a compositional range, and check combined range outputs (Section 5.1).

Verus form. Inference: Use a pure spec fn model for formulas and a separate executable Rust representation, then prove representation invariants and refinement lemmas. Keep parsing and file I/O behind explicit contracts. Verus can prove the Rust implementation against the model, but the external Rust compiler, runtime, and target platform remain trusted unless a separate verified compiler is used.

Evidence and limits. The end-to-end theorem says that if the binary prints s VERIFIED UNSAT\n, then the parsed formula is unsatisfiable for the two-argument mode (DIMACS file and LPR proof) (Section 5.2, p. 176; Figure 10, p. 177). The theorem assumes well-formed command-line and file-system models and a machine-state placement of compiled code (Section 5.2, p. 176). It permits an out-of-memory termination in the CakeML runtime (Section 5.2, p. 176), so “never crashes” is conditional on resource availability. The trusted computing base still includes the CakeML FFI model and target-hardware semantics; the compiler itself is excluded (Section 5.2, p. 177).

technique: verify performance optimizations behind abstract invariants

What it is and when to use it. The implementation uses imperative structures only in hot paths while preserving the abstract checker theorem. The main optimizations are byte-array bitsets for assignments, arrays for clauses, lazy deletion indices, lookup arrays for first clause occurrences, exceptions for failure, verified hash tables for compositional inclusion, buffered I/O, and a verified MD5 implementation (Section 5.3).

How to do it. The paper describes these optimizations and says they are verified; it does not list each proof obligation, so the clauses below that say to prove a property are Inference. (1) Replace set-based assignments with a byte-array bitset and prove each lookup agrees with the abstract assignment (Section 5.3.1). (2) Store clauses in an array with a lazily updated list of undeleted indices, plus a lazily tracked lookup array of each literal’s smallest clause index (Section 5.3.1); prove that iteration visits exactly the undeleted clauses (Section 5.3.1). (3) Represent failures with exceptions and prove that every successful path has the same result as the option-based specification (Section 5.3.2). (4) Hash clauses with a verified rolling-hash table and prove inclusion checks against the abstract formula (Section 5.3.3). (5) Batch file reads with verified buffered I/O (Section 5.3.4). (6) Prove that imperative MD5 matches its functional specification; do not treat this as a cryptographic proof, because “we do not prove any formal cryptographic properties of the hashing function.” (Section 5.3.5, p. 178)

Verus form. Inference: Each optimized Rust structure should carry a representation invariant and a lemma relating it to a ghost mathematical set or sequence. assert can discharge local correspondence facts; proof functions can establish array bounds and permutation-preservation. Treat hash collisions as a correctness concern unless the hash is only used for indexing followed by exact equality checks.

Evidence and limits. The paper says proof files in the second benchmark suite range from 300 MB to 4 GB and are streamed line by line (Section 5.3.4, p. 178). The MD5 result is functional equivalence only, not collision resistance. Inference: performance engineering can remain outside the conceptual specification only when every optimization is proved to preserve it.

benchmark evidence and numerical limits

All experiments used identical Intel Xeon E5-2695 v3 nodes at 2.30 GHz with 128 GB RAM (Section 6, p. 179). On 102 SAT Race 2019 unsatisfiable proofs generated by CaDiCaL, Table 4 reports cake_lpr success on 97, timeout on 0, other failures on 0, and N/A on 5; the denominator is 102 proofs, and N/A reflects an earlier toolchain failure or timeout rather than cake_lpr’s checker result (Table 4, p. 180). The paper says cake_lpr is on average 1.2× slower than acl2-lrat in LRAT checking, although cake_lpr is faster on 28 benchmarks (Section 6.2, p. 179). The same section reports the full generation-plus-checking GRAT toolchain as 3.5× slower for cake_lpr and 3.4× slower for acl2-lrat, and the paper attributes part of the GRAT toolchain’s speed to GRATgen running in parallel with 8 threads (Section 6.2, p. 179).

For the mutilated-chessboard RAT suite, Table 5 covers five sizes from 20×20 through 100×100. Cake_lpr takes 0.5, 3.5, 10.6, 22.6, and 44.2 seconds respectively, with 125,752 through 9,506,092 proof steps and 5 through 499 MB files (Table 5, p. 181). The authors report that cake_lpr “scales essentially linearly in the size of the proofs (up to ≈ 10 million proof steps)” and “comes within a 5x factor of the unverified lrat-check tool” (Section 6.3, p. 180). For the EDP compositional run, wall time falls from 3,871.7 seconds at one thread to 60.2 seconds at 128 threads, a reported 64.3× speedup relative to one thread; speedup is nearly linear for 1-32 threads but drops off at 64 and 128, which the paper says is “likely due to the unbalanced nature of proof sizes” (Table 6 and Section 6.4, p. 181).

what is proved, trusted, and threatening to VL

The proved claims include PR soundness, refinement from concrete LPR checking to the abstract proof system, parser/printer inversion for well-formed formulas, command-line behavior, compositional range coverage, and compilation preservation down to machine code (Sections 5.1–5.2). The trusted base still includes the FFI model and target hardware semantics; assumptions about input files and resources remain explicit (Section 5.2). The checker proves that a certificate implies unsatisfiability, not that a SAT solver’s encoding expresses the intended mathematical problem.

Inference: This poses a medium-to-high threat to agent-written verified Rust at certificate boundaries. An agent may produce a sound proof checker while encoding the wrong formula, omit a range, or assert a false environment contract. The paper’s range hashes and coverage proof suggest a concrete mitigation: make proof-input identity, partition coverage, and parser round trips explicit verified obligations. Inference: VL should not redo a generic SAT proof-checker survey or the LPR/CakeML implementation; it should reuse the separation between abstract specification, concrete optimized checker, certificate generation, and end-to-end executable validation.

techniques for the catalog

  • LPR witness-and-hint format — enrich propagation-redundancy clauses with unit-propagation hints for fast checking
  • certificate preprocessing — use DPR-trim to add hints and shrink witnesses before verified checking
  • compositional proof ranges — split a proof into independently checked ranges and verify complete coverage
  • cube-and-conquer certificates — derive parallel subproofs from a tautological cube partition and unsatisfiable cores
  • refinement to verified binary — prove abstract, concrete, I/O, and compiled implementations in successive refinement steps
  • invariant-preserving optimization — verify arrays, exceptions, hash tables, buffered I/O, and hashing against functional specifications Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The MD5 hash is chosen for convenience because it is available on most machines, so users can, e.g., manually compare md5 hashes of their input DIMACS and proof files to check that the correct files were used on all machines.”): I read the whole paper text and looked at the page images of Figures 1-6; I checked every quotation, section/page reference, algorithm step and benchmark number against it; I changed the PR definition wording, the LPR line-format step (Figure 1 grammar), the footnote-2 and Figure 2 reference, the DPR-trim witness-shrinking and deletion statements, the Figure 5 and option 5 descriptions, theorem page references, the Table 5 page, the EDP speedup wording and the GRAT ratio sentence, and I added the Section 6.1 LPR versus LRAT-route timings and marked unlisted proof obligations as Inference; I did not check the cited related work, the HOL4 theorem statements in Figures 10-11 beyond the prose (they are images), or the raw timing data in the cake_lpr repository.

Last edited: