Foundational Constraint Solving for Expressive Refinement Typing

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

paper and result

Khan, Markopoulos, Lehmann, and Jhala present Flex, a Lean implementation of foundational solving for constrained Horn clauses (CHCs) generated by refinement type systems. The paper’s central claim is that solver reductions can emit Lean proof terms checked by the kernel, while Lean’s logic permits specifications beyond an SMT solver’s fixed decidable theories. The abstract says: “We present Flex, a foundational Constrained Horn Clause (CHC) solver implemented in Lean, that reduces the trusted base to the kernel alone, and allows using Lean’s entire proof ecosystem to verify low-level systems code, via three contributions.” (§1, p.1)

The paper’s architecture separates a constraint generator from a solver, then certifies both the reductions and the generated verifier. It reports two generators (an imperative Floyd–Hoare verifier and a refinement-typed lambda calculus verifier) and a Flux backend. The authors state: “The solver in §4 removes the backend from the trusted base by generating a kernel checkable proof of the constraint’s validity.” (§5, p.18) The exact trust claim is narrower than trusting an entire Rust toolchain: the kernel checks Flex’s proof terms, while compiler plugins, specifications, and trusted wrappers remain outside that kernel theorem.

technique: represent verification as foundational CHCs

what it is

A CHC is a proposition containing universally quantified variables, implications, conjunctions, and existential Horn predicates (Horn variables). A Horn variable κ : b1 → … → bn → Prop stands for an unknown predicate to synthesize. The paper defines satisfiability by assigning each κ a Lean predicate and replacing applications with that predicate (§3.1, pp.9–10). Terms and predicates are Lean terms, so the refinement language can use any theory expressible in Lean. The authors write: “As terms and predicates are Lean terms, they can use any theory expressible in Lean.” (§3.1, p.10)

when to use it

Use this encoding when a verifier needs unknown loop invariants or unknown refinements and the desired specification may require quantifiers, recursion, bit-vectors, or other Lean-expressible predicates. The encoding keeps program-generation and constraint-solving separate, so one solver can serve multiple frontends.

how to do it

1. Define the base sorts and first-order terms used by the program (the paper’s core examples use Int and Bool) (§3.1, Fig. 8, p.9)
2. Introduce a Horn variable for each unknown invariant or refinement, with arguments containing every value needed at its use sites (§3.2, pp.10–11)
3. Build constraints from implications, conjunctions, and universal quantification; make each unknown predicate existentially quantified (§3.1, p.10)
4. Solve the closed constraint and retain the generated proof that the solved constraint implies the original (§4, pp.12–17)

Verus form (inference)

Inference: In Verus, the analogous shape is to state an explicit requires/ensures contract and introduce a ghost predicate or spec fn for an invariant, then prove the resulting obligations with assert, assert forall, and proof lemmas. Verus does not expose Flex’s existential CHC variables as a general refinement-inference interface; invariant discovery remains manual or solver-assisted through Verus’s supported constructs. The mapping is therefore a design analogy, not a feature claim about Verus.

evidence, assumptions, limits

Flex’s guarantee is conditional on a sound Lean oracle and a well-formed generated constraint. The paper states: “Theorem 4.3 (Fix-Soundness). If Oracle is sound and Fix(c, Q) = (c′, q), then ⊢ q : c′ → c.” (§4.4, p.17) The method assumes each Horn variable’s arguments are passed consistently; the paper calls this well-formedness requirement explicit (§3.2, p.11). A CHC encoding does not prove that the encoded property is the actual product requirement.

technique: Zap for acyclic Horn variables

what it is

Zap eliminates Horn variables that do not participate in dependency cycles. It computes the strongest solution from all goals, substitutes that solution into body occurrences, replaces head occurrences with ⊤, and constructs a proof term certifying the rewrite. The paper summarizes: “Zap eliminates acyclic horn variables (left) using Elim to compute solutions (right).” (§4.2, Fig. 10, p.13)

when to use it

Apply Zap before cyclic-variable solving whenever the dependency graph has acyclic variables. It gives deterministic elimination and avoids invoking a search tactic for the certificate.

how to do it

1. Compute dependencies between Horn variables and partition them into cyclic and acyclic sets (§4.1, pp.12–13)
2. For an acyclic variable κ, enumerate its goals and compute Sol(κ,c), the disjunction of the bodies of those goals (§4.2, pp.13–14)
3. Reduce every body occurrence of κ with the solution and every head occurrence to ⊤ (§4.2, Fig. 10, p.13)
4. Traverse the original constraint with Certκσ,ρ; at divergent heads use Nav to align contexts and emit a Lean proof term (§4.3, pp.14–15)
5. Repeat until no acyclic variable remains (§4.2, p.13)

The strongest-solution construction is exact for the acyclic case. The authors state: “Theorem 4.1 (Zap-Equivalence). [14] If (c′, ·) = Zap(c) then c is satisfiable iff c′ is satisfiable.” (§4.3, p.15) They also state kernel-facing soundness: “Theorem 4.2 (Zap-Soundness). If (c′, q) = Zap(c) then ⊢ q : c′ → c.” (§4.3, p.15)

Verus form (inference)

Inference: A Verus analogue is a proof lemma that derives a reusable invariant consequence once, followed by assert uses of that consequence in the caller. Verus has no Zap command or existential predicate elimination; the engineer supplies the predicate and proof term directly. The transferable idea is to separate acyclic facts from cyclic loop invariants and discharge the former deterministically.

evidence and limits

On 369 constraints, Zap reduced all constraints; its maximum reported running time was 62 ms. Search alternatives were weaker: “Zap_grind reduces only 247 of the 369 constraints (67%), and on the constraints it can reduce, it consumes 18× more heartbeats and it is 13× slower on average.” (§6.2, p.24) Zap_aesop reduced 90% and was 22 times slower on average (§6.2, p.24). These measurements use the five suites listed in Table 2 and compare default Lean tactics on the same workstation; they do not establish universal speedups.

technique: Fix predicate abstraction for cyclic variables

what it is

Fix handles cyclic Horn variables using predicate abstraction. A qualifier is a predicate template; all sort-correct parameter instances become candidates. Fixpoint repeatedly removes candidates that an oracle cannot prove valid at a head goal. The paper states: “Fix is parameterized by the procedure Oracle, which attempts to prove a goal, which lets the user plug in theory-specific oracles to synthesize solutions for CHCs over arbitrary Lean propositions.” (§4.4, p.17)

when to use it

Use Fix when unknown predicates depend on themselves, as loop invariants do. Supply qualifiers that express likely relations and an oracle able to prove candidate implications in the chosen Lean theory.

how to do it

1. Choose a qualifier library Q of predicate templates (§4.4, p.16)
2. Instantiate every qualifier against every Horn variable with sort-compatible argument mappings; initialize each variable to the full candidate set (§4.4, pp.16–17)
3. At each head prefix, call the oracle and retain only candidates whose instantiated predicates are provable under the current assignment (§4.4, p.17)
4. Repeat weakening until no candidate can be removed; termination follows because the finite candidate set strictly decreases (§4.4, p.17)
5. Replace head applications by ⊤, body applications by the computed conjunction, and use Certθ to construct a proof of the original constraint (§4.4, p.17)

The paper’s running example uses κex : Int → Int → Prop and qualifier q≤ = λz0:Int,z1:Int. z0 ≤ z1; all four sort-compatible mappings are candidates (§4.4, p.16). This is the concrete recipe for generating relational invariant candidates rather than guessing one predicate manually.

Verus form (inference)

Inference: In Verus, encode each selected candidate as a spec fn or a lemma proposition, then prove the loop’s invariant(...) clauses and preservation assertions. The candidate-pruning loop itself would run outside Verus as a synthesis tool; only the final invariant and its proof are Verus source. Do not write invariant(...) as a function call, and do not attach ensures to a spec fn.

evidence and limits

The strongest result is relative completeness: “Fix returns the strongest valid solution expressible as conjunctions of predicates from Q.” (§4.4, p.17) This is relative to qualifier coverage and oracle completeness, not completeness for arbitrary invariants. In the full benchmark, cyclic constraints had 82.3% success (135/164); 37 total failures included 21 recursion-depth, 4 heartbeat, 4 missing-qualifier, and 8 concrete-goal failures (Table 4, p.25). The denominator and cyclic subset are essential: 135 successes out of 164 cyclic constraints, not 82.3% of all 880.

technique: generate verified conditions for imperative programs

what it is

The Imp frontend shallowly embeds commands and uses textbook weakest-precondition generation. For every while, it introduces a Horn predicate as the unknown invariant and generates initial, body, and exit obligations. The paper gives the generated shape: “when the generator hits a while it introduces a Horn variable κ for the unknown invariant — a |V |-ary predicate — and constrains it to satisfy the usual initial, body and exit obligations.” (§5.1, p.18)

how to do it

1. Represent a program state as a map from variables to integers and assertions as predicates on states (§5.1, p.18)
2. For while g do c, create κ over the ordered program variables (§5.1, p.18)
3. Emit P → κ for entry, verify the body from κ ∧ g back to κ, and emit κ → ¬g → Q for exit (§5.1, p.18)
4. Solve the resulting CHC with Zap/Fix and use the proved implication to establish the Floyd–Hoare triple (§5.1, p.18)

The paper proves: “If VC(P, c, Q) then |= {P } c {Q }.” (Theorem 5.1, §5.1, p.18) The theorem is for the shallow Imp semantics, so language-specific Rust behavior is outside this theorem.

Verus form (inference)

Inference: In Verus, write executable Rust, state requires and ensures, and place the loop predicate in invariant(...); prove preservation with assert or proof lemmas. Verus’s loop invariant is explicit, while Flex’s κ is synthesized from CHCs. The same entry/body/exit obligations are the conceptual proof obligations.

technique: refinement inference with a foundational type checker

what it is

The λRK frontend uses refined base types {ν:b | r} and dependent arrows. Bidirectional synthesis/checking generates CHCs for subtyping; a base refinement subtype emits ∀ν:b. r1 → r2. The authors prove both type soundness and constraint-generation soundness. (§5.2–§5.4, pp.19–21)

how to do it

1. Keep expressions in A-normal form so dependent applications substitute variables into codomains (§5.2, p.19)
2. Selfify variables by conjoining ν = x, enabling path-sensitive occurrence typing (§5.3, p.20)
3. Generate synthesis, checking, and subtyping constraints; for each base subtype emit the universal implication (§5.4, p.21)
4. Solve the CHC assignment and apply the declarative typing theorem (§5.4, p.21)

The end-to-end theorem says: “if a program passes constraint generation and the resulting constraints are satisfiable, then the program evaluates to a value in its type’s interpretation.” (§5.4, p.21) The runtime erases type annotations, so refinements affect static checking only (§5.2, p.19).

Verus form (inference)

Inference: Verus expresses analogous value relations with spec fn, requires, ensures, and proof lemmas, but does not infer dependent function refinements through this λ-calculus algorithm. A Verus implementation can retain executable Rust and attach contracts; the inferred CHC machinery would be an external front end whose result must be checked by Verus proofs.

technique: expressive memory invariants beyond SMT fragments

The case studies use Lean definitions when Flux’s prior SMT-restricted language cannot express the property. The ring buffer tracks initialized slots with a map and defines init_inv using a quantified condition over valid indices. The paper gives the invariant verbatim: “def init_inv ( rb : RingBuffer ) : Prop := ∀ i : Int , 0 ≤ i ∧ i < rb . cap → valid_idx rb i → rb . init i” (§6.1, p.23)

how to apply it

1. Keep simple arithmetic definitions (rb_len, valid_idx) as ordinary refinement functions (§6.1, p.23)
2. Define the quantified invariant in Lean, over every index in the capacity range (§6.1, p.23)
3. Mark the method obligation so the Lean backend can use that definition at the memory read (§6.1, p.23)
4. Prove both the read precondition and invariant preservation (§6.1, p.23)

The authors report five case-study totals: 1,250 Flux lines, 52 CHCs, 416 specification lines, and 2,784 proof lines (Table 1, p.22). The RingBuffer row is 257 Flux lines, 10 CHCs, 75 specification lines, and 501 proof lines. These denominators describe the artifact’s reported line counts, not proof correctness probabilities. The paper also cautions that “complex invariants (e.g., in merge and quicksort_range) must still be supplied by hand.” (§6.1, p.23)

Verus form (inference)

Inference: A Verus version would define valid_idx and an init_inv spec fn, state it in the buffer invariant, and prove that get requires initialization for the selected index. A trusted wrapper for maybe-uninitialized memory would remain a trust boundary unless its behavior is modeled and proved. Quantified specifications may require carefully shaped lemmas and solver triggers; Flex’s ability to use arbitrary Lean predicates does not transfer automatically.

evidence, trusted base, and product implications

The strongest automation result covers 880 constraints across four suites: 843 successes (95.7%); among 164 cyclic constraints, 135 succeeded (82.3%). Flex took 21.8 minutes total versus 31 seconds for Liquid Fixpoint’s SMT backend (Table 4, p.25). The setup was Ubuntu 24.04.4, AMD Ryzen 7 8845HS, 8 cores/16 threads, 27 GB RAM (§6, p.21). Flex-bench was excluded from the automation experiment because its examples were deliberately beyond SMT automation (§6.3, p.24).

The paper’s success is conditional on Lean’s kernel, the soundness of the oracle, the generated frontend, and trusted wrappers such as the ring-buffer slice abstraction. It does not prove that a specification matches a product requirement, that Rust compilation and unsafe libraries are correct, or that every generated proof is fast enough for development. The paper itself identifies manual work, qualifier sensitivity, recursion/heartbeat limits, and remaining concrete goals (§6.1–§6.3).

Inference: For VeruLaw, the most direct reuse is a certificate-producing CHC layer for specification or invariant candidates, with Verus checking the final Rust proof. This could reduce reliance on opaque SMT answers, but it would add a Lean kernel and translation boundary to the trusted base. The reported 95.7% success and 21.8-minute total are evidence for this paper’s benchmark suite only. The product threat is medium: an agent-generated contract can still be wrong, and a solver-generated proof can certify that wrong contract; the value is an independently checkable certificate and better counterexample/debugging structure.

techniques for the catalog

• foundational CHC encoding — represent unknown refinements and loop invariants as existential Horn predicates interpreted by Lean
• Zap acyclic elimination — compute strongest acyclic solutions, rewrite constraints, and emit kernel-checkable certificates
• Fix predicate abstraction — instantiate qualifier templates and prune cyclic candidates with a sound oracle
• certificate construction — certify every solver rewrite with Lean proof terms rather than trusting a solver result
• Imp VC generation — synthesize loop-invariant obligations from entry, body, and exit conditions
• refinement CHC generation — derive universal subtype implications from dependent refinement types
• quantified memory invariant — define non-SMT invariants such as initialized ring-buffer indices in Lean Checked 2026-10-13: audit record khan2026foundational; paper-study comparison complete; gate executed; experiments not rerun

Last edited: 2026-10-14