I had attended the Eleventh Summer School on Formal Techniques (SSFT 2022) online.
During this event, I first got to use the PVS theorem prover. Had
heard a lot about it before the SSFT, but had never used it. Have come
across a mention of the grind proof strategy of PVS more
than a couple of times.
This blog post is a description of the first proof that I did with PVS, along with some stuff that I found out while doing it.
Mistakes, if any, are my own and corrections are welcome.
(I originally wrote this blog post right after the SSFT back in 2022, but didn't finish writing all I wished to. Was worried of errors in what I had written, so refrained from putting it up online.
But hey, better to make it public and let others correct me than to keep this to myself, right? 🙂)
By the way, registration for this year's SSFT is open at the moment. It was a great experience for me even though I joined online. If possible, do join physically!
PVS, which stands for Prototype Verification System, is an interactive theorem prover.
Proofs are constructed with guidance from the user. A batch mode is available to re-run pre-existing proofs, though.
The logic used by PVS is based on sequent calculus.
Proofs in PVS seem to be in the 'backward-reasoning' style. We go from the goal to the assumptions. A top-down approach.
Users can define custom procedures, known as strategies (analogous to tactics in coq), to construct proofs for automating the theorem proving process.
PVS is implemented mainly in common lisp and requires a common-lisp runtime to work.
Emacs or vscode can be used as front-ends to interact with the pvs system. I used emacs.
Let me show one of the first proofs that we did in PVS. Quite an amusing one too.
One of the proofs that we did during the summer school was inspired by the lyrics of the song 'Everybody loves my baby' which went like:
Everybody loves my baby
But my baby don't love nobody but me.
There are two conditions:
So we could formulate them as:
∀p, loves(p, baby)∀p, loves(baby, p) → (p = me)where loves(a, b) means a loves
b, but not necessarily b loves
a.
With these assumptions, it is possible to prove that 'me' and 'my baby' are the same person!
| No | Statement | Reason |
|---|---|---|
| 1 | ∀p, loves(p, baby) |
Assumption |
| 2 | ∀p, loves(baby, p) → (p = me) |
Assumption |
| 3 | loves(baby, baby) |
1 with p=baby |
| 4 | loves(baby, baby) → (baby = me) |
2 with p=baby |
| 5 | baby = me |
Modus ponens with 4 and 3 |
But of course, 'me' and 'my baby' can't have been same person. We were able to derive this due to an incomplete way of framing the assumptions.
Look at ∀p, loves(baby, p) → (p = me). The baby may love
themselves, which gives loves(baby, baby), but that doesn't
mean baby = me.
This is an example of an attempt to prove a theorem exposing a bug in the specification.
Anway, let's try doing the proof with these assumptions itself.
Writing this down as a PVS specification file (a file with
.pvs extension),
mybaby: THEORY
BEGIN
% 'person' is an inhabited Type
% The '+' means that there is at least one term of the type 'person'
person: TYPE+
% 'me' and 'mybaby' are people
% ie, they are values of the type 'person'
me, mybaby: person
% A few variables of type 'person'
x, y, z: VAR person
% A predicate accepting two values of type 'person'
loves(x, y): boolean
% Everyone loves my baby
everybodyLovesMyBaby: AXIOM
forall x: loves(x, mybaby)
% If my baby loves somebody, that is me
mybabyLovesOnlyMe: AXIOM
loves(mybaby, x) IMPLIES x = me
% We this, we can prove that mybaby and me are same!
mybabyIsMe: LEMMA
mybaby = me
END mybaby
(Anything that follows a % in a line is a comment till
the end of that line.)
First, we got to type check this file.
In the emacs interface, we can do C-c C-t for that
(C is Ctrl key).
If the file type checked successfully, we would get a message like
mybaby typechecked in 0.01s: No TCCs generated; 1 msg
TCC means Type-Correctness Conditions. They are obligations generated by the type checker 'which must be discharged before the corresponding theory is considered type correct'¹⁰. The example that we considering is quite simple and doesn't have any TCCs.
Now position the cursor over a part of the theorem to be proven,
which in our case is mybabyIsMe and do
C-c p.
mybabyIsMe spans two lines in our source file, placing
the cursor at any point in those two lines seems to be okay, even on
white space as long as it is on one of those two lines.
On starting the proof, we would get
mybabyIsMe :
|-------
{1} mybaby = me
Rule?
This is a sequent (have mentioned a little about sequents in PVS as part of the addendum of this blog post).
The Rule? is the prompt asking for our next input to
guide the proof.
Here are some handy keyboard shortcuts that can be used to retrive commands from usage history:
| Shortcut | Use |
|---|---|
M-p |
Last command |
M-n |
Next command |
M-s |
Auto-complete from history |
Back to our proof, in
|-------
{1} mybaby = me
the part above the line are the assumptions (which at this point is nothing) and that below the line is the current goal that needs to be proved.
Time to bring in our everybodyLovesMyBaby axiom. Type
the following into the prompt:
(lemma "everybodyLovesMyBaby")
and the sequent becomes:
{-1} FORALL (x): loves(x, mybaby)
|-------
[1] mybaby = me
Let's instantiate this using mybaby
(inst - "mybaby")
and we infer that the baby loves himself.
{-1} loves(mybaby, mybaby)
|-------
[1] mybaby = me
Bringing mybabyLovesOnlyMe as well into the picture,
(lemma "mybabyLovesOnlyMe")
and the sequent changes to
{-1} FORALL (x: person): loves(mybaby, x) IMPLIES x = me
[-2] loves(mybaby, mybaby)
|-------
[1] mybaby = me
Now we got loves(mybaby, mybaby) and
FORALL (x: person):
loves(mybaby, x) IMPLIES x = me. So we can sort of follow the
implication
(forward-chain -)
and the proof is done.
Forward chaining on -,
Q.E.D.
A transcript of the last proven proof can be shown with M-x
show-last-proof.
For the proof that we just did, it shows as:
mybabyIsMe :
|-------
{1} mybaby = me
Applying everybodyLovesMyBaby then
Instantiating the top quantifier in - with the terms:
mybaby, and then
Applying mybabyLovesOnlyMe
this simplifies to:
mybabyIsMe :
{-1} FORALL (x: person): loves(mybaby, x) IMPLIES x = me
{-2} loves(mybaby, mybaby)
|-------
[1] mybaby = me
Forward chaining on -,
This completes the proof of mybabyIsMe.
Q.E.D.
Once a proof is complete, it would be saved in a .prf
file. This is the proof script that records the steps that we took in
the course of proving the theorem. The proof can be rerun and verified
if needed using this.¹⁸ This file is
not meant to be edited by users and is best left alone so that only PVS
itself handles it.
.prf file associated with the proof that we just did
looks something like this:
(mybaby
(mybabyIsMe 0
(mybabyIsMe-1 nil 1823146151
("" (lemma "everybodyLovesMyBaby")
(("" (inst - "mybaby")
(("" (lemma "mybabyLovesOnlyMe") (("" (forward-chain -) nil nil))
nil))
nil))
nil)
((person nonempty-type-decl nil mybaby nil)
(mybaby const-decl "person" mybaby nil)
(mybabyLovesOnlyMe formula-decl nil mybaby nil)
(everybodyLovesMyBaby formula-decl nil mybaby nil))
shostak)))
I think shostak here refers to the name of a decision
procedure brought about by the work of R. E. Shostak.
Tried to find the file format of the .prf files, but
couldn't find it. It being a internal format and thereby being
susceptible to frequent changes may be a reason. Found a 2007 document
that mentions it though.
The goal of a PVS proof is to construct a tree where the leaf nodes
are trivially true (ie, TRUE).
In the case of the 'my baby loves only me' example, the tree looks like
∀p, loves(p, baby) ∀p, loves(baby, p) → (p = me)
------------------- ---------------------------------
loves(baby, baby) loves(baby, baby) → (baby = me)
-------------------------------------------------------------
baby = me
We can think of the proof tree growing from the root
(baby = me) to the leaves.
⊢ ∀p: loves(p, baby) ⊢ ∀p: loves(baby, p) → (p = me)
| |
| |
+-- ⊢ loves(baby, baby) +-- ⊢ loves(baby, baby) → (baby = me)
| |
| |
+------------------------------+
|
|
+-- ⊢ baby = me
The proof starts off as a sequent without antecedents with just the theorem to be proved as consequent.
From the PVS prover guide:
'At any time in a PVS proof, attention is focused on some sequent that is a leaf node in the current proof tree'.
A proof which has already been completed can be edited in a 'proof buffer'.
Position cursor on the theorem whose proof needs to be edited and do
M-x edit-proof.
For our 'my baby loves only me' proof, the (unedited) proof is:
;;; Proof mybabyIsMe-1 for formula mybaby.mybabyIsMe
(""
(lemma "everybodyLovesMyBaby")
(inst - "mybaby")
(lemma "mybabyLovesOnlyMe")
(forward-chain -))
Looks pretty much like lisp, doesn't it? Probably because it is lisp.
After editing, the new proof can be attached to the same or different
formula with M-x install-proof.
(Haven't properly figured this one yet, really. But this is roughly how it is.)
The default PVS interface is just emacs with some customizations. There are commands and key-bindings for some PVS-specific things, but other than that it's just emacs.
This also means that if you already have emacs set up, that configuration would also be loaded (provided there are no conflicts with those of pvs, I guess). For instance, I had evil-mode set up and could use it in the emacs launched by pvs as well.
Here are a few default key-bindings/commands:
| Description | Command | Key binding |
|---|---|---|
| Start proof | M-x pr |
C-c p |
| Type check | M-x typecheck |
C-c C-t |
| Show TCCs | M-x show-tccs |
C-c C-q s |
| Quit | M-x exit-pvs |
C-x C-c |
| Suspend PVS | M-x suspend-pvs |
C-x C-z |
We can change these key-bindings if we needed as it's just emacs, which is well known for its customizability.
Still, emacs can take time to get used to (although it is very well worth the time), and a plugin (made by some folks at NASA) to use VSCode editor as the interface to PVS is also available.
Lot of people at NASA seem to use PVS. They have published a large PVS library named the NASA PVS library.
In the PVS website, two 'flavours' of PVS can be seen. One with SBCL and the other with Allegro.
PVS needs an implementation of common lisp to work and SBCL and Allegro are two such implementations.
(SBCL stands for Steel Bank Common Lisp. A reference to Carnegie-Mellon University, the place from where SBCL originated. Andrew Carnegie was involved in the steel industry and Andrew Mellon was a banker.³)
One of the differences between SBCL and Allegro is that SBCL is free software whereas Allegro is a commercial implementation and comes with some restrictions although non-commerical use seems okay.
Another difference is that PVS operates faster when used with Allegro when compared to SBCL. Probably a reason why the PVS website recommends Allegro.
I first tried to run the example mentioned in this blog post using
PVS-SBCL, but it had some bug that prevented the proof from getting
completed (the '(forward-chain -)' wouldn't go through).
But PVS-Allegro had no problem with it.
Maybe the Allegro version gets more priority in the PVS development process.
Anyway, now I use the Allegro version. Still would've liked to try SBCL version when it gets fixed though.
The 2015 Hollywood film Martian shows PVS running on a computer on multiple occasions. Shankar had mentioned this during his session and I later found out a web-page that talks about it:
As evinced by the NASA PVS library, PVS enjoys some popularity at NASA. Yet PVS is not a tool meant to be used in space. But it can help in making sure that the stuff being sent to space would work as it is meant to be by verifying their designs.
Proof goals are sequents (a la Gentzen's sequent calculus).
Sequents are 'conditional tautologies'. Could think of them as formulas which are true only if some conditions are satisfied.
Sequents are usually represented like
A₁, A₂, ..., Aₙ
-----------------
B₁, B₂, ..., Bₘ
or equivalently, like
A₁, A₂, ..., Aₙ ⊢ B₁, B₂, ..., Bₘ
This means that if all the Aᵢ-s are true, then at least one of the Bᵢ-s must be true.
A₁ ∧ A₂ ∧ ... ∧ Aₙ ⊢ B₁ ∨ B₂ ∨ ... ∨ Bₘ
The Aᵢ-s are the antecedents and the Bᵢ-s are the consequents.
Both groups may simply be thought as formulas.
⎫
⎫ ⎮
A₁, A₂, ..., Aₙ ⎬ antecedents ⎮
⎭ ⎮
----------------- ⎬ sequent
⎫ ⎮
B₁, B₂, ..., Bₘ ⎬ consequents ⎮
⎭ ⎮
⎭
A sequent without antecedents is always true. For example,
⊢ M is always true (sort of an unconditional
tautology).
In PVS, a sequent looks like ¹¹
{-1} A1
{-2} A2
.
.
[-n] An
|-------
{1} B1
[2] B2
.
.
{-m} Bm
The antecedents (with negative numbering) appear above the line whereas the consequents (with positive numbers) show up under the line.
The numbers are used to name the forumlas.
Newly introduced formulas have their number enclosed within curly braces. And those formulas which were there in a parent goal itself have their number surrounded by square brackets.