Verifying Concurrent Go Code in Coq with Goose