fix lock spec code depending on Σ

This fixes the problem that in the generic lock spec, the code is allowed to depend on Σ. Unfortunately there's some syntactic overhead that comes with this since all the predicates and lemmas now need to quantify over Σ, and we need to managed the lockG Σ assumptions explicitly as well since we can only make them a typeclass after the lock type is declared...

The alternative would be to split up the lock spec into a typeclass for the code and one for the predicates and lemmas, but I don't think that would be significantly less overhead on the spec side, and it would be more overhead for users.

If this approach seems acceptable then I can adjust rwlock and atomic_heap to do the same.