PAC with collision

[diaolo01]

This PR continues #1235. It uses Predicates for handling PAC collisions. The PAC solver is rebuilt using the Predicates to preserve collision history across multiple AUT* instructions.

[HadrienRenaud]

A lot of work into this, nice one. I have a lot of small esthetics comments, feel free to choose the ones you want to keep.

Do you think there are some performance difference? For example on make vmsa-test? How long does make pac-test takes to run?

The main question I have is the following. If I understand correctly, right now the way to add a predicate is the following:

1. Use an operation that use a collision wrapper
2. This splits the execution and adds an equation Assign (fresh_var (), Binop (AssumeCollision, v1, v2)) (resp. AssumeNoCollision on the other execution) (skipping the case where both values are constants)
3. When in valconstraint.ml v1 and v2 are reduced to constants c1 = {x with pac = p1} and c2 = {x with pac = p2}, Constant.collision returns Some (p1, p2), and thus AArch64Op.assumeCollision raises a Constraint (Eq (p1, p2)) (resp Neq)
4. valconstraint.ml then pushes on the equation list Predicate (Eq (p1, p2))
5. valconstraint.ml calls the PAC solver at the end of its run with all the predicates accumulated.

Would it possible to skip the binop phase and directly push the predicates in AArch64Sem? That would change:

1. similar
2. This splits the execution and adds the predicates AssumeCollision (v1, v2) (resp. AssumeNoCollision)
3. valconstraint doesn't touch the predicates
4. valconstraint doesn't touch the predicates
5. similar as before, but with AssumeNoCollision instead of Neq and AssumeCollision instead of Eq. Potentially we need to add a step of substitution inside predicates to convert AssumeCollision (V.Var s1, V.Var s2) into AssumeCollision (V.Val c1, V.Val c2), but this is a very standard step.

The main advantage with this is that it would remove the need for the Constraint exceptions, and probably simplify the interaction between the PAC solver and the non-pac solver.

Please note that I don't know how litmus nor herd/constraints.ml work and so I can't really review this part of the code. I also haven't reviewed the litmus tests.

[HadrienRenaud]

Extract this in a separate function?

[fsestini]

Thanks for the work you put into this. I'm not too familiar with the PAC feature, or the logic around constraints, so please bear with me if some of my comments on those aspects don't quite make sense.

I do have a more general concern however: this PR introduces new abstract functions/types in Arch_herd.S (for the constraint solver), but the abstraction feels fragile in both directions: implementations assume specific caller behavior (e.g., pp_solver_state must return "" for empty_solver because top_herd replaces solver states when debugging is disabled; similarly for compare_solver_state), and callers assume specific implementation details (e.g., top_herd relies on do_dump_final_state always including solver printing via pp_solver_state).
This creates a brittle contract that's not enforced by the types and makes reading the code harder (you can't understand local choices, like the "empty solver_state" trick at top_herd.ml:542, without knowing implementation details of distant call sites) and later refactors more prone to break things inadvertently.
My suggestion would be to either make those assumptions more explicit in the API, or keep the abstraction honest by removing caller‑specific behavior from implementations and implementation‑specific assumptions from call sites. I appreciate this is quite vague, so please refer to the in-code comments.

[diaolo01]

Thank you @HadrienRenaud for the review.
I have measured the time spent on make test with and without PAC collision: 180.69s user 42.37s system 317% cpu 1:10.19 total vs 180.62s user 42.07s system 332% cpu 1:06.91 total. TLDR; with PAC less parallelism is used and it spends 4 more seconds.
Running make test.pac takes roughly 1 vs 0.5 seconds.

I have now removed the Constraint indirection and emit predicates directly from AARch64Sem. This results in 1.2 seconds for make test.pac and 54 seconds for make test.

Thank you @fsestini for the review.
Perhaps the biggest change was that I have moved the PAC solver into a module and differentiated between the compare functions used for the pretty printing and sets ordering.