miniproof

miniproof

A lightweight formal verification language

miniproof states the laws of a language's operations and commands as a small equational theory, and checks the proofs written in it. From a theory it generates a Haskell record of functions and a polysemy effect, and it turns the laws into properties that test an interpreter.

Read the READMEBrowse the source

A theory from the review gate

The NixLab review gate decides whether a merge request may merge. Its verdicts are a theory of three constructors and one operation, join, which combines two verdicts. The gate's verdict is the join of every rule's settled verdict.

-- verdicts form a chain: approve < hold < reject

data Verdict = approve | hold | reject

op join    : Verdict -> Verdict -> Verdict

eq joinAssoc       : join a (join b c) = join (join a b) c
eq joinComm        : join a b = join b a
eq joinIdem        : join a a = a
eq approveIdentity : join approve a = a
eq rejectAbsorbs   : join reject a = reject

thm holdOverApprove : join hold approve = hold
  = join approve hold by joinComm
  = hold by approveIdentity

The theorem holdOverApprove is proved in two steps. The first cites joinComm and the second cites approveIdentity. miniproof checks that each step follows from the equation it cites, and refuses the proof if one does not.

How it fits together

  1. Theory

    A theory declares sorts, data sorts, operations, commands and named equations. It can import other theories.

  2. Checked proofs

    Each theorem carries a written proof. miniproof checks every step against the equation, theorem or premise it cites, and refuses a step that does not follow.

  3. Generated algebra and effect

    Template Haskell compiles a theory under a binding to Haskell types. Its operations become a record of functions, and its commands become a polysemy effect.

  4. Laws against an interpreter

    Each equation becomes a property that any value of that record must satisfy. Each law over programs becomes a property that both sides, run through a pure interpreter from the same state, give the same answer and the same final state.

Supported today

  • Sorts, operations and named equations, with premises for conditional equations.
  • Data sorts with free constructors, and proofs by cases on them.
  • Proofs by structural induction, which cite the induction hypothesis at a smaller argument.
  • Parametrised sorts and sort variables, with standard theories of lists, optional values and maps.
  • Commands, and laws over programs written with pure and do, with the monad laws built in.
  • Rewriting to a normal form, with certificates that are replayed independently.
  • Mappings between theories, checked syntactically to preserve operations and equations.
  • A Haskell record of functions and a polysemy effect, generated from a theory.
  • Properties that test an algebra against the equations and an interpreter against the laws over programs.

In progress

These are planned and not yet available. Each links to the issue that tracks it.

What it is not

miniproof is not a general proof assistant. It checks equational proofs about the operations and commands of a language. The metatheory of a language belongs in Agda, compiled to Haskell through agda2hs.