1. REQUIREMENTS
===============

We only list the versions of required software that are known to
work. Note that EasyCrypt may still compile and work as expected using
versions of packages other than those listed.

To compile EasyCrypt and run the examples you will need:

* GNU Automake

* GNU Make 3.81

  Available at http://www.gnu.org/software/make/
  Version 3.82 will most probably work

* Objective Caml >= 3.11
 
  Available at http://caml.inria.fr/download.en.html
  Older versions >= 3.08 will most probably work

* Why3 0.71
 
  Install the version provided in the repository at trunk/why3-0.71
  Patched from the version available at http://why3.lri.fr/

* CVC3 2.4.1

  Available at http://www.cs.nyu.edu/acsys/cvc3/

* Alt-Ergo 0.94
 
  Available at http://alt-ergo.lri.fr/

The following automated theorem provers are supported by EasyCrypt,
but are not needed to reproduce the case studies:

* Z3 

  Available at
  http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html

* Simplify

  Pre-compiled binaries for various architectures are available at
  http://krakatoa.lri.fr/ws/Simplify-1.5.5-13-06-07-binary.zip 

* Yices

  Available at http://yices.csl.sri.com/

* Eprover

  Available at http://www4.informatik.tu-muenchen.de/~schulz/E/

* Vampire

  Available at http://www.vprover.org/

To install the ProofGeneral front-end for EasyCrypt you will
additionally need:

* GNU Emacs 23.2
 
  Available at http://www.gnu.org/software/emacs/

* ProofGeneral 4.1

  Available at http://proofgeneral.inf.ed.ac.uk/


2. INSTALLING WHY
=================

To compile EasyCrypt you need to install the byte-compiled version of
the Why3 library. Follow first the standard installation instructions 
in the corresponding Why3 README file. If you do not plan to use
Why3 as a standalone tool it is recommended to invoke the Why3 configure
script with the --disable-ide option to avoid unnecessary library 
dependences:
  ./configure --disable-ide
  make
  make install

After installing Why3 from source code, you must type

 make byte
 make install-lib

to install the library.

Once you have installed Why3 and the automated provers of your choice,
please make sure that Why is correctly configured to use the provers
by running the command

 why3config --detect

If everything is correct, you should see a table detailing the provers
that Why3 detected---you can safely ignore any "not know to be
supported" warnings. Remember that you need at least CVC3 and Alt-Ergo
to reproduce the case studies.


3. COMPILATION
==============

When the contents of the package were extracted, you should have ended
up with a directory containing this README file and a sub-directory
"easycrypt". ("easycrypt/trunk" when installing from the SVN repository). 

To compile EasyCrypt, simply change to the sub-directory "easycrypt" and type
 
 ./configure --with-proof-general=PATH_TO_PROOFGENERAL

The argument above is optional but recommended. For a list of additional 
options type

 ./configure --help

Then type

 make

and then 

 make install
 
with the appropriate access permissions.

If everything goes well, a binary named "easycrypt.top" will be
generated. To test the setup you may then run

 make test

and verify that all tests pass.


4. RUNNING THE EXAMPLES
=======================

Several examples are available under the directory
"easycrypt/examples". To compile them from the directory "easycrypt",
simply type

 ./easycrypt examples/elgamal.ec
 ./easycrypt examples/helgamal.ec
 ./easycrypt examples/fdh.ec


5. INSTALLING THE PROOFGENERAL FRONT-END
========================================

5.1. ProofGeneral - Requirements
--------------------------------

* Proof general >=  4.1

  Available at http://proofgeneral.inf.ed.ac.uk/download

* CertiCrypt


5.2. ProofGeneral - Manual Installation
---------------------------------------

Add the following line to <proof-general-home>/generic/proof-site.el
in the definition of `proof-assistant-table-default':

   (certicrypt "CertiCrypt" "ec" nil (".v" ".vo" ".glob" ".ml"))

Copy the directory "certicrypt" and its contents to the directory
where ProofGeneral was installed, typically

   /usr/local/share/emacs/site-elisp/ProofGeneral/

and check that the final directory has the appropriate access permissions.

5.3. ProofGeneral - Automatic Installation
------------------------------------------

The provided Makefile will install everything in default
locations (or the location specified to the ./configure script). Simply type

   make install_proofgeneral

or 

   sudo make install_proofgeneral

as appropriate.


5.4. ProofGeneral - Configuration
---------------------------------

Add the following line to your emacs configuration file (typically ~/.emacs):

 (load-file "/usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el")


Set the path to the EasyCrypt executable and the prelude file in your
Emacs configuration. This can be achieved either by modifying the
variable certicrypt-prog-name inside Emacs:

 Proof-General
   -> Advanced 
     -> Customize 
       -> Certicrypt 
         -> CertiCrypt prog name

You should set its value to (modifying paths as appropriate):

 "<path-to-easycrypt>/easycrypt -emacs -prelude <path-to-prelude>/easycrypt_base.ec"

The prelude file "easycrypt-base.ec" can be found at "easycrypt/src/".

Alternatively, you can modify your Emacs local configuration file
(typically ~/.emacs):

 (custom-set-variables
 ...
  '(certicrypt-prog-name 
    "<path-to-easycrypt>/easycrypt -emacs
        			   -prelude <path-to-prelude>/easycrypt_base.ec)
 ...)


