[[crypto_vector_sail_specifications]]
=== Sail Specifications

RISC-V maintains a 
link:https://github.com/riscv/sail-riscv[formal model]
of the ISA specification,
implemented in the Sail ISA specification language
cite:[sail].
Note that _Sail_ refers to the specification language itself,
and that there is a _model of RISC-V_, written using Sail.

It was our intention to include actual Sail code in this specification.
However, the Vector Crypto Sail model needs the Vector Sail model as a
basis on which to build. This Vector Cryptography extensions specification
was completed before there was an approved RISC-V Vector Sail Model.
Therefore, we don't have any Sail code to include in the instruction
descriptions. Instead we have included Sail-like pseudo code. While we have
endeavored to adhere to Sail syntax, we have taken some liberties for the
sake of simplicity where we believe that that our intent is clear to the
reader.

[NOTE]
====
Where variables are concatenated, the order shown is how they would appear
in a vector register from left to right.
For example, an element group specified as `{a, b, e, f}` would appear in a vector
register with `a` having the highest element index of the group and `f` having the
lowest index of the group.
====

For the sake of brevity, our pseudo code does not include the handling of
masks or tail elements. We follow the _undisturbed_ and _agnostic_ policies
for masks and tails  as described in the *RISC-V "V" Vector Extension*
specification. Furthermore, the code does not explicitly handle overlap and SEW
constraints; these are, however, explicitly stated in the text.

In many cases the pseudo code includes
calls to supporting functions which are too verbose to include directly
in the specification.
This supporting code is listed in
<<crypto_vector_appx_sail>>.


The 
link:https://github.com/rems-project/sail/blob/sail2/manual.pdf[Sail Manual]
is recommended reading in order to best understand the code snippets.
Also, the
link:https://github.com/billmcspadden-riscv/sail/blob/cookbook_br/cookbook/doc/TheSailCookbook_Complete.pdf[The Sail Programming Language: A Sail Cookbook]
is a good reference that is in the process of being written.

For the latest RISC-V Sail model, refer to
the formal model Github
link:https://github.com/riscv/sail-riscv[repository].

