Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq