[doc] A bit more detailed usage page.

doc/index.rst

@@ -3,6 +3,8 @@
    You can adapt this file completely to your liking, but it should at least
    contain the root `toctree` directive.
 
+.. _index:
+
 CAISAR documentation
 ====================
 
@@ -36,6 +38,8 @@ Support Vector Machines (SVM) are supported through an ad-hoc CSV format.
 Gradient boosting models and decision trees will soon be
 supported.
 
+.. _supported_provers:
+
 Provers
 -------
 
@@ -44,7 +48,7 @@ answers on proof obligations. Those programs are called
 "provers", altough some of them may not directly provide a
 logical proof.
 
-The supported provers is as follow:
+The supported provers are the following:
 
 * `PyRAT <https://laiser.frama-c.com/laiser-websites/pyrat-website/>`_,
   a neural network verifier powered by abstract interpretation (some developers of CAISAR are also working on PyRAT)

doc/usage.rst

+*Written in november 2022*
+
 .. _usage:
 
 Usage
 =====
 
-Property verification
----------------------
+Prover registration
+-------------------
+
+CAISAR relies on external provers to work. You must install
+them first, then point CAISAR to their location. Please
+refer to each prover documentation to install them.
 
-CAISAR can be used to verify properties on neural networks.
-The prototype command is ``caisar verify --prover=PROVER property.mlw``.
-File ``property.mlw`` defines the goal you want to verify,
-written in the Whyml language.
-Example of ``.mlw`` files can be seen in tests folder.
+Provers tend to be complex programs with multiple options.
+Some combination of options may be suited for one
+verification problem, while inefficient for another. As they
+also have different interface, it is also necessary to register
+their call in a way CAISAR can understand.
+To do so, you must register provers inside the ``config/caisar-detection-data.conf`` file.
+Each supported prover is registered by specifying the following fields:
 
-External verifiers detection
-----------------------------
+* ``name``: the name under which CAISAR will know the prover
+* ``exec``: the prover's executable name
+* ``alternative`` (optional): an alternative configuration for the
+  prover. To use it with CAISAR, use the option
+  ``--prover-altern``. Useful when you want to use the same
+  prover on different problems.
+* ``version_switch``: the command used to output the prover's
+  version
+* ``version_regexp``: a regular expression parsing the
+  output of ``version_switch``
+* ``version_ok``: CAISAR supported version of the prover.
+  Provers should only be used with their supported version.
+* ``command``: the actual command CAISAR will send to the prover. There are a few builtin expressions provided by CAISAR:
 
-CAISAR relies on external verifiers to work. You must install
-them first, then point CAISAR to their location.
-To do so,
-use ``DIR=/path/to/solver/exec caisar config -d.``
+  * ``%f``: the generated property file sent to the prover
+  * ``%t``: the timelimit value
+  * ``%{nnet-onnx}``: the name of the neural network file
+* ``driver``: location of the CAISAR driver for the prover, if any
 
-List of supported verifiers:
 
-* PyRAT
-* `Marabou <https://github.com/NeuralNetworkVerification/Marabou>`_
-* `SAVer <https://github.com/abstract-machine-learning/saver>`_
+Assuming you have installed a prover and you filled the `caisar-detection.conf` file,
+you can register the prover to CAISAR using the following command: ``DIR=/path/to/solver/exec caisar config -d``.
+
+Property verification
+---------------------
+A prominent use case of CAISAR is to model a specification for an artificial intelligence
+system, and to verify its validity for a given system.
+
+The modelling uses `WhyML <https://why3.lri.fr/doc/syntaxref.html>`_,
+a typed first-order logic language.
+Example of WhyML are in the `source code <https://git.frama-c.com/pub/caisar/-/tree/master/examples/>`_.
+You may also read the :ref:`examples` section of this
+documentation to get a first grasp on using WhyML.
 
-List of actively developed supports:
+Provided a file `trust.why` containing a goal to verify, the command ``caisar verify --prover=PROVER trust.why``
+will verify the goals using the specified prover. A list of
+supported provers is available in :ref:`supported_provers`. The prover
+must already be registered by CAISAR. Currently, only one
+prover can be selected at a time; future work will allow
+selecting multiple provers and orchestrate verification
+strategies.
+Internally, CAISAR will translate the goals into a form that
+is acceptable by the targeted prover, generating a file (the
+``%f`` defined in the previous section).
 
-* Tools that support SMTLIB as inputs: `Alt-Ergo <https://alt-ergo.ocamlpro.com/>`_, `Z3 <https://github.com/Z3Prover/z3/wiki>`_, `Colibri <https://colibri.frama-c.com/>`_
+Built-in properties
+-------------------
+In addition to all the theories provided by Why3, CAISAR
+provide additional theories that model commonly desirable properties for machine learning programs.
+All those predicates are located in the file ``stdlib/caisar.mlw``.
+Among them are theories to describe classification datasets,
+local and global robustness around a neighborhood.