Modulo operator and dead Command code removal

[MattWindsor91]

This small PRQ adds a modulo operator % to Starling, with C-style precedence rules. This will work in Z3, but not HSF (afaik HSF doesn't do modular arithmetic?).

As we don't yet have any examples that go through and use modulo (sense barrier needs some more iterated views work, Peterson needs arrays), I've added a few unit tests along the way to try to make sure this works properly.

While adding support and tests in the Command intermediate value section I noticed that there is a huge swathe of dead code for getting one plus the highest intermediate in an expression. I've removed this so I don't have to add modulo to it :P

[MattWindsor91]

@BenSimner the use case is that modulo makes certain operations involving arrays much easier—for example, deciding what the other thread's thread ID in Peterson's algorithm becomes (myID + 1) % 2. It'll also be useful if I implement ringbuffer proofs in Starling.

[MattWindsor91]

@BenSimner It's also used for the sense barrier, but the sense barrier is blocked by some iterated views fun (like every exciting arrays proof :<)

[septract]

All looks good to me (aside from the things raised by @BenSimner, but I think your answers are sensible). :shipit: