Liquid PureScript · lps Refinement types · external tool · Z3

How it works

CoreFn in, verdicts out.

No compiler fork, no macros. The verifier reads the CoreFn JSON the PureScript compiler already emits, pairs it with your spec file, and turns each function into a handful of small logical obligations that Z3 either proves or breaks.

01The pipeline

Two inputs converge. On the left, spago build (with a no-op backend) drops corefn.json for each module. On the right, your .lps file is parsed to a spec. They meet at Vc, the verification-condition generator, which walks the code in checking mode and emits obligations. Each obligation becomes SMT-LIB2 text piped to the z3 binary.

Demo.purs → corefn.jsonspago build, backend cmd: "true"
Demo.lpsthe refinement layer
CoreFn.DecodeJSON → Module (ADT)
Spec.Parser.lps text → aliases + fn specs
Resolvefloat-alias table → PrimOp per local Var
signatures cross-checked against docs.json
↓   both feed   ↓
Vc — verification-condition generatorchecking-mode traversal of each spec'd decl → [Obligation]  where Obligation = { ctx : [Pred], goal : Pred, span }
Logic.SmtObligation → SMT-LIB2 text
Solver.Z3z3 -in · unsat ⇒ SAFE / sat + model ⇒ UNSAFE
Reportverdict + source span + countermodel

Every arrow is a plain ADT-to-ADT function; the only effects are reading files and spawning z3. The SMT boundary is text, so every obligation can be dumped with --smt2-dir and replayed by hand — the same inspectability principle as differential conformance in the backends family.

02Why CoreFn, and what Resolve is for

CoreFn is the compiler's desugared core: if/then/else is already a Case, guards are alternatives, and every node carries a source span. It is also backend-agnostic — the same core the Erlang and other backends consume — so a proof about the core holds for any backend's output.

One wrinkle shapes the design. The compiler floats type-class methods: n > 0 is not an application of greaterThan at the use site. Instead a synthetic module-local declaration appears — Demo.greaterThan = Data.Ord.greaterThan ordInt — and the use site references that local. Resolve scans for that shape and builds a table mapping each local name to a primitive SMT operation (>, +, -, &&, …) for Ord, Ring, Semiring, EuclideanRing, Eq, and HeytingAlgebra on Int / Boolean.

Types come from docs.json, not externs — externs are CBOR now, but docs.json carries full type ASTs as JSON. Specs are cross-checked against it: an arity or base-type disagreement fails the function before any solving, so a spec that has drifted from its code is caught as a mismatch, not a false verdict.

03Checking mode, for a reader who knows PureScript but not SMT

Take a spec f :: t1 -> tr and its definition f x = body. The verifier builds a context Γ — a bag of facts it may assume — and asks whether the result refinement must hold.

  1. Bind the arguments. Each argument's refinement enters Γ as an assumption. For abs :: Int -> Nat, the argument is unrefined, so Γ starts empty.
  2. Walk the body, collecting path conditions. A Case on a Boolean adds the scrutinee to Γ on the true branch and its negation on the fallback. Guards do the same, each later guard also assuming the earlier ones failed. A non-recursive let binds an equality into Γ.
  3. At each leaf — an expression in tail position — emit an obligation: under Γ, does the result refinement hold with the leaf substituted for the result variable?
  4. Discharge it. One obligation, one Z3 query: assert Γ, assert the negation of the goal, ask check-sat. unsat means the goal can't be broken — SAFE. sat hands back a model — a concrete counterexample — UNSAFE.

Worked example: why bad fails

bad n = n - 1 against Nat = { v : Int | v >= 0 }:

Γ            = { }                         -- n is unrefined
body embeds  = n - 1                        -- Resolve maps Demo.sub to (-)
obligation   = { } ⊢ (n - 1) >= 0
SMT          = (declare-const n Int)
               (assert (not (>= (- n 1) 0)))
               (check-sat)
result       = sat,  model  n = 0     →  UNSAFE at Demo.purs:9:9

And abs, same result type, produces two obligations — one per branch — n > 0 ⊢ n >= 0 and ¬(n > 0) ⊢ (0 - n) >= 0 — both unsat when negated, so SAFE.

Compositional by construction

A call to a spec'd function checks that function's precondition at the call site (an obligation) and assumes its postcondition via a fresh result variable. Recursion assumes the function's own spec — standard inductive reasoning. Call facts are scoped per branch, so a postcondition justified under one path can't leak into a sibling.

Sound, sometimes imprecise

An application of an unknown function, or a let the logic can't embed, becomes a fresh unconstrained variable. The tool may reject good code (imprecision), but it will never bless bad code inside the trusted fragment. The logic stays in QF_LIA — quantifier-free linear integer arithmetic — so Z3 is a decision procedure, never a heuristic; “unknown” is not a possible answer.

04Two bugs worth telling

The build turned up two failures that are really facts about the boundary being crossed — worth keeping.

The parser that ate a keyword

Adding juxtaposition application to the spec parser (so len xs reads as “apply len to xs”) made the application parser greedy: it happily swallowed the following type keyword as a third argument to a measure. The fix was to make the reserved words actually reserved — the application parser has to stop at a keyword, not consume it. A satisfying bug: the grammar quietly told you where one declaration ends and the next begins.

Array is spoken for

The natural SMT sort name for PureScript arrays is Array — but SMT-LIB reserves Array for its own theory of arrays, and Z3 rejected the declaration outright. So at the SMT boundary the sort is renamed PSArray; element types are erased and only length is visible to the logic. The lesson generalises: the text boundary to the solver is a foreign namespace, and crossing it means respecting its reserved words.