Liquid PureScript · lps Refinement types · external tool · Z3

The spec language

A small language for saying which value.

An .lps file is a list of declarations: type aliases, function specs, trusted assume specs, and data / measure declarations. The refinement logic stays inside a decidable fragment on purpose — non-linear arithmetic is rejected at parse time, so Z3 is always a decision procedure.

01The grammar

specfile::= { decl }
decl::= "type" CONID [ vars ] "=" rtype  — alias
 | VARID "::" fnspec  — function spec
 | "assume" VARID "::" fnspec  — trusted spec
 | "data" CONID "=" ctors  — datatype
 | "measure" VARID "::" … + equations  — measure
fnspec::= rtype { "->" rtype }
rtype::= "{" VARID ":" base "|" pred "}"  — refined base
 | base  — unrefined (pred = true)
 | CONID  — alias reference
base::= "Int" | "Boolean" | CONID  (datatype) | "Array"
pred::= pred ("&&" | "||") pred | "not" pred | "(" pred ")"
 | term ("==" | "/=" | "<" | "<=" | ">" | ">=") term
 | "true" | "false"
term::= term ("+" | "-") term | term "*" term  (literal·var only)
 | INT | VARID | measure-app | "(" term ")"

The slice logic is QF_LIA + Bool; multiplication of two variables is rejected when the spec is parsed. Measures widen it to QF_UFLIA — the “UF” is the uninterpreted measure function.

02Refined base types

A refinement is a base type, a binder, and a predicate the value must satisfy. Name it once with type, reuse it everywhere.

type Nat = { v : Int | v >= 0 }

abs  :: Int -> Nat
sign :: Int -> { s : Int | 0 - 1 <= s && s <= 1 }
flag :: { n : Int | n >= 0 } -> { b : Boolean | b }

abs and sign prove SAFE; flag shows a refinement on a Boolean result — the returned bool must be true whenever the argument is non-negative.

03Dependent binders

Argument names in a spec are binding positions: an earlier argument's binder is in scope in every later refinement. This is how a spec states a relationship between arguments.

myDiv :: Int -> { d : Int | d /= 0 } -> Int

clamp :: { lo : Int }
      -> { hi : Int | hi >= lo }              -- hi related to lo
      -> Int
      -> { v : Int | v >= lo && v <= hi }     -- result related to both

clamp proves SAFE: under hi >= lo, every branch of the body lands in [lo, hi].

04assume — trusted specs

Imported and FFI functions have no CoreFn body to check. An assume declaration states a spec that is taken on faith — the tool trusts it and uses it at call sites, but never verifies it. It is an axiom you are choosing to add. 

-- trusted spec for a floated class method, used to discharge call sites
assume min :: { a : Int }
           -> { b : Int }
           -> { v : Int | (v <= a && v <= b) && (v == a || v == b) }

Trust is explicit and visible. Shared corpora of assume specs live in .lps files you prepend with --include; lib/prelude.lps seeds min / max / abs / signum / clamp on Int. Nothing is trusted that you didn't write down.

05data and measure — reasoning about structure

To reason about a user datatype, declare its shape and a measure: a logic-level function from the datatype to a number, with one equation per constructor. The verifier treats the datatype as an opaque sort and reasons inductively about constructors. 

data IntList = INil | ICons Int IntList

measure len :: IntList -> { v : Int | v >= 0 }
  INil       = 0
  ICons x xs = 1 + len xs

count  :: { l : IntList } -> { v : Int | v == len l }
append :: { a : IntList } -> { b : IntList }
       -> { v : IntList | len v == len a + len b }
singleton :: Int -> { v : IntList | len v == 1 }

All three prove: count by assuming its own spec at the recursive call; append through constructor-application facts; singleton through nested constructor applications. Drop the + 1 from a would-be count and it refutes with a countermodel over the uninterpreted sort.

Arrays come built in

Array is a built-in element-erased datatype with a built-in length measure — only the length is visible to the logic. Array literals contribute exact lengths, and lib/arrays.lps supplies trusted specs for length / cons / snoc / take / drop. 

-- a valid index into a non-empty array
mid :: { xs : Array | length xs > 0 }
    -> { v : Int | v >= 0 && v < length xs }

mid xs = length xs / 2 proves under the non-empty precondition; the same body without it — badMid — refutes with the empty array. See them both on the verdicts page.