The Erlang-Coq Synthesizer Tool (ECS)

The Erlang-Coq Synthesizer Tool (ECS) is a framework for certified extraction of Erlang Code. Its theory is described in this paper. Basically, we formalized a monadic type theory in Coq (Calculus of (Inductive) Constructions) and used the extraction mechanism to extract Haskell programs by stating and proving Coq lemmas and theorems. Haskell is not well-suited to distributed computations so we provided an additional Haskell-Erlang Compiler (HEC) to make the code distributed.

In this page we provide the instructions for the use of ECS, the Coq formalization of our type theory (LambdaXD) and the HEC sources along with two working examples.

Summarizing the workflow is:

  1. Develop a formal proof in Coq
  2. Extract the Haskell source from a proof
  3. Compile from Haskell to Erlang using the hec compiler
  4. In the resulting Erlang code, add the main function
  5. Prepare running environment
  6. Run!

Building and Setting up ECS

Download the whole archive ECS-0.1.
This archive contains the following packages:

  • Compiler
  • LambdaXD

and the working examples

  • rpc
  • update

HEC is built over the BNF Compiler (BNFC) and Haskell, but you will
need Coq and Erlang infrastructure in order run the final code

Once set up the environment:

  • unzip the package
  • enter the directory
  • launch “make” from the command line.

You should have now a Perl script named “hec” which uses the binaries just built.

Using HEC

In Erlang, the name of the file without extensions, for example, <name>.erl, must be the same of the name of the module specified inside the source code with “-module” Erlang directive. We suggest reading the Erlang reference manual for further details.

Here’s the syntax for using HEC:

./hec [-debug] -module <module> <input-file> <output-file>

where, the <input-file> is the Haskell source file produced by Coq, the <module> is the name of the Erlang module to produce which usually is the same of the <output-file> which could be anyone you want, but it is important that it has the “erl” extension.

Using ECS

Once you have stated and proved your lemma you have to use the “Recursive Extraction &lt;lemma&gt;” command provided by Coq in order to get the Haskell code. (See Coq documentation about Extraction).

The Coq source file, from now on <your_file>.v, should use our library by loading the Proofs.v file, which is inside LambdaXD, e.g it should have a line “Load ‘Proofs'”. So, you have to tell the coqc command where the LambdaXD directory is, e.g.:

coqc -I <LambdaXD_DIR> <your_file>.v

Now the Coq compiler will produce the output which can be redirected to the Haskell file like this:

coqc -I <LambdaXD_DIR> <your_file>.v > <your_file>hs

The Haskell file has to be compiled into Erlang; this is done by using the HEC compiler previously built:

./hec -module <your_file> <your_file>.hs <your_file>.erl

Now, we have the Erlang file. However, Erlang code is not ready to be run yet. Often, functions are generated with open variables, so you will need to provide a main() function that uses them by hand.

Example: Remote Procedure Call (RPC)

In the “rpc” directory there is the rpc.v which comes with a Makefile. The Makefile needs the compiler and the coq library path, so the syntax is the following:

make LAMXD_PATH='<lambdaXD_path>' COMPILER_PATH='<compiler_path>'

Now the rpc2.erl file should have been produced.

In order to run it you need to implement the main() function (a functions which uses the rpc auto generated function); as an example, we choose this implementation:

foo(N)-> N+1.

main() -> rpc({disp,’disp@′}, {exec, ‘exec@’}, fun foo/1, 1000).

where the first two parameters are the references to the remote hosts. We now have to run the Erlang environment in this to worlds:

dispatcher# erl -name 'disp@'

executer# erl -name ‘exec@’

Notice, this commands have to be typed in two different shells. Now run the code:

# erl -name 'local@'
(client2@> c(rpc2).
./rpc2.erl:25: Warning: variable 'Mod' is unused

Execute the main function:

(client2@> rpc2:main().
Dispatcher: spawning function on Target {exec,'exec@'}
Executer: sending result to {,'client2@'}

You can see the function foo/1 has been moved to the remote world and have computed the result, which is 1001.

Example: remote Update and remote Read

In the update directory there is the specification and proof of two functions whose the specification says:

“the first function produces, if not already existing, a reference to a remote location and puts a value inside it using a mobile computation, the second function takes the remote reference, reads the value by doing an rpc call and returns back the previously written value.”

As before, run “make” to translate the update.v into an Erlang update.erl file. Now we choosed the following implementation for main():

main() -> X = update({disp, 'disp@'}, {exec,'exec@'}, 1000, 1234),
ref = element(2,X),
remoteread = element(3,X),

The update function is in fact a function which returns a pair of two computations, the first is the remote write function, the second is the remote read. The remote read gets the remote location where to write from the remote write.

The implementation suggest to take the Pid (representing remote memory cell) and to pass as parameter to the remote read, which takes it and return back the value.

Below there is the expected output:

# erl -name 'client2@'
Erlang R14B03 (erts-5.8.4) [source] [64-bit] [smp:4:4] [rq:4] [async-threads:0] [hipe] [kernel-poll:false]

Eshell V5.8.4 (abort with ^G)
(client2@> c(update).
./update.erl:34: Warning: variable 'Index' is unused
./update.erl:48: Warning: variable 'Mod' is unused
(client2@> update:main().
Dispatcher: spawning function on Target {exec,'exec@'}
Executer: sending result to {,'client2@'}
Dispatcher: spawning function on Target {exec,'exec@'}
Get!Executer: sending result to {,'client2@'}