docs/verification.rst - 3p/nicta/cogent - Git at Google

 Verification
 ============

 .. highlight:: sh

 A compiled Cogent program produces many Isabelle/HOL theory files to assist in verification.

 Dependencies
 ------------

 Compiled Cogent theory files have several dependencies:

 * `Isabelle/HOL 2019`_, the proof assistant used for generated theory files (.thy)
 * AutoCorres_, an Isabelle/HOL tool to extract C code into an Isabelle/HOL embedding
 * `Cogent theories`_, included in the Cogent repository
 * `C refinement theories`_, included in the Cogent repository

 Cogent theories and C refinement theories are properly linked to compiled files using the
 ``--root-dir=PATH`` compiler flag, which should specify the root directory of the
 `Cogent repository`_.

 Generated Theory Files
 ----------------------

 Compiling a program with the ``-A`` flag produces all needed verification files (among with other
 output files). You can
 optionally generate each individual file using it's relevant flag. The files are:

 TypeProof
     A proof of type correctness for the compiled program, generated with ``--typeproof``.
 ShallowShared
     The shared components of the shallow embedding, generated with either ``--shallow-desugar`` or
     ``--shallow-normal``.
 Shallow_Desugar
     The compiled shallow embedding from the desugared compiler code, generated with ``--shallow-desugar``.
 Shallow_Normal
     The compiled shallow embedding in normal form, generated with ``--shallow-normal``.
 ShallowShared_Tuples, Shallow_Desugar_Tuples
     Shallow embedding files that feature tuples instead of records, generated with ``--shallow-desugar-tuples``.
 SCorres_Normal
     Various value relations for each type from the compiled Cogent program, generated with ``--scorres-normal``. Can also come in desugared and monomorphised form.
 Deep_Normal
     The deep embedding for the compiled file, in normal form, generated with ``--deep-normal``. Can also come in desugared and monomorphised form.
 NormalProof
     The proof that the compiled shallow embedding is in normal form, generated with ``--normal-proof``.
 ACInstall
     Creates a shallow embedding of the generated C code via AutoCorres_, generated with ``--ac-install``.
 CorresSetup
     Various lemmas needed for the correspondence proof, generated with ``--corres-setup``.
 CorresProof
     Creates the correspondence proof between the Cogent deep embedding and the C shallow embedding, generated with ``--corres-proof``.
 MonoProof
     Proving the equivalence of polymorphic functions and specialised monomorphic functions, generated with ``--mono-proof``.
 AllRefine
     The final proof that shows the generated C code is a refinement of the generated shallow embedding, generated with ``--all-refine``.

 The generated files depend on each other in a hierarchy, depicted below:

 .. graphviz:: assets/dependencies.dot

 In addition to the theory files, a ``ROOT`` file is produced for building the
 files. You can reproduce this file by running the compiler with the ``--root``
 flag.

 Building/Running The Generated Files
 ------------------------------------

 Before using the generated theory files, ensure you have built the AutoCorres heap like so::

     L4V_ARCH=X64 isabelle build -v -b -d $AC_DIR AutoCorres

 Where ``$AC_DIR`` is the root directory of AutoCorres.

 In Jedit
 ^^^^^^^^

 Launch the Jedit editor with the following command::

     L4V_ARCH=X64 isabelle jedit -d $AC_DIR -l AutoCorres

 Where again, ``$AC_DIR`` is the root directory of AutoCorres.

 Then, simply open any file you wish to view.

 On the command line
 ^^^^^^^^^^^^^^^^^^^

 Using the generated ``ROOT`` file, you can build the suite of files like so::

     isabelle build -D $GENERATED_FILES_DIR \
                    -d $REPO_ROOT/cogent/isa \
                    -d $AC_DIR

 This will:

 * Select the root file located in the directory specified by ``$GENERATED_FILES_DIR``
   and evaluate it, which is the directory where your ``ROOT`` file and generated
   theory files are located;
 * Include the Cogent theory files in ``$REPO_ROOT/cogent/isa``, where ``$REPO_ROOT``
   is the root directory of the Cogent repository;
 * Include AutoCorres theories located in ``$AC_DIR``.

 Examples
 --------

 A Simple Example
 ^^^^^^^^^^^^^^^^

 In this example, we're going to write a function that squares a ``U64``, and prove
 the correctness of the embedding in Isabelle/HOL.

 You can find all the code for this example in our `repository <https://github.com/NICTA/cogent/tree/master/cogent/examples/square>`_

 We'll use the following Cogent code:

 .. literalinclude:: ../cogent/examples/square/square.cogent
     :language: haskell

 And we'll build a shallow embedding using the following command:

 .. code-block:: bash

     cogent square.cogent -g -o square\
         --root-dir="../../.." \
         --shallow-normal \
         --entry-funcs=entrypoints.cfg

 which gives us the following shallow embedding:

 .. code-block:: isabelle

     (*
       This file is generated by Cogent
     *)

     theory Square_Shallow_Normal
     imports "Square_ShallowShared"
     begin

     definition
         square :: "64 word ⇒ 64 word"
     where
         "square x__ds_var_0 ≡ HOL.Let x__ds_var_0 (λx. (*) x x)"

     end

 Next, we'll create a file and import our shallow embedding, then prove its
 correctness against the specification of square in Isabelle/HOL:

 .. literalinclude:: ../cogent/examples/square/SquareProof.thy
     :language: isabelle


 A More Involved Example
 ^^^^^^^^^^^^^^^^^^^^^^^

 The code for this example is more involved than the previous, so follow along with the source located
 `here <https://github.com/NICTA/cogent/tree/master/cogent/examples/system-abstract-verif>`_.

 Naturally when writing Cogent code, you'll interface with C code frequently. This C code must go through AutoCorres for
 the refinement proof, so we'll need to put a bit more effort to set up the verification chain for such Cogent programs.

 This time, we'll be using abstract functions and types to represent the C functions and types we wish to call and use.
 Our program will take in a toy ``KernelState`` type, and check the status of a magic number in an object of this type. If the number
 has been corrupted, we'll cause a kernel panic; otherwise, continue on.

 The C code this time will involve the C standard library, which we don't want to pass into AutoCorres as it often
 causes errors. In realistic situations, the same issue can potentially be caused by system code included into Cogent programs that
 may not directly be verified along with the Cogent code (such as Linux kernel headers), so we need a way to work around this.

 Note that, as we will use types from the standard library that are not implemented in our antiquoted C or Cogent code, we
 must inform the compiler of the existence of these types. We do this with the flag ``--ext-type=types.cfg`` (we have explained this flag in :ref:`first-program`), which points
 to the file in our example directory. As we'll use the file stream type, the only line in this file is ``FILE``.

 We'll write two wrapper files, each called ``wrapper.ac`` that contain different definitions of various library types and functions
 in order to work around AutoCorres. Observe the sample source code directory layout::

     .
     ├── entrypoints.cfg
     ├── Kernel.cogent
     ├── main.ac
     ├── Makefile
     ├── plat
     │   ├── system
     │   │   └── wrapper.ac
     │   └── verification
     │       └── wrapper.ac
     └── types.cfg

 You'll notice in our platform folder (``plat``), we have a ``system`` folder and a ``verification`` folder each with it's own wrapper file.

 In the system folder, the wrapper file includes the C library for execution, defines the abstract types used in the Cogent code,
 and finally includes our to be compiled Cogent code followed by the main code. You may also notice that we define two messages as
 string literals in variables (``KERNEL_PANIC_MESSAGE``, ``KERNEL_OK_MESSAGE``). AutoCorres won't accept string literals in C code,
 so it's important to abstract them out of the main code. Finally, the wrapper includes the implementations of our abstract functions
 (``kernelPanic``, ``memMagicNumer``) that our Cogent code uses, and a ``main`` function to test the Cogent code, all located in ``main.ac``.

 .. literalinclude:: ../cogent/examples/system-abstract-verif/plat/system/wrapper.ac
     :language: c

 In the ``verification`` folder however, we must provide definitions of the standard library types and functions we use
 (``FILE``, ``fprintf``, ``malloc``, ``free``, ``exit``, ``stdout``). During verification we'll treat these functions like a black box,
 so the actual implementation doesn't matter (as long as AutoCorres can parse them). For example, we can give the following
 definitions to the FILE type and fprintf:

 .. code-block:: c

     typedef struct filedummy {
         int dummy;
     } FILE;

     int fprintf(FILE * stream, char * str) {
         // do nothing
         return 0;
     }

 We can also give dummy definitions to our string literal placeholder variables at this time too:

 .. code-block:: c

     char * KERNEL_PANIC_MESSAGE = 0x0;
     char * KERNEL_OK_MESSAGE    = 0x0;

 Now AutoCorres will be happy with our code!

 To make the verification build chain simpler, in our ``Makefile`` we simply change which ``wrapper.ac`` is supplied to
 the compiler depending on whether or not we want to build for verification or to build the system to run.

 Finally, we're left with our Cogent code:

 .. literalinclude:: ../cogent/examples/system-abstract-verif/Kernel.cogent
     :language: haskell


 To run this example, run ``make system`` to compile the code into an executable called ``kernel``, or run
 ``make verification`` to build all Isabelle/HOL verification files and C code suited for AutoCorres.

 Common Errors
 -------------

 ACInstall
 ^^^^^^^^^

 .. highlight:: none

 You may see the following error from AutoCorres when running this file::

     ### In file included from file.c:3:
     ### file.h:6:10: fatal error: cogent-defns.h: No such file or directory
     ###  #include <cogent-defns.h>

 This is due to ``cpp`` being unable to find the Cogent C header, which is located in the Cogent repository
 in `cogent/lib/cogent-defns.h <https://github.com/NICTA/cogent/blob/master/cogent/lib/cogent-defns.h>`_. Adding the compiler flag ``--fake-header-dir=$REPO_ROOT/cogent/lib`` will fix this.
 You can additionally set this directory to the result of ``cogent --libgum-dir``, which will print the location of the Cogent
 standard library directory.

 You may also see the following error::

     *** Undeclared constant: "??.\<Gamma>"
     *** At command "autocorres" (line 14 of "ACInstall.thy")

 This can be due to several reasons:

 * You have not specified entrypoint functions via the compiler flag ``--entry-funcs=FILE``.
 * Your source file/entrypoiint functions contain only polymorphic functions. Concrete C functions
   will only be generated when these polymorphic functions are instantiated by your Cogent
   source file or your entrypoint file. You can do so in the entrypoint file like so: ``functionName[TypeName]`` (also see :ref:`poly-function-example` for more explanation).


 .. _AutoCorres: https://ts.data61.csiro.au/projects/TS/autocorres/
 .. _`Isabelle/HOL 2019`: https://isabelle.in.tum.de/
 .. _`Cogent theories`: https://github.com/NICTA/cogent/tree/master/cogent/isa/
 .. _`C refinement theories`: https://github.com/NICTA/cogent/tree/master/c-refinement
 .. _`Cogent repository`: https://github.com/NICTA/cogent
	Verification
	============

	.. highlight:: sh

	A compiled Cogent program produces many Isabelle/HOL theory files to assist in verification.

	Dependencies
	------------

	Compiled Cogent theory files have several dependencies:

	* `Isabelle/HOL 2019`_, the proof assistant used for generated theory files (.thy)
	* AutoCorres_, an Isabelle/HOL tool to extract C code into an Isabelle/HOL embedding
	* `Cogent theories`_, included in the Cogent repository
	* `C refinement theories`_, included in the Cogent repository

	Cogent theories and C refinement theories are properly linked to compiled files using the
	``--root-dir=PATH`` compiler flag, which should specify the root directory of the
	`Cogent repository`_.

	Generated Theory Files
	----------------------

	Compiling a program with the ``-A`` flag produces all needed verification files (among with other
	output files). You can
	optionally generate each individual file using it's relevant flag. The files are:

	TypeProof
	A proof of type correctness for the compiled program, generated with ``--typeproof``.
	ShallowShared
	The shared components of the shallow embedding, generated with either ``--shallow-desugar`` or
	``--shallow-normal``.
	Shallow_Desugar
	The compiled shallow embedding from the desugared compiler code, generated with ``--shallow-desugar``.
	Shallow_Normal
	The compiled shallow embedding in normal form, generated with ``--shallow-normal``.
	ShallowShared_Tuples, Shallow_Desugar_Tuples
	Shallow embedding files that feature tuples instead of records, generated with ``--shallow-desugar-tuples``.
	SCorres_Normal
	Various value relations for each type from the compiled Cogent program, generated with ``--scorres-normal``. Can also come in desugared and monomorphised form.
	Deep_Normal
	The deep embedding for the compiled file, in normal form, generated with ``--deep-normal``. Can also come in desugared and monomorphised form.
	NormalProof
	The proof that the compiled shallow embedding is in normal form, generated with ``--normal-proof``.
	ACInstall
	Creates a shallow embedding of the generated C code via AutoCorres_, generated with ``--ac-install``.
	CorresSetup
	Various lemmas needed for the correspondence proof, generated with ``--corres-setup``.
	CorresProof
	Creates the correspondence proof between the Cogent deep embedding and the C shallow embedding, generated with ``--corres-proof``.
	MonoProof
	Proving the equivalence of polymorphic functions and specialised monomorphic functions, generated with ``--mono-proof``.
	AllRefine
	The final proof that shows the generated C code is a refinement of the generated shallow embedding, generated with ``--all-refine``.

	The generated files depend on each other in a hierarchy, depicted below:

	.. graphviz:: assets/dependencies.dot

	In addition to the theory files, a ``ROOT`` file is produced for building the
	files. You can reproduce this file by running the compiler with the ``--root``
	flag.

	Building/Running The Generated Files
	------------------------------------

	Before using the generated theory files, ensure you have built the AutoCorres heap like so::

	L4V_ARCH=X64 isabelle build -v -b -d $AC_DIR AutoCorres

	Where ``$AC_DIR`` is the root directory of AutoCorres.

	In Jedit
	^^^^^^^^

	Launch the Jedit editor with the following command::

	L4V_ARCH=X64 isabelle jedit -d $AC_DIR -l AutoCorres

	Where again, ``$AC_DIR`` is the root directory of AutoCorres.

	Then, simply open any file you wish to view.

	On the command line
	^^^^^^^^^^^^^^^^^^^

	Using the generated ``ROOT`` file, you can build the suite of files like so::

	isabelle build -D $GENERATED_FILES_DIR \
	-d $REPO_ROOT/cogent/isa \
	-d $AC_DIR

	This will:

	* Select the root file located in the directory specified by ``$GENERATED_FILES_DIR``
	and evaluate it, which is the directory where your ``ROOT`` file and generated
	theory files are located;
	* Include the Cogent theory files in ``$REPO_ROOT/cogent/isa``, where ``$REPO_ROOT``
	is the root directory of the Cogent repository;
	* Include AutoCorres theories located in ``$AC_DIR``.

	Examples
	--------

	A Simple Example
	^^^^^^^^^^^^^^^^

	In this example, we're going to write a function that squares a ``U64``, and prove
	the correctness of the embedding in Isabelle/HOL.

	You can find all the code for this example in our `repository <https://github.com/NICTA/cogent/tree/master/cogent/examples/square>`_

	We'll use the following Cogent code:

	.. literalinclude:: ../cogent/examples/square/square.cogent
	:language: haskell

	And we'll build a shallow embedding using the following command:

	.. code-block:: bash

	cogent square.cogent -g -o square\
	--root-dir="../../.." \
	--shallow-normal \
	--entry-funcs=entrypoints.cfg

	which gives us the following shallow embedding:

	.. code-block:: isabelle

	(*
	This file is generated by Cogent
	*)

	theory Square_Shallow_Normal
	imports "Square_ShallowShared"
	begin

	definition
	square :: "64 word ⇒ 64 word"
	where
	"square x__ds_var_0 ≡ HOL.Let x__ds_var_0 (λx. (*) x x)"

	end

	Next, we'll create a file and import our shallow embedding, then prove its
	correctness against the specification of square in Isabelle/HOL:

	.. literalinclude:: ../cogent/examples/square/SquareProof.thy
	:language: isabelle


	A More Involved Example
	^^^^^^^^^^^^^^^^^^^^^^^

	The code for this example is more involved than the previous, so follow along with the source located
	`here <https://github.com/NICTA/cogent/tree/master/cogent/examples/system-abstract-verif>`_.

	Naturally when writing Cogent code, you'll interface with C code frequently. This C code must go through AutoCorres for
	the refinement proof, so we'll need to put a bit more effort to set up the verification chain for such Cogent programs.

	This time, we'll be using abstract functions and types to represent the C functions and types we wish to call and use.
	Our program will take in a toy ``KernelState`` type, and check the status of a magic number in an object of this type. If the number
	has been corrupted, we'll cause a kernel panic; otherwise, continue on.

	The C code this time will involve the C standard library, which we don't want to pass into AutoCorres as it often
	causes errors. In realistic situations, the same issue can potentially be caused by system code included into Cogent programs that
	may not directly be verified along with the Cogent code (such as Linux kernel headers), so we need a way to work around this.

	Note that, as we will use types from the standard library that are not implemented in our antiquoted C or Cogent code, we
	must inform the compiler of the existence of these types. We do this with the flag ``--ext-type=types.cfg`` (we have explained this flag in :ref:`first-program`), which points
	to the file in our example directory. As we'll use the file stream type, the only line in this file is ``FILE``.

	We'll write two wrapper files, each called ``wrapper.ac`` that contain different definitions of various library types and functions
	in order to work around AutoCorres. Observe the sample source code directory layout::

	.
	├── entrypoints.cfg
	├── Kernel.cogent
	├── main.ac
	├── Makefile
	├── plat
	│ ├── system
	│ │ └── wrapper.ac
	│ └── verification
	│ └── wrapper.ac
	└── types.cfg

	You'll notice in our platform folder (``plat``), we have a ``system`` folder and a ``verification`` folder each with it's own wrapper file.

	In the system folder, the wrapper file includes the C library for execution, defines the abstract types used in the Cogent code,
	and finally includes our to be compiled Cogent code followed by the main code. You may also notice that we define two messages as
	string literals in variables (``KERNEL_PANIC_MESSAGE``, ``KERNEL_OK_MESSAGE``). AutoCorres won't accept string literals in C code,
	so it's important to abstract them out of the main code. Finally, the wrapper includes the implementations of our abstract functions
	(``kernelPanic``, ``memMagicNumer``) that our Cogent code uses, and a ``main`` function to test the Cogent code, all located in ``main.ac``.

	.. literalinclude:: ../cogent/examples/system-abstract-verif/plat/system/wrapper.ac
	:language: c

	In the ``verification`` folder however, we must provide definitions of the standard library types and functions we use
	(``FILE``, ``fprintf``, ``malloc``, ``free``, ``exit``, ``stdout``). During verification we'll treat these functions like a black box,
	so the actual implementation doesn't matter (as long as AutoCorres can parse them). For example, we can give the following
	definitions to the FILE type and fprintf:

	.. code-block:: c

	typedef struct filedummy {
	int dummy;
	} FILE;

	int fprintf(FILE * stream, char * str) {
	// do nothing
	return 0;
	}

	We can also give dummy definitions to our string literal placeholder variables at this time too:

	.. code-block:: c

	char * KERNEL_PANIC_MESSAGE = 0x0;
	char * KERNEL_OK_MESSAGE = 0x0;

	Now AutoCorres will be happy with our code!

	To make the verification build chain simpler, in our ``Makefile`` we simply change which ``wrapper.ac`` is supplied to
	the compiler depending on whether or not we want to build for verification or to build the system to run.

	Finally, we're left with our Cogent code:

	.. literalinclude:: ../cogent/examples/system-abstract-verif/Kernel.cogent
	:language: haskell


	To run this example, run ``make system`` to compile the code into an executable called ``kernel``, or run
	``make verification`` to build all Isabelle/HOL verification files and C code suited for AutoCorres.

	Common Errors
	-------------

	ACInstall
	^^^^^^^^^

	.. highlight:: none

	You may see the following error from AutoCorres when running this file::

	### In file included from file.c:3:
	### file.h:6:10: fatal error: cogent-defns.h: No such file or directory
	### #include <cogent-defns.h>

	This is due to ``cpp`` being unable to find the Cogent C header, which is located in the Cogent repository
	in `cogent/lib/cogent-defns.h <https://github.com/NICTA/cogent/blob/master/cogent/lib/cogent-defns.h>`_. Adding the compiler flag ``--fake-header-dir=$REPO_ROOT/cogent/lib`` will fix this.
	You can additionally set this directory to the result of ``cogent --libgum-dir``, which will print the location of the Cogent
	standard library directory.

	You may also see the following error::

	*** Undeclared constant: "??.\<Gamma>"
	*** At command "autocorres" (line 14 of "ACInstall.thy")

	This can be due to several reasons:

	* You have not specified entrypoint functions via the compiler flag ``--entry-funcs=FILE``.
	* Your source file/entrypoiint functions contain only polymorphic functions. Concrete C functions
	will only be generated when these polymorphic functions are instantiated by your Cogent
	source file or your entrypoint file. You can do so in the entrypoint file like so: ``functionName[TypeName]`` (also see :ref:`poly-function-example` for more explanation).







	.. _AutoCorres: https://ts.data61.csiro.au/projects/TS/autocorres/
	.. _`Isabelle/HOL 2019`: https://isabelle.in.tum.de/
	.. _`Cogent theories`: https://github.com/NICTA/cogent/tree/master/cogent/isa/
	.. _`C refinement theories`: https://github.com/NICTA/cogent/tree/master/c-refinement
	.. _`Cogent repository`: https://github.com/NICTA/cogent