Gerwin Klein

I have also not seen this in a very long time. Would it be possible to run a stress test to confirm? (E.g. that one test a few hundred times...

Agreed, it's not going to be certain, but it should be better than "we haven't seen this in a while" :-)

The document so far does not mention `words[0]` or `words[1]`, so I think adding them to the diagram may add more confusion than it helps. It can currently really only...

(rebased)

I think this still needs to wait for the corresponding l4v PR to be up. @michaelmcinerney is that correct?

(Currently the tests on master are broken from the AArch64 debug API PR, so we should hold off on merging code PRs until that is fixed)

Better to do them simultaneously, but with the new `mcs` manifest handling we can actually check, I've started a proof test on the PR now.

Issue #854 is slightly related to this in the sense that it wants to make more use of projections in ASpec.

(rebased)