Agda-IVE

What is Agda-IVE?

Agda-IVE (Agda Integrated Verification Environment) is a conceptual name for the combination of (1) Agda (2) Agda's plug-in mechanisms that enable us to invoke external (automatic) theorem provers from Agda and (3) libraries written in Agda Language that contain definitions required for using the plug-ins. With Agda-IVE, you can switch interactive and automatic verification at any time of proving. This contrasts with the situation that Agda itself heavily relies on interactive proving. The mixed approach taken by Agda-IVE allows you to formally solve large and complicated verification problems for which automatic provers would not terminate in reasonable time and hence require a small amount of human directions. Examples of such human directions include:

Agda-IVE was designed and coined by National Institute of Advanced Industrial Science and Technology (AIST) Research Center for Verification and Semantics (CVS), Japan.

MLAT Plug-in

In this section, we take MLAT plug-in as a concrete example to explain Agda-IVE. This plug-in calls a Hoare triple prover that is a compoment of the MLAT system, developed and copyrighted by AIST/CVS.

Introduction

MLAT plug-in enables us to verify a Hoare triple using Agda as follows:
proof :: HT pre code post
proof = {!external "mlat"!}
where code is a target program specified in a simple while-language called PML (Pointer Manipulation Language) and pre and post are formulas that specify pointer structures pointed to by program variables. Note that these are in fact written in Agda Language. The existence of a term at type HT pre code post says that the triple can be proved. In Agda, the expression {! ... !} is a placeholder for a term and filling placeholders with appropriate terms amounts to writing proofs. The plug-in call external "mlat" is considered to have the requested type if the automatic prover answers yes, in which case Agda-IVE will display:
proof :: HT pre code post
proof = external "mlat"

Smaller Example

The following is a small but complete example of using MLAT plug-in:
-- #include "../MLAT_Hoare/PmlHoareLogic.agda"

postulate next :: Fld
reach(!a,!b::Var) :: PFormula = (a ===> EF next (nom b))  -- reachability

postulate x :: Var  -- program variables
postulate y :: Var
postulate z :: Var

prog :: Program = [ (x,next) .:= y ]
proof :: HT (reach y z && not (reach y x)) prog (reach x z) = {!external "mlat"!}
There are three (distinct) program variables, each of which points to a memory cell. The program is x.next := y which updates the next field of the cell pointed to by x to the cell pointed to by y. This example aims at verifying that reach y z && not (reach y x) is a sufficient precondition for the execution to make the cell pointed to by z reachable from the cell pointed to by x.

Since pointer logic is so powerful, the availability of the MLAT's automatic prover in practice is rather restrictive. For instance, we are advised to decompose postconditions into conjunctions of simpler formulas and then apply an external call to each conjunct in order that automatic verification can terminate in more reasonable time. Given a simpler postcondition, we can often guess a simpler, weaker precondition that substitutes the entire precondition, which can be done by collecting relevant formulas from the precondition expressed also as a conjunction.

Manual decomposition of the triple with respect to the construction of the program code may also be useful. In particular, since MLAT plug-in for the time being can verify a triple only for a basic block, this process is almost mandatory.

We expect that many of such decomposition tasks can be automated in the future although they need to be done manually for now.

Interactive Problem Decomposition

We use Agda's functionalities for interactively constructing proofs, such as C-c C-r (refine current goal) and C-c C-l (introduce local definitions). In this manner, we decompose problems into smaller ones. When you feel a goal small enough, you can try using automatic prover, by refining it with external "mlat".

For example, consider the following problem.

prog1 :: Program = [ z :=. (z,next) ]
prog2 :: Program = [ (y,next) .:= z ]
prog3 :: Program = prog1 ++ prog2
pre   :: PFormula = {! !}
proof :: HT pre prog3 (reach x z) = {! !}
We are to find a sufficient precondition pre for the execution to let (reach x z) hold as well as a proof that pre is indeed a sufficient precondition. Instead of trying to do this directly, we can do better by decomposing the problem using Agda's interactive functionalities as follows:
prog1 :: Program = [ z :=. (z,next) ]
prog2 :: Program = [ (y,next) .:= z ]
prog3 :: Program = prog1 ++ prog2
pre   :: PFormula = {! !}
proof :: HT pre prog3 (reach x z) =
  let mid :: PFormula = {! reach x y && reach x z !}
      h1 :: HT pre prog1 mid         = {! !}
      h2 :: HT mid prog2 (reach x z) = {!external "mlat"!}
  in  seqHp h1 h2
The proof is now seqHp, a postulated constant or an axiom that provides sequence introduction in the Hoare logic, applied to two subproofs. It is relatively easy to determine an intermediate condition mid that lets the second half of the proof, h2, hold. Having set mid to be a conjunction, we can accordingly reduce the first half of the problem, h1, again interactively as follows:
prog1 :: Program = [ z :=. (z,next) ]
prog2 :: Program = [ (y,next) .:= z ]
prog3 :: Program = prog1 ++ prog2
reach1(!a,!b::Var) :: PFormula = (a ===> EX next (EF next (nom b)))
pre   :: PFormula = {! !}
proof :: HT pre prog3 (reach x z) =
  let mid :: PFormula = reach x y && reach x z
      h1 :: HT pre prog1 mid =
        let pre11 :: PFormula = {! reach  x y !}
            pre12 :: PFormula = {! reach1 x z !}
            w11 :: HT pre   []    pre11       = {! !}
            h11 :: HT pre11 prog1 (reach x y) = {!external "mlat"!}
            w12 :: HT pre   []    pre12       = {! !}
            h12 :: HT pre12 prog1 (reach x z) = {!external "mlat"!}
        in  cnjrHp (seqHp w11 h11) (seqHp w12 h12)
      h2 :: HT mid prog2 (reach x z) = external "mlat"
  in  seqHp h1 h2
The proof h1 is now conjunction introduction applied to two proofs corresponding to the respective conjuncts. The subproofs are obtained by sequence introduction. Observe the use of the empty program [] which enables us to use MLAT in order to solve entailment problems.

Mnemonic constants and functions can also be defined flexibly on top of Agda. For instance, we introduced reach1 for expressing the non-reflexive reachability. In Agda 1, however, introducing such top-level names requires re-typechecking of an entire input text.

After proving the major parts h11 and h12, we can easily combine their preconditions to compose the entire precondition, pre:

prog1 :: Program = [ z :=. (z,next) ]
prog2 :: Program = [ (y,next) .:= z ]
prog3 :: Program = prog1 ++ prog2
reach1(!a,!b::Var) :: PFormula = (a ===> EX next (EF next (nom b)))
pre   :: PFormula = {! reach x y && reach1 x z !}
proof :: HT pre prog3 (reach x z) =
  let mid :: PFormula = reach x y && reach x z
      h1 :: HT pre prog1 mid =
        let pre11 :: PFormula = reach  x y
            pre12 :: PFormula = reach1 x z
            w11 :: HT pre   []    pre11       = {!external "mlat"!}
            h11 :: HT pre11 prog1 (reach x y) = external "mlat"
            w12 :: HT pre   []    pre12       = {!external "mlat"!}
            h12 :: HT pre12 prog1 (reach x z) = external "mlat"
        in  cnjrHp (seqHp w11 h11) (seqHp w12 h12)
      h2 :: HT mid prog2 (reach x z) = external "mlat"
  in  seqHp h1 h2
In this way, interactive problem decomposition can be particularly useful for analyzing what has to be proved.

Instructions for Installing MLAT Plug-in

  1. Download a tarball of MLAT system from here which contains a special version of MLAT system tailored for Agda-IVE as well as its backend solver JavaBDD. Extract this tarball to a directory, say C:\MLAT-X. To use MLAT system, you must have JAVA system installed.
  2. To use MLAT plug-in, the pfvalid executable-script file must be in PATH. For those using Windows, download pfvalid.bat and put it to a directory in PATH. If you have extracted the tarball to a directory other than C:\MLAT-X, you must for yourself open pfvalid.bat by notepad and edit the value of the environment variable MLAT_HOME.
  3. Windows users can download the latest version of Agda executable emacsagda.exe which communicates with MLAT system better than before. Replace the emacsagda.exe found in the directory where Agda was installed with the new file above. Linux users are requested to download the latest source package Agda-1.0.2a-latin1.tar.gz and compile it manually.
  4. Finally, you can download a preliminary version of the libraries and examples from here. This package may be updated in the near future.

Written by Norio KATO on November 26, 2008.