Translating PVS to Dedukti with Personoj

Gabriel Hondet


Table of Contents

1. Translating theoretically
2. How to translate and X-check PVS files?
2.1. Requirements
2.2. Compiling PVS with a patched prelude
2.3. Installing lambdapi
2.4. Install and setup of personoj
2.5. Translating the Prelude
3. Xchecking PVS proofs

Personoj is a suite of tools to translate specifications from the higher order, highly automated proof assistant PVS to the universal type checker Dedukti.

Translating PVS to Dedukti serves mainly two purposes. The first is to port PVS developments to other proof assistants, so that users of say, Coq, could use in their work theorems or specifications done in PVS. The second is to cross-check PVS specifications and proofs with an independent checker in order to increase our trust in these proofs and specifications.

This work is part of a larger project led by the Deducteam made of Logipedia and Nubo.

1. Translating theoretically

Translating PVS into Dedukti requires to be able to express a sufficiently large subset of the theory of PVS into the λΠ-calculus modulo theory. Such a task is usually not easy. In the case of PVS, defining the logic of PVS is already tricky, but its core has been formally studied in F. Gilbert PhD thesis. In particular, two languages has been defined. The first named PVS-Core is the language in which PVS specifications are written in. It is based on Simple Type Theory with implicit predicate subtyping, ad-hoc polymorphism and some sort of prenex polymorphism and dependent types. In particular, this language does not contain proof terms and type checking a term is not decidable. The second language named PVS-Cert is a language for PVS-Core certificates. It replaces implicit predicate subtyping of PVS-Core with explicit predicate subtyping. This allows terms to contain proof terms and type checking terms becomes decidable.

PVS-Cert has been encoded in lambdapi, an extension of Dedukti with meta-variables. This encoding is described there. The encoding of PVS-Core is work in progress. In particular, encoding implicit predicate subtyping requires some procedure to make it explicit. Personoj provides the encodings that can be used by lambdapi (in its development version) to explicit PVS-Core specifications and type check them.

2. How to translate and X-check PVS files?

We call translation of a PVS file the process of creating a file in the syntax of lambdapi (suffixed by .lp) from a PVS specification (suffixed by .pvs). Cross-checking a PVS file consists in type checking its translation.

Important

this document is focused on the translation of the standard library of PVS called Prelude. Its management is a bit particular because it is somewhat linked to the lisp code of PVS. Some steps shouldn’t be necessary when translating other libraries such as NASA’s pvslib.

Tip

Looking at the scripts used by the continuous integration may help with the installation and translation.

Note

If not stated otherwise, all paths are relative to the root of the local clone of personoj (if the paths are not absolute). This path is also assumed to be stored in the environment variable $PERSONOJPATH.

2.1. Requirements

2.2. Compiling PVS with a patched prelude

Note

Compiling PVS is required because the prelude must be patched to remove some sort of ad-hoc polymorphism. Because PVS is linked against the prelude during compilation, we need to patch the prelude and then compile PVS with the modified prelude.

Caution

this tutorial is made for Linux operating systems. PVS handles poorly BSD systems and I do not use MacOS nor Windows.

git clone https://github.com/CSL-SRI/PVS
cd PVS
git checkout pvs7.1
export PVSPATH=$(pwd)

The patches to be applied to the prelude are in prelude/patches/ and must be applied in the order defined by their filename.

for p in $(find 'prelude/patches/' -name '*.diff' | sort); do
 patch "${PVSPATH}/lib/prelude.pvs" "$p"
done

PVS can then be compiled following the instructions in $PVSPATH/INSTALL.

Note

It’s difficult (but possible) to use a system-installed SBCL to compile PVS. For this, the script tools/build-pvs.sh can be used:

cp tools/build-pvs.sh "$PVSPATH"/
cd "$PVSPATH"
autoconf
./configure
./build-pvs.sh

Tip

PVS can be loaded into any SBCL session (unless the running SBCL is not the same as the one PVS has been compiled with) using

(defun load-pvs (&optional pvspath)
  "Load PVS into the current lisp environment. Argument PVSPATH is the filespec
to the sources of PVS. If not provided, it is fetched from the environment
variables PVSPATH."
  (let ((pvspath
          (cond
            (pvspath (uiop:ensure-pathname pvspath :ensure-directory t))
            ((uiop:getenvp "PVSPATH") (uiop:getenv-pathname "PVSPATH"))
            (t (error "Cannot load PVS: PVSPATH not set.")))))
    (uiop:with-current-directory (pvspath)
      (load "pvs.system")
      (uiop:symbol-call :make "OPERATE-ON-SYSTEM" :pvs :load))))

2.3. Installing lambdapi

The easiest way is to use the opam (version 2.0 or later):

opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner_why3quant'

Note

A local OPAM switch with all dependencies installed can be set up with (can be called at the root of personoj)

opam switch create .

Note

If the compilation of lambdapi fails, opam may force the exact version of all dependencies with the --locked option. The downside is that is also forces the version of ocaml and may require changing the switch.

2.4. Install and setup of personoj

The encoding can be install with (BSD) make,

cd encoding && make install

The exporter must be loaded by PVS upon startup. For this, add the following to ~/.pvs.lisp

(defun load-personoj (&optional pth)
  "Load Personoj specification exporter and proof exporter. If given, PTH is the
path to the root of the repository. Otherwise, the root is taken from the
environment variable PERSONOJPATH."
  (let* ((pth (cond
                (pth (uiop:ensure-pathname pth :ensure-directory t))
                ((uiop:getenvp "PERSONOJPATH")
                 (uiop:getenv-pathname "PERSONOJPATH" :ensure-directory t))
                (t (error "Cannot load personoj: PERSONOJPATH not set."))))
         (pth (merge-pathnames #P"pvs_patches/" pth)))
    (uiop:with-current-directory (pth)
      (load "load.lisp"))))
(load-personoj)

Tip

load-personoj can be called with a parameter which supersedes the variable $PERSONOJPATH.

2.5. Translating the Prelude

Caution

BSD makefiles are used rather than GNU makefiles. Linux users may have to use bmake rather than make.

cd prelude && make

will create a set of empty .lp files and translate and type check other files. The (nearly) empty files stand for theories that can’t be translated yet.

Tip

if the translation fails, ensure that $PVSPATH and $PERSONOJPATH are correctly set up.

3. Xchecking PVS proofs

PVS files do not contain proof terms. One of the consequences is that proofs are not reprensented as lambda terms and thus verifying a proof does not consist in checking that the type of the term is the proposition that it proves. A proof is recorded as a sequence of tactics [1] that are replayed.

Because LPMT relies on the Curry-Howard principle, that a proof is a term whose type is the type of the proposition it proves, PVS proofs must be transformed. PVS tactic sequences are too fragile and too much implementation dependant to be processed. We rather use the proveit program to replay the proofs in PVS and print all the sequents of the proof in a trace file.

The PVS patch proof-hooks.lisp makes proveit to output traces that can be processed by the program in psnj_toolbox. The patch proveit.lisp allows proveit to operate correctly on the PVS prelude (otherwise proveit does nothing when called on the prelude).

Caution

Allegro PVS must be used to produce traces. Traces may be produced with proveit --traces -l <path/to/file.pvs>.

In particular, the ocaml package provides a psnj binary with a command pipe that transforms a PVS file into a type checked lambdapi file. To do this, the following operations are carried out:

  1. sequents are extracted as propositions from the traces along with their position in the proof tree;
  2. these propositions are transformed into implications such that the premises imply the conclusion (premises and conclusions are defined by the positions in the proof tree);
  3. propositions are rewritten into a weaker logic (namely Simple Type Theory with logical connectives);
  4. each inference step is proved through a call to the tactic why3; that calls external solvers.


[1] The list of tactics is available here