[Civl] Fix primitives

[shazqadeer]

This PR attempts to fix up the layer 0 primitives used in the Treiber stack example so that they make more sense. There is considerable improvement from before. One annoying thing still left is the presence of assume statements in the definition of AtomicLoadNode#0. These assume statements are converted into assert statements in the next layer up inside AtomicLoadNode. But it would be better to refactor the proof somehow to have the assert statements at the lowest layer.