SURVEY:SUMMARY:BUILD_DIFFICULTY[not_applicable, reasonable_effort, code_problematic or string] not_applicable
SURVEY:SUMMARY:CLASSIFICATION[practical,theoretical,hardware] practical
SURVEY:SUMMARY:CORRECT_CODE_LOCATION[string] The build notes report on two attempts to build EasyCrypt 1.0, the second one successful.A first remark is that the paper is not about EasyCrypt, but about a formal proof that should be checked using EasyCrypt. (EasyCrypt itself is presented in an older paper published at CRYPTO 2011.) Thus, inorder to reproduce the paper results one would need to first build EasyCrypt and then run it to check the formal proof.The paper introduction indicates that the infrastructure needed to check this proof is available on request:  "The EasyCrypt input file corresponding to the proof presented in Section 4 appears in an extended version [7]; all the infrastructure needed to machine-check this proof is available on request."Both build attempts used code found in the EasyCrypt website. Unfortunately, from the build notes I infer that the code downloaded is that of a pre-release of EasyCrypt version 1.0, rather than version 0.2, which is the one that must be used to check the proof in the paper. This code is also available from the same website at   http://old.easycrypt.info/easycrypt-0.2.tgz(As a side remark, it would be better if the field TOOL:DATA_LINK showed the exact location from which the code was downloaded, not just the webpage where it was found.)
SURVEY:SUMMARY:PUBLISHED_CODE[not_applicable, yes, no] yes
SURVEY:SUMMARY:SAME_VERSION[not_applicable, yes, no_but_available, no_and_not_available] yes
SURVEY:SUMMARY:STUDY_FOUND_CORRECT_CODE[not_applicable, yes, no] no
SURVEY:AUTHOR1:BUILD_COMMENT[string] 
SURVEY:AUTHOR1:BUILD_DIFFICULTY[not_applicable, reasonable_effort, code_problematic or string] not_applicable
SURVEY:AUTHOR1:BUILD_DIFFICULTY_COMMENT[string] none
SURVEY:AUTHOR1:CLASSIFICATION[practical,theoretical,hardware] practical
SURVEY:AUTHOR1:CLASSIFICATION_COMMENT[string] 
SURVEY:AUTHOR1:CORRECT_CODE_LOCATION[string] The build notes report on two attempts to build EasyCrypt 1.0, the second one successful.A first remark is that the paper is not about EasyCrypt, but about a formal proof that should be checked using EasyCrypt. (EasyCrypt itself is presented in an older paper published at CRYPTO 2011.) Thus, inorder to reproduce the paper results one would need to first build EasyCrypt and then run it to check the formal proof.The paper introduction indicates that the infrastructure needed to check this proof is available on request:  "The EasyCrypt input file corresponding to the proof presented in Section 4 appears in an extended version [7]; all the infrastructure needed to machine-check this proof is available on request."Both build attempts used code found in the EasyCrypt website. Unfortunately, from the build notes I infer that the code downloaded is that of a pre-release of EasyCrypt version 1.0, rather than version 0.2, which is the one that must be used to check the proof in the paper. This code is also available from the same website at   http://old.easycrypt.info/easycrypt-0.2.tgz(As a side remark, it would be better if the field TOOL:DATA_LINK showed the exact location from which the code was downloaded, not just the webpage where it was found.)
SURVEY:AUTHOR1:PUBLIC_COMMENT[string] The paper reports on a machine-checkable proof. The introduction indicates that the infrastructure needed to check this proof is available on request:    "The EasyCrypt input file corresponding to the proof presented in    Section 4 appears in an extended version [7]; all the    infrastructure needed to machine-check this proof is available on    request."  At no point the authors were contacted; rather, as shown in the build notes, the analysts obtained the code from a link found on Google (http://www.easycrypt.info/#download). A glance at the notes shows that the code downloaded is that of a candidate release of EasyCrypt (v1.0), rather than the version used in the paper (v0.2). So, the outcome of the evaluation, although successful, could not possibly be a measure of the reproducibility of the paper's results.  Should the analysts have contacted the authors (or should they have downloaded the right version of EasyCrypt), they would have been able to reproduce the paper's results without significant effort. To sustain this claim, we give detailed instructions on how to get and build EasyCrypt v0.2, and check the proof on Debian 7.6 (the latest stable release). The whole process could be completed in under 5 minutes and does not require any particular skill besides identifying the Debian packages corresponding to external dependencies (listed in the README file).  1) Install external dependencies    sudo apt-get install ocaml libocamlgraph-ocaml-dev alt-ergo cvc3  2) Get EasyCrypt 0.2   wget http://old.easycrypt.info/easycrypt-0.2.tgz  tar zxf easycrypt-0.2.tgz  3) Build and install Why3 and EasyCrypt (following instructions in the README file)   cd easycrypt-0.2/why3-0.71/  ./configure-disable-ide  make  sudo make install  make byte  sudo make install-lib  why3config-detect  cd ..  ./configure  make  sudo make install  4) Check the proof reported on the paper   ./easycrypt examples/ZAEP.ec
SURVEY:AUTHOR1:PUBLISHED_CODE[not_applicable, yes, no] yes
SURVEY:AUTHOR1:SAME_VERSION[not_applicable, yes, no_but_available, no_and_not_available] yes
SURVEY:AUTHOR1:SAME_VERSION_COMMENT[string] 
SURVEY:AUTHOR1:STUDY_FOUND_CORRECT_CODE[not_applicable, yes, no] no