Programatica Tools

Directory tools/evman

The README file is displayed below the directory index.

Name	Last modified	Size
Parent Directory		-
Makefile	2005-10-11 01:09	1.9K
cert.sh	2005-03-22 23:08	6.5K
functions.sh	2006-05-24 00:27	3.3K
icons/	2004-09-01 23:49	-
install.sh	2003-07-16 00:12	182
servers/	2006-02-08 08:01	-
validation.sh	2005-01-20 23:15	1.2K

What is in this directory (evman)

This directory contains files relating to evidence (certificate) management, in particular the command line tool cert and the implementation of the certificate servers.

The code for certificate managment provided here is mostly inteded to serve as glue between the main Programatica tools (pfe) and external tools, such as theorem provers, and is implemented as shell scripts (but perhaps it would be better to do all of this in Haskell...).

Files

cert.sh: This is the main command-line based certificate management tool. It is also used from pfebrowser, so interaction with the user has to be designed so that it works both from the command line and in the GUI provided by pfebrowser.
Some generic certificate management functionality is implemented directly in cert.sh, while certificate type specific work is delegated to scripts in the servers subdirectory. At present, two functions are delegated: new to create new certificate and validate to validate certificates.
functions.sh, validation.sh: Auxiliary shell functions used by many of the certificate management scripts.
Makefile: Guess what...

Subdirectories

icons: A collection of certificate icons provided by Mark P. Jones.
servers: This directory contains implementation of servers for specific certificate types, with one subdirectory per server.

Certificate server implementation

The following is required for each certificate server (some of these things might be created automatically, using the Makefile):

Certificate type description file: server.attr (more details are given below),
Certificate icons: invalid.gif, unknown.gif, valid.gif,
The program new for creating new certificates, invoked from cert.sh,
The program validate for validating certificates, invoked from cert.sh.

The existing servers have new and validate programs that are implemented as fairly short shell scripts. An easy way to create a new server is to copy and modify an existing one. When common patterns emerge, functions can be moved to the funtions.sh or validation.sh files.

There is no requirement that the programs new and validate are implemented as shell scripts. All that is required is that the files are executable and behave as expected.

Certificate files maintained by certificate servers

Certificate servers are expected to create and maintain a number of files for each certificate:

File	What it is used for
`cert.attrs`	This file holds various certificate attributes. Attribute files and certificate attributes are described in more detail below.
`valid` `invalid`	These files are datestamps to indicate when the certificate was last marked valid or invalid. This helps tools quickly determine if a certificate is valid, invalid or if a more thorough test is needed to determine its status.
`deps`	This file records a signature of the parts of the source code that the certified assertion depends on. It can be generated with the command `pfe tasig M.A >.../deps` It allows tools to tell the difference between source code changes that affect the validity of an assertion from irrelevant changes, so that needless revalidation can be avoided. It also allows the `I_say_so` certificate server to use the command `pfe tadiff ...` to present a list of relevant changes to the user.
`srclist.txt`	This file caches the list of source files containing code that the certified assertion depends on. Together with the `valid` and `invalid` datestamp files, it is often possible to determine the validity of a certificate just by consulting the last modification date of files. It is used by the command `cert ls`.
`output.txt`	This is the standard place for diagnostic output from the certificate server. The user can consult this, for example to find out why certificate validation failed.

Attribute files

Both servers and the certificates they create are described by a set of attributes that are stored in attribute files. There are both Haskell functions and shell script functions to parse attribute files.

Attribute file format

Attribute files use a textual file format for association lists. Each line in an attribute file may specify a binding of a tag string to a value string using a single colon to separate the two. If the colon is omitted, then a value of "" is assumed. Leading whitespace at the beginning of each line and preceding the value (i.e., after the first, if any, colon) is ignored. Lines containing only whitespace, or in which the first non-whitespace character is a '#' are treated as comments. (Despite this, we do not intend attribute files to be a human-readable format under normal circumstances.)

Here is a sample attribute file:

 # This is a comment
 
 foo: your name here!
 date:today
 
 # here is a line with no value ...
 set filec
 
 foo:bar
 # if the same tag is used more than once, then
 # we simply get multiple attribute values with
 # the same tag.

Server attributes

Certificate server attributes are stored in a file called server.attr in the server's directory. For an example, see servers/Alfa/server.attr

The tools currently assumes the following attributes to be present:

Attribute name	Attribute meaning
`name`	The name of the server
`description`	A one-line explanation of what kind of certificates the server creates.
`attribute`	Certificate attribute description. This can be given any number of times to describe what user editable attributes are present in certificates created by this server. (These have a specific syntax that should be documented in more detail!)

Additional fields can be present.

Certificate attributes

Certificate attributes are (to some extent) defined by the different certificate servers. However, some attributes are expected to have the same meaning in all certificates:

Attribute name	Attribute meaning
`type`	The name of the server that created the certificate.
`conc`	Conclusion. This is the name of the assertion that the certificate serves as evidence for. It should be an unqualified assertion identifer. (This is not meaningful in all certificate types.)
`hyp`	Hypotheses. This is either `..` or a list of qualified identifiers. A more detailed description is given below.
`file` `file/type`	Names of auxiliary files used to establish the validity of the certificate. For example, for Alfa certificates, the name of the file containing the proof is recorded in the attribute `file/proof`.

Additional fields can be present.

Hypotheses

For certificates that certify a sequent hyp|-conc, the hyp has the following forms:

.., which means that the validity of the certificate can depend on everything referenced (directly or indirectly) from the assertion named in the conc attribute.
A list of qualified identifiers. Each identifier in the list should denote either an assertion or a value.
- For assertion names, the hypothesis is that the named assertion is valid.
- For value names, the validity of the certificate can depend on the definition of that name.
Definitions of names that are free in the assertion, or in definitions of explicitly listed names, do not influence the validity of the assertion. (In effect, free names are implicitly universally quantified.)

Authors: various

Contact: Thomas Hallgren