.. _usage: Using CAISAR ============ Commands summary ---------------- The CAISAR executable provide several subcommands, called using ``caisar [COMMAND]``. ``caisar --help`` provides a list of all available commands. Additionally, ``caisar [COMMAND] --help`` gives a synopsis for each available command. Command line options -------------------- ``caisar verify`` have the following specific command line options: * ``-D name:value`` or ``--define=name:value``: define a declared constant ``name`` with the given value ``value``. Constant must be declared in the theory file. * ``--dataset=FILE``: Path of a dataset file. To be deprecated. * ``-g [theory]:goal,..,goal`` or ``--goal [theory]:goal,...,goal``: Verify only the ``goal`` in the ``theory``. Theory must already be defined in the specification file. When no theory is provided, verify the specified goals for all theories. * ``-T theory`` or ``--theory=theory``: Verify all goals in ``theory``. * ``-m MEM`` or ``--memlimit=MEM``: Memory limit. ``MEM`` is intended in megabytes (MB); (GB) and (TB) can also be specified. Default: 4000MB. * ``-t TIME`` or ``--timelimit=TIME``: Time limit. ``TIME`` is intended in seconds (s); minutes (m) and hours (h) can also be specified. (MB), (GB) and (TB) can also be specified. Default: 20s. * ``-p PROVER`` or ``--prover=PROVER``. Prover to use. Support is provided for the following: Marabou, PyRAT, SAVer, AIMOS, CVC5, nnenum, alpha-beta-CROWN. See :ref:`provers` for a detailed description of each prover capacity. * ``--prover-altern=VAL``: alternative prover alternatives to use. Prover alternatives are prover-specific configurations that help provers to better perform on specific problems. Supported prover alternative are ``ACAS`` for alpha-beta-CROWN and PyRAT. Logging ******* CAISAR provides different log verbosity levels. To change the log verbosity level, provide the option ``--verbosity`` to the ``verify`` command. Available levels are ``quiet``, ``error``, ``warning``, ``info`` and ``debug`` (defaults to ``warning``). CAISAR also provides log *tags*. Each tag adds additional information in the log, independently of the log verbosity level. However, note that the ``debug`` verbosity level allows logging with all tags enabled. To enable a particular tag, use the option ``--ltag=TAG``, with ``TAG`` one of the following: * ``Autodetect``: display the output of the autodetect routine of CAISAR described in :ref:`prover-registration` * ``ProverSpec``: display the actual specification provided to the prover * ``ProverCall``: display the actual command used to call the prover * ``InterpretGoal``: display the goal interpretation * ``StackTrace``: display the stack trace upon a CAISAR error .. _prover-registration: 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 already supports several provers, listed in :ref:`provers`. Assuming you have installed a prover with an entry in the ``caisar-detection.conf`` file, you can register the prover to CAISAR using the following command: ``PATH=$PATH:/path/to/solver/executable caisar config -d``. Your prover should be displayed with its relevant version. 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 `_, a typed first-order logic language. Example of WhyML are in the `source code `_. You may also read the :ref:`examples` section of this documentation to get a first grasp on using WhyML. 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:`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). 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. Advanced usage: registering a new prover ---------------------------------------- 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. Registering for autodetection ***************************** The first step is to register provers inside the ``config/caisar-detection-data.conf`` file. Each supported prover is registered by specifying the following fields: * ``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 executable. There are a few builtin expressions provided by CAISAR: * ``%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 Building the specification for the prover ***************************************** It is necessary to convert the WhyML specification into an input that is understandable by the prover. CAISAR provide built-in translation from WhyML to the VNN-Lib and SMTLIB2 specification input formats. If your prover support those abovementioned input formats, adding support to your prover requires adding it in the files ``src/provers.ml``, ``src/provers.mli`` and the function ``call_prover`` in ``src/verification.ml``. For other input formats, it is necessary to write custom OCaml code in the ``src/printers/`` folder as well. Parsing the output of the prover ******************************** CAISAR rely on Why3's `drivers `_ to parse the output of the prover. If you add support for a new prover, consider opening a merge request on our `forge `_!