VOLPIC: A verification pipeline for Pascal

Announcements
1

Today I released the source for VOLPIC, a verification pipeline I’ve been developing for the Pascal programming language: GitHub - CharlesAverill/volpic: Verifier of Lifted Pascal in Coq

logo_black
logo_black1080×602 99 KB

VOLPIC parses log files from the Free Pascal Compiler to obtain a structured, compiler-checked representation of a program, converts that structure to an AST representing Gallina code, and generates a Coq file containing function definitions ready for verification.

flowchart-2-1
flowchart-2-13076×2072 275 KB

VOLPIC is still in alpha, so

  • There are a ton of bugs in the lifter
  • Lots of array operations are still broken due to dependent typing shenanigans
  • Lots of Pascal language features are not yet supported
  • I haven’t yet built strong enough automation tools or sufficient theorems to aid in verifying non-trivial code yet

Despite the shortcomings, I’m very proud of how far I’ve taken the project working solo as a freshly-graduated undergraduate student. I’m looking forward to adding support for more language features, replacing my string-manipulation generator with a generator that hooks into the Coq API, writing more lemmas to enable verification, and getting some sample proofs written out. Please let me know what you think!

Here’s a presentation I gave over a broad overview of the project

1 Like
2

This announce piqued my curiosity. The presentation still leaves me wanting for more information. Could you include in the presentation the code for the linear search and the produced Coq code? And then maybe the statement you prove about it?

Right now, if I want to see this produced code, I need to run your tool, and I don’t know how much time that would take (installing, reading the documentations, and so forth).

3

Hi! All of my examples are in the theories/ directory in the repo, here’s the link to the closest-to-working lifted linear search (manually modified to compile): volpic/theories/algos/algorithms_modified.v at main · CharlesAverill/volpic · GitHub. Here’s the code it was generated from: volpic/theories/algos/algorithms.pas at main · CharlesAverill/volpic · GitHub. And here’s the code that was automatically lifted from it: volpic/theories/algos/algorithms.v at main · CharlesAverill/volpic · GitHub. The first file contains this prop that I aim to prove for linear_search:


Inductive list_search {A : Type} : list A -> A -> nat -> Prop :=
  | sc_hd : forall (x : A) (xs : list A),
      list_search (x :: xs) x 0
  | sc_tl : forall (x y : A) (xs : list A) (n : nat),
      list_search xs x n -> list_search (y :: xs) x (S n).

Definition vector_search_correct {T : Type} {n : nat} (vec : vector T n) :=
	list_search (Vector.to_list vec).

I’m sad to say that my live demo for this presentation died a few hours before I was set to present and I’m still trying to figure out why. The linked file above has been manually modified by me, but I’ll soon be implementing those modifications in the lifter to robust-ify the array access code. The linear search extracted from that function runs but doesn’t produce the right answer, the current theory is that a bug in the subscripting or loop boundary generation is breaking semantic equivalence.

In terms of running the code, it would be a fair amount of time and effort at the moment. You’d have to build a custom version of FPC, which takes a while on the first compile. Other than that it’s a fairly simple setup, no other dependencies.

I’ll likely post on here again when I have a more substantial proof of concept, I’ve been working towards lifting sorts and searches for the past ~1 week. Current problems with generation are

  • Retrieving from a list with a dependent type seems impossible or not automatible (although I think if I rework function arguments this can be fixed)
  • There’s a bug that’s popped up frequently in which a series of let … := … in statements does not end with an updated store (I believe the binary_search in the linked file above still has that issue)
  • Array writes seem very difficult, also due to dependent typing

I’m hoping to get some guidance from a mentor in the upcoming week to set me on the right path for fixing these issues, and suggestions are always welcome. Thank you for your interest!