[Civl] strengthened Pop spec to standard linearizability

[shazqadeer]

When I presented the Treiber stack proof to @erickoskinen , @NamrathaG , and @menesro, it was pointed out that the spec of Pop is too weak and does not distinguish between two separate cases when no data is returned:

• stack is empty and this is a successful outcome
• stack is non-empty but the operation failed and could be retried

This PR strengthens the spec of Pop to address this shortcoming with the biggest changes being:

• Pop returns an Option X rather than X; it is possible for success to be true and this value to be None
• The abstractions of ReadTopOfStack on Push and Pop side are different; the one on Push side is a right mover but the one on Pop side is not a mover at all.

[bkragl]

nice!