.. _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 [OPTION]… FILE…`` provides the following command-line ``[OPTION]``: * ``-D CONSTANT:VALUE`` or ``--define=CONSTANT:VALUE``: Define a toplevel ``CONSTANT`` declaration with the given ``VALUE``. ``CONSTANT`` must be declared in the theory file. * ``-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. * ``-L VAL`` or ``--loadpath=VAL``: Additional loadpath. * ``-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``. * ``--log-file``: Path to log CAISAR trace. Defaults to ``caisar.log`` * ``--onnx-out-dir=DIRECTORY``: Write all ``NIR`` from current verification query as ``ONNX`` file in ``DIRECTORY``. * ``-p PROVER[:ALTERN][:PRECISION][,...]`` or ``--prover=PROVER[:ALTERN][:PRECISION][,...]``: Provers to use. ``PROVER[:ALTERN][:PRECISION][,...]`` is comma-separated list of ``PROVER[:ALTERN][:PRECISION]`` items; ``PROVER`` is case insensitive, ``ALTERN`` is case sensitive, and ``PRECISION`` takes values from 0 (default, fastest but imprecise verification) to 5 (accurate but slow verification). Available provers: ``Marabou``, ``maraboupy``, ``PyRAT``, ``SAVer``, ``AIMOS``, ``cvc5``, ``Alt-Ergo``, ``Z3``, ``nnenum``, ``alpha-beta-CROWN``. See :ref:`provers` for a detailed description of each prover capacity. * ``--speclang=LANG``: Specification language to use. By default, CAISAR expects specifications to be written in the high-level specification language ``WhyML``. CAISAR also has the ability to directly process ``VNNLIB 1.0`` [1]_ when also providing a path to a valid ``ONNX`` with the ``--onnx_vnnlib`` option. .. [1] The 1.0 version is `loosely defined here `_. The 2.0 version will be implemented as a separate library. 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. The ``caisar-detection.conf`` file describe all provers supported by CAISAR, including versions and configuration alternatives. See section :ref:`registering-prover` for more details. 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. CAISAR with JSON ---------------- It is possible to use most of CAISAR capabilities either from the command-line, or by passing to CAISAR JSON values. A verification query can be achieved with the ``verify-json`` command, and external prover detection can be achieved with the ``config-json`` command. ``verify-json`` will require a valid JSON value describing a CAISAR verification query, closely following OCaml types. ``config-json`` will output available provers for CAISAR either on stdout, or as a JSON value as well. The specification of aforementioned values relies on `JSON schemas `_, and are automatically generated by CAISAR at each build. The resulting schemas are available under the ``config/schemas`` folder. They can be the backbone of an API to CAISAR in another programming language. The ``caisarpy`` Python API is an example of one of those. In case of needs, one can manually generate JSON schemas using the ``generate-json-schemas`` command. .. _registering-prover: 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. Useful to finetune a prover for a given use case * ``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. A driver describes transformations applied to a task to produce a valid prover query, and how to parse the prover output. 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 `_!