.. _interpretation:

The CAISAR modelling language
=============================

Origin: WhyML
-------------

CAISAR heavily relies on Why3 and uses the WhyML language as a basis for its own
interpretation language. A reference of WhyML is available on the original `Why3
manual <https://www.why3.org/doc/syntaxref.html>`_.

However, since Why3 aims to verify a whole range of programs, it cannot
specialize on a particular program structure. For further background, the paper
[F2013]_ from one of Why3's original author details the rationale and tradeoff
involved in the WhyML design and implementation. To quote the author, "[the Why3
team] has come up with logic of compromise".

As CAISAR focuses on artificial intelligence systems, it can make some
additional assumptions on the nature of the inputs, program and users:

* users will have a basic background on linear algebra, and expect CAISAR to
  reflect this

* inputs will mostly be multidimensional vectors (machine learning community
  coined the term "tensor" as well) of floating point values, strings, ints or
  chars

* the program control flow will mostly be composed of a lot of real or
  floating-point arithmetic operations: there is no loop with runtime invariant,
  nor conditional

With those constraints in mind, CAISAR provides several extensions to WhyML,
that we detail here. They can be used directly in any WhyML file provided to
CAISAR.

Some of those extensions will be "interpreted". During the translation from
"pure" WhyML terms to actual inputs to provers, symbols will be replaced with
other symbols, or directly computed by CAISAR.

Built-ins
---------

.. _built-in:

.. index:: Interpretation; interpretation

The built-ins are available under ``stdlib/caisar/``. To access the symbols they
define, the corresponding theory needs to be imported in the scope of the
current one. For instance, to import the symbols defined by the theory
``Vector``, prepend ``use caisar.types.Vector`` at the top of the file.

Vector
******

Types
~~~~~

.. literalinclude:: ../../stdlib/caisar/types.mlw
   :language: whyml
   :start-at: type vector 'a
   :end-at: type index = int


Functions
~~~~~~~~~

.. literalinclude:: ../../stdlib/caisar/types.mlw
   :language: whyml
   :start-at: val function ([])
   :end-at: map2 v1 v2 f

Predicates
~~~~~~~~~~
.. literalinclude:: ../../stdlib/caisar/types.mlw
   :language: whyml
   :start-at: predicate has_length
   :end-at: length(v1)

This vector type is abstract and can be extended. For instance, the vector
theory for integer is defined likeso:

.. literalinclude:: ../../stdlib/caisar/types.mlw
   :language: whyml
   :start-at: theory VectorInt
   :end-at: end

Model
*****

Types
~~~~~

.. literalinclude:: ../../stdlib/caisar/model.mlw
   :language: whyml
   :start-at: type model
   :end-at: type kind

Functions
~~~~~~~~~

.. literalinclude:: ../../stdlib/caisar/model.mlw
   :language: whyml
   :start-at: val function read_model
   :end-at: function (@@)

Dataset
*******

Types
~~~~~

.. literalinclude:: ../../stdlib/caisar/dataset.mlw
   :language: whyml
   :start-at: use caisar.types.Vector
   :end-at: type dataset = vector (a, b)

Functions
~~~~~~~~~

.. literalinclude:: ../../stdlib/caisar/dataset.mlw
   :language: whyml
   :start-at: Returns
   :end-at: function read_dataset

Predicates
~~~~~~~~~~

.. literalinclude:: ../../stdlib/caisar/dataset.mlw
   :language: whyml
   :start-at: predicate forall_
   :end-at: Vector.forall_


.. _nir:

The Neural Intermediate Representation (NIR)
********************************************

``NIR`` is CAISAR's internal representation of machine learning models.
It is a Directed Acyclic Graph (DAG) where nodes are describing operations on
multidimensional arrays (also called *tensors*), and edges describe the dataflow
from inputs to outputs.

The ``NIR`` is heavily influenced by the `ONNX <https://onnx.ai/>`_
representation of neural networks. Unless stated otherwise in the code
documentation, the semantics of ``NIR`` nodes follows the ``ONNX`` semantics.

Here is the list of supported operators:

.. literalinclude:: ../../lib/nir/node.mli
   :language: ocaml
   :start-at: type descr =
   :end-at: [@@deriving show]


.. [F2013] Jean-Christophe Filiâtre, *One Logic to Use Them All*,
   CADE 24 - the 24th International Conference on
   Automated Deduction