Add Chase-Lev deque

This MR adds logically atomic specifications and proof of Chase-Lev work-stealing deque.

Note: the proof uses a strong variant of mono_nat_own_alloc and a variant of LATs having extra non-atomic postconditions, so mono_nat.v and atomic.v were taken from the Iris repository and edited.