[Civl] small fixes to Treiber stack example

[shazqadeer]

This PR updates the primitive atomic actions in treiber stack so that they uniformly follow the pattern of Map_Get, Map_Put, Cell_Unpack, Cell_Pack, etc.

The outstanding problems are as follows:

• Most primitive atomic actions do Map_Get on ts at the beginning and Map_Put on ts at the end. The proof would be better if each primitive atomic action did at most one Map_Get or Map_Put.
• There is a problematic assume in AtomicLoadNode#0 without which the proof does not succeed. The issue seems related to the first point. To clean up the proof, it seems that we need to maintain and prove an invariant at the lowest level---either top is nil or top is a member of stack.