each detail of the MAA is expressed using term rewrite systems only; the model does not rely upon any externally-defined type or function and is thus independent from machine-specific assumptions, e.g., 32-bit vs 64-bit words or little- vs big-endian ordering.

-   Our model is [*executable*]{}. From a theoretical point of view, this was enabled by the aforementioned shift from general LOTOS abstract data types to term rewrite systems, which are less declarative and more operational. From a practical point of view, this shift was not sufficient, as the MAA intensively manipulates block values (i.e., 32-bit numbers), which cannot be reasonably implemented in the Peano style (the execution stack quickly overflows when these numbers are represented using the and constructors). To overcome this issue, we chose to represent blocks in binary form, as words of four octets. So doing, the logical operations on blocks (, , , and ) are easy to define using bitwise and octetwise manipulations. The arithmetical operations (, , and ) are more involved: we implemented them using 8-bit, 16-bit, and 32-bit adders and multipliers, more or less inspired from the theory of digital circuits.

-   Our model is [*minimal*]{}, in the sense that each sort, constructor, 