Table of Contents
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.
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.
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.
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.
Looking at the scripts used by the continuous integration may help with the installation and translation.
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.
refiner_why3quant
make
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.
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"
donePVS can then be compiled following the instructions in $PVSPATH/INSTALL.
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
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))))The easiest way is to use the opam (version 2.0 or later):
opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner_why3quant'
A local OPAM switch with all dependencies installed can be set up with (can be called at the root of personoj)
opam switch create .
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.
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)load-personoj can be called with a parameter which supersedes
the variable $PERSONOJPATH.
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.
if the translation fails, ensure that $PVSPATH and
$PERSONOJPATH are correctly set up.
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).
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:
why3;
that calls external solvers.