[miaou] Implement description of irreflexive tests

[fsestini]

This PR extends miaou7 to be able to generate English prose descriptions of memory model requirements expressed in the form of irreflexive test in the cat file.

Not all such irreflexivity tests are supported. This extension specifically targets cat tests corresponding to the prose requirements from the Arm ARM Section B2.3.1, in the definition of Reads-from-memory and the definition of Coherence-Before, Coherence-after. In the current cat model, these are the irreflexive tests coRW1-Exp, coRW1-MTE, coWW-Exp, coWR-Exp, and coWR-MTE. For these tests, the extended miaou7 will generate a description that closely matches the currently handwritten prose from the Arm ARM. For example:

$ dune exec miaou7 -- ./herd/libdir/aarch64/ArmARM-M.a/aarch64.cat -show coRW1-Exp
For two effects E\textsubscript{1} and E\textsubscript{2}, if all of the following apply:
\begin{itemize}
\item \ExpR{E\textsubscript{1}}.
\item One of the following applies:
  \begin{itemize}
  \item All of the following apply:
    \begin{itemize}
    \item \expandafter{\MakeUppercase\po{E\textsubscript{1}}{E\textsubscript{2}}}.
    \item \expandafter{\MakeUppercase\sameloc{E\textsubscript{1}}{E\textsubscript{2}}}.
    \end{itemize}
  \item \expandafter{\MakeUppercase\rmw{E\textsubscript{1}}{E\textsubscript{2}}}.
  \end{itemize}
\item \ExpW{E\textsubscript{2}}
\end{itemize}
then it is not the case that \expandafter{\MakeUppercase\rfi{E\textsubscript{2}}{E\textsubscript{1}}}.

Heuristic for identifying premises and conclusion

The generated prose follows an “if [precondition] then [postcondition]” structure. However, the corresponding cat expressions do not carry an intrinsic notion of “precondition” vs “postcondition”.

The extended miaou7 applies a heuristic to determine which parts of the cat expression are interpreted as premises and which as the conclusion. Specifically, it looks for irreflexive tests of one of the following forms:

• irreflexive r₁; r₂; …; r, where r is not an identity relation ([...]), or
• irreflexive [e]; r₁; r₂; …; r; [e₁]; [e₂]; …; [en], again with r not an
  identity.

In both cases, the final non-identity relation r is interpreted as the postcondition, and all relations preceding it are interpreted as the precondition. This matches how irreflexive tests such as coRW1-Exp, etc., are written in the cat model and hand-described in B2.3.

Note that as a result of this heuristic, any trailing identity relations after r are ignored. The assumption is that, in a test of the form

irreflexive [e]; r₁; r₂; …; r; [e₁]; [e₂]; …; [en]

the set e and e₁ & ... & en are expected to be the same, in which case the test above is equivalent to

irreflexive [e]; r₁; r₂; …; r

(I believe the equivalence should also hold if the set e is a strict subset of e₁ & ... & en, but not the other way around.)

This assumption is not currently checked by the tool, although it is consistent with the current state of the memory model. If needed, miaou7 could be strengthened to verify that this condition holds.

Ideas for future tweaks to the cat model

Ideally, we would like miaou7 to generate identical prose for equivalent cat statements.

For example, the following two statements should yield the same description:

irreflexive [R]; foo; [W]; bar; [R]
irreflexive [R]; foo; [W]; bar

miaou7 already handles this case by internally normalising the first form into the second, as described above. However, other patterns are not yet handled. For example:

irreflexive [Exp & W]; (po & same-loc); [Exp & R]; (ca & int); [Exp & W] as coWR-Exp

Since po & same-loc is an internal relation, ca must also be internal for the overall relation to be potentially reflexive. In other words, ca & ext always yields an irreflexive relation, and therefore does not represent an interesting "irreflexivity" test.

The above can therefore be simplified to:

irreflexive [Exp & W]; (po & same-loc); [Exp & R]; ca; [Exp & W] as coWR-Exp

This PR does not introduce such simplification (in the cat model or in miaou7's internals). Consequently, the generated prose will include a description of the int component:

$ dune exec miaou7 -- ./herd/libdir/aarch64/ArmARM-M.a/aarch64.cat -show coWR-Exp
For two effects E\textsubscript{1} and E\textsubscript{2}, if all of the following apply:
\begin{itemize}
\item \ExpW{E\textsubscript{1}}.
\item \expandafter{\MakeUppercase\po{E\textsubscript{1}}{E\textsubscript{2}}}.
\item \expandafter{\MakeUppercase\sameloc{E\textsubscript{1}}{E\textsubscript{2}}}.
\item \ExpR{E\textsubscript{2}}
\end{itemize}
then it is not the case that all of the following apply:
\begin{itemize}
\item \expandafter{\MakeUppercase\ca{E\textsubscript{2}}{E\textsubscript{1}}}.
\item \expandafter{\MakeUppercase\int{E\textsubscript{2}}{E\textsubscript{1}}}.
\end{itemize}

While we can certainly continue to make miaou7 smarter, another option is to apply light simplifications to the formal memory model itself (for example, rewriting ca & int to ca in irreflexivity tests), so that tools like miaou7 can assume the input cat model is already “pre-normalised” by convention.

I believe @relokin is overall in agreement with this idea; it would be great to also get @artkhyzha ’s opinion. In any case, please note that no changes to the cat files are planned for this particular PR.