.. _transformations:

Transformations in CAISAR
=========================

What are transformations
------------------------

`ONNX <https://onnx.ai>`_ is the de-facto standard to represent neural networks.
No solver supports all ONNX operators; neither does CAISAR for that matter.
Adding support for one ONNX operator to a solver is not a trivial task:
it requires resource and it is error-prone;
it is also a liability as it makes code more difficult to maintain.

Fortunately, some ONNX operators can be described as a combination of other, generally simpler, operators.
They are *syntactic sugar*.
*Transformations* in CAISAR are automatic operations
that modify an existing ONNX to replace certain operators
(that were in the original model being tested or that have been added by CAISAR itself)
with equivalent sub-networks that include simpler operators.
In this way, it is possible to call an existing solver on a problem
that contains an ONNX operator that the solver does not support,
as long as it supports those operators that the transformation introduced.

Some transformations might appear surprising or unnecessary.
For instance, it is possible to transform the `Add` operator with `Constant` and `Sub`
by using the equality :math:`x+y = x - (0-y)`.
Most solvers will not use this transformation as they will probably support `Add`;
however, if one wants to remove support to the `Add` operator for any reason
(provability of correctness, maintainability, efficiency, etc.),
this option is available.

Transformations can be chained, which gives a sort of *hierarchy* of operators.
However, this hierarchy is not strict,
and CAISAR offers a wide array of transformations.

Using transformations during verification
-----------------------------------------

The list of transformations to apply is specified in the driver of the solver.
For instance, application of the `transform_arg_max` transformation,
which replaces the `ArgMax` operator with a combination
of basic operators such as `MatMul`, `Add`, `Sign`, and `ReLu`,
can be indicated by the following instruction:

::

    transformation "transform_arg_max"

Transformations are called in order.
One transformation may introduce an operator that is not supported.
Consider for instance a scenario where both `ArgMin` and `ArgMax` operators need to be removed from the network.
The transformation for operator `ArgMin` introduces a copy of `ArgMax`;
thus, it is important to apply the transformer that removes `ArgMax`
after applying the one that removes `ArgMin`.

Transforming existing ONNX
--------------------------

CAISAR is also able to apply the transformations to an ONNX
and output the resulting ONNX.
This feature is used through the following command:

.. code-block:: console

    caisar simplify -i input_file.onnx -o output_file.onnx -s list_of_transforms.txt

where

* ``input_file.onnx`` is the path to the ONNX file on which the transformations are to be applied;
* ``output_file.onnx`` is the path to the ONNX file generated by CAISAR; and
* ``list_of_transforms.txt`` is a text file that contains the names of the transformations to apply (one per line).


Existing transformations and hierarchy
--------------------------------------

The list of transformations can be accessed with the following `ocaml` command:

.. code-block:: ocaml

    Nir.Transform.registrables |> Base.List.map ~f:(fun (_,n,_) -> n);;

Base operators
**************

The base ONNX operators are those that we might expect pretty much all solvers to support.
Nonetheless, there are some operations within this set.

We consider that the base operators are:

* `Constant`,
* `Add`,
* `Sub`,
* `Mul`,
* `MatMul`,
* `ReLu`,
* `Transpose`,
* and `Sign`.

The last two operators are less often supported.
As proof-of-concept, CAISAR includes a transformation
that rewrites the operator `Add` with `Constant` and `Sub`
so that `A + B` is rewritten `A - (0 - B)`.
This transformation is called `transform_add`.

ReduceSum
*********

Operator `ReduceSum` can be rewritten only when its second input
(the list of axes upon which the operation is to be made)
is a `Constant` tensor.
`ReduceSum` is then composed of a sequence of triplets
(each associated with one of the axes)
in which a `Transpose` is first performed to move the dimension at the end,
a `MatMul` is used to sum up the elements,
and a `Transpose` is performed to restore the position of the axis.
(The `Tranpose` is *not* performed when the axis is already the last one.)
Finally, a `Reshape` may be applied if the `keepdims` flag is negative.

ArgMax and ArgMin
*****************

.. _argmax:

.. figure:: argmax.png
    :scale: 70%
    :align: center

    Transforming `ArgMax` and `ArgMin` operators into basic operators.

`ArgMax` and `ArgMin` can be transformed using the `transform_arg_max` and `transform_arg_min` transformations, respectively.
`ArgMax` is transformed into base operators, including `Sign` and `Relu`;
`ArgMin` is transformed into `ArgMax`.
The two transformations are shown on :numref:`argmax`.

The semantics of `ArgMax` transformation as well as its proof is available in a
:download:`separate document <./argmax_transform.pdf>`.