Proof-Carrying Code

Contents

• Dependencies
• Using Touchstone
• Important Directories
• References

See also: the Touchstone compiler page, the Proof-Carrying Code page, George Necula's home page, and the Touchstone online demo (more pointers are listed below).

Dependencies

This release of Touchstone works only on Alphas running Digital Unix V3.2 or V4.0. In addition to software that comes with Digital Unix (such as the assembler and linker), you'll need the following: GNU make, gcc, perl5 (installed as /usr/local/bin/perl5), m4, and SML/NJ version 110.

Using Touchstone

First, you need to download and unpack the Touchstone sources. These can be found at ftp.cs.cmu.edu. We'll use $ROOT to refer to the top-level Touchstone directory (containing subdirs pcc, cc, and prover).

Set the following environment variables (CCOMP and PCC should be absolute paths):

• CCOMP=$ROOT/cc
• PCC=$ROOT/pcc
• ARCHOS=_ALPHA_OSF

Before you can use Touchstone for the first time, you have to run GNU make in $ROOT/pcc. This builds the programs engine and transl_elf and puts them in $ROOT/pcc/Bin.

Touchstone includes a driver program that knows all the steps necessary to compile a Touchstone C program into proof-carrying code. This driver is the ML function Main.compile. Each time you want to use Touchstone, you need to:

• Set the environment variables CCOMP, PCC, and ARCHOS, as above.
• cd to $ROOT/cc
• Invoke SML/NJ with the Compilation Manager. Depending on how SML/NJ was installed on your system, this will be either sml or sml-cm.
• At the SML/NJ prompt, type CM.make ();.
• At the SML/NJ prompt, type something like
  Main.compile "test/bcopy.cc"; The path handed to Main.compile is relative to the CCOMP environment variable.

Here's a short description of some of the important directories in this release:

pcc/cc/src

ML source for an optimizing, certifying compiler for a type-safe subset of C

pcc/prover/src

ML source for a theorem prover

pcc/pcc/Src

C source for:

transl_elf

translates a fully explicit Elf signature into a binary (represented as Alpha assembler input).

engine

Both the VCGen and proof checker for Touchstone. Works with the binary for predicates and proofs, stored in COFF files.

pcc/pcc/Exper/LF

LF logic and axioms for Touchstone's safety policy.

pcc/cc/test

Test code and benchmarks (*.cc) written in Touchstone C. A few of the Touchstone programs include C driver programs (named *.main.c). The Touchstone compiler's log file is stored here (out).

cc/pccout

Temporary files and output produced by Main.compile go here.

pcc/Bin

Contains perl scripts and binaries used during Main.compile.

• George Necula's thesis deals with PCC and Touchstone:
  

  Compiling with Proofs George C. Necula.
  CMU-CS-98-154

  A few related papers are listed at the Fox Project Publications page.
• The Fox Project home page.
• Frank Pfenning's Logical Frameworks page.