[Why3-club] Generating Coq with Why3 into separate files

Stefan Berghofer berghofe at in.tum.de
Thu Mar 13 14:43:56 CET 2014


On 03/07/2014 02:21 PM, Julien Thierry wrote:
> Dear Why3-Club,
>
> In the case of generation to manual prover like Coq from a WhyML file, we
> would like to separate the part generated by Why3 and the part that should
> be edited into different files as is already the case for Isabelle.
>
> One possible model could be having three files:
> - one generated containing a proposition corresponding to a Why3 goal (and
> axioms)
> - one manually editable to prove the proposition (which wont be generated
> if already existing)
> - one generated to verify that the proof file actually proves the right
> predicate
>
> I'm joining file corresponding to a simple example to illustrate the model:
> test.v contains the predicate, proof_test.v the proof manually editable and
> check_proof_test.v the verification.
>
> The question is, would that be a viable model? Is there a better way to
> split the goal and the proof into different files?
>
> Best regards,

Hi Julien,

what you describe is quite similar to the approach used in the first version of
the link between the "old" SPARK tools and Isabelle, which was based on the Victor
tool due to Paul Jackson (http://homepages.inf.ed.ac.uk/pbj/spark/victor.html).
For each SPARK *.vcg (or *.siv) file, the tool generated two Isabelle theory files
called ..._Declaration.thy and ..._Obligation.thy. The first of these files contains
declarations of functions used in the VCs, whereas the second contains lemma statements
with trivial proofs that check that the user has indeed proved the right VCs. In addition,
there are two user-editable files, one called ..._Specification.thy containing definitions
of SPARK proof functions (similar to ghost functions in SPARK 2014), and another one called
..._User.thy containing the actual proofs of the VCs. A verification of the RIPEMD-160 hash
function using this approach (due to Fabian Immler) can be found in the Archive of Formal
Proofs:

   http://afp.sourceforge.net/entries/RIPEMD-160-SPARK.shtml

For example, the four types of files corresponding to the VCs for the Round function of
RIPEMD-160 can be found at

   http://afp.sourceforge.net/browser_info/current/AFP/RIPEMD-160-SPARK/Round_Declaration.html
   http://afp.sourceforge.net/browser_info/current/AFP/RIPEMD-160-SPARK/Round_Specification.html
   http://afp.sourceforge.net/browser_info/current/AFP/RIPEMD-160-SPARK/Round_User.html
   http://afp.sourceforge.net/browser_info/current/AFP/RIPEMD-160-SPARK/Round_Obligation.html

I cannot say much about the viability of this approach, because we soon abandoned it in
favour of a specific plugin for Isabelle that could directly read the *.vcg and *.siv files
generated by the SPARK tools, therefore avoiding the detour via an additional tool.
A verification of RIPEMD-160 using this newer approach can be found in the Isabelle
distribution at

   http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/SPARK/Examples/RIPEMD-160

The new link between Isabelle and Why3 is very similar to the link between Isabelle and the
old SPARK tools. The Why3 part of the link produces a file containing a description of the
proof obligations in a format that is both easy to parse and generate (i.e. XML). On the
Isabelle side, there is again a plugin extending Isabelle with a number of theory commands
such as why3_open, why3_vc and why3_end for loading a generated *.xml file with proof obligations,
proving a particular proof obligation, and closing the verification environment, respectively.
Although it may be some extra work to write a plugin for your target prover, this approach
gives you a greater degree of flexibility and also more control over what is happening.
For example, the why3_vc command enforces that the user proves the right VC, and the why3_end
command checks that all open VCs have been proved. Moreover, this approach also simplifies
things for the user, because there is no need to juggle different types of files.

Would writing a Coq plugin using a similar approach be an option for you as well? While this
plugin was relatively straightforward to write for Isabelle, it may be more complicated for
Coq, since the Coq driver contains some extra quirks such as proofs that all Why3 types are
inhabited.

I doubt that the Why3 infrastructure for writing drivers for external provers currently supports
the generation of more than one file for a particular task. The outputs of the fprintf commands in
the printers all end up in the same file, and also the Why3 session description file why3session.xml
only seems to be able to keep track of one file for each goal and prover. To circumvent this problem,
I provided an additional wrapper script that is called by Why3 with the name of a generated *.xml
file as an argument, and then calls Isabelle with the corresponding *.thy file. If the *.thy file
does not yet exist, the wrapper script generates a stub *.thy file containing the names of the proof
obligations extracted from the *.xml file. Unfortunately, there are still some issues with this
approach. Why3 is only aware of the existence of the *.xml files but not of the *.thy files. As
a consequence, Why3 issues an error message when the *.xml files are not present, even though they
could be generated and the only important files for replaying the proof are the *.thy files. This
is why the *.xml files for the examples involving Isabelle are currently part of the Why3 repository
as well, see e.g.

   https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=why3/why3.git;a=commitdiff;h=ac1ef3c2c1b06980a681e2f287ca80ce86207c6c

I am not completely happy with this situation, since generated files should usually not be under
revision control.

Disclaimer: I am not an expert on the internals of Why3, so take the above with a grain of salt.
Maybe someone from the Why3 development team can comment on it.

Greetings,
Stefan



More information about the Why3-club mailing list