and non-constructor defined in our model is actually used (i.e., the model does not contain “dead” code).

-   Our model is [*readable*]{}. Despite its size, efforts have been made to give it a modular structure, which is reflected in the sections of Annex \[ANNEX-REC\]. Particular care has been taken to choose constructors appropriately and to keep non-constructor definitions as simple as possible.

Validation of the MAA Model {#VALIDATION}
===========================

In this section, we detail the various steps performed to make sure that our model is correct:

-   Our model is [*self-checking*]{}. Because the REC language has no input/output primitive and no provision for interfacing with external C code, it cannot be used to compute the MAC value of a given file. In order to check whether our model was correct or not, we enriched it with 203 test vectors originating from three sources, namely: (i) all the test vectors provided in Tables 1 to 6 of [@ISO-8731-2:1992 Annex A] and [@Davies-Clayden-88]; (ii) all the test vectors provided in [@ISO-8730:1990 Annex E.3.3] — the subsequent test vectors of [@ISO-8730:1990 Annexes E.3.4 and E.4] were discarded because of their size (they deal with two messages having 84 and 588 blocks, which would 