Let $G$ be an abelian variety with good reduction over a finite extension $K$ of $\mathbb{Q}_p$. In equation (2.4) on page 179 of my edition of "The Frobenius and monodromy operators for curves and abelian varieties" by Coleman and Iovita, they mention that there is an isomorphism $H^1_{dR}(G) \cong H^{1 \dagger}(G^\dagger)$, where $G^\dagger$ is "the dagger completion of $G$ along the special fiber of its model" (meaning its model $\mathcal{G}$ over $\mathcal{O}_K$ with good reduction). 

The meaning of this notation is not totally clear to me. Earlier in the paper, when $Y$ is a smooth proper curve over $K$ with a model $\mathcal{Y} / \mathcal{O}_K$ with good reduction, they write $H^{1 \dagger}(Y^\dagger) \cong H^1_{cris}(\overline{\mathcal{Y}}, K_0) \otimes_{K_0} K$, where $\overline{\mathcal{Y}}$ is the special fiber, $K_0 \subseteq K$ is the maximal unramified subfield, and $H^1_{cris}$ is crystalline cohomology. 

However, for properties of this dagger cohomology group they then cite the papers "Formal cohomology I/II" by Monsky-Washnitzer and Monsky. These papers make no mention of crystalline cohomology. They do define a cohomology theory, called Monsky-Washnitzer cohomology, but Monsky and Washnitzer only define this cohomology for certain affine schemes, not proper ones. They do not define what it means to take the dagger completion of a proper variety, although they do define a "weak completion" operation for rings which uses the dagger notation.

As I see it there may be two ways that I can interpret the isomorphism $H^1_{dR}(G) \cong H^{1 \dagger}(G^\dagger)$. If I define the latter group as $H^{1 \dagger}(G^\dagger) \cong H^1_{cris}(\overline{\mathcal{G}}, K_0) \otimes_{K_0} K$, then it appears this isomorphism is a well-known de Rham-crystalline cohomology comparison theorem. 

Alternatively, I had some trouble finding a reference for the term "dagger completion", but there is this paper of Hsie from 2018, which seems to globalize Monsky-Washnitzer cohomology to non-affine schemes: https://synthical.com/article/506aac66-ffb1-11ed-9b54-72eb57fa10b3 Ideally, it would be best for me if the weak completion operation of Monsky-Washnitzer globalizes, and I can interpret $G^\dagger$ by covering $\mathcal{G}$ by affine patches $U_i = \Spec A_i$, where $A_i$ is an $\mathcal{O}_K$-algebra, weakly completing $A_i$ with respect to $\mathfrak{m}_K A_i$ to obtain $A_i^\dagger$, and then gluing the patches $\Spec A_i^\dagger$ to obtain $G^\dagger$. I could hopefully interpret this as a dagger formal scheme in the sense of Hsie, and then $H^{1 \dagger}(G^\dagger)$ is the Monsky-Washnitzer cohomology as defined in Hsie. Ultimately my goal is to perform some explicit computations. This construction has the benefit that there seems to be a natural map $H^1_{dR}(G) \to H^{1 \dagger}(G^\dagger)$ coming from functoriality of Kahler differentials, and this is probably where the isomorphism claimed in Coleman would come from.

However, I have no idea if this interpretation is valid. The paper of Coleman is much older than that of Hsie, and Hsie's paper contains no de Rham comparison theorem like the one Coleman uses. I am not committed to using Hsie's paper, but it seems like there may be some interpretation of $H^{1 \dagger}(G^\dagger)$ which uses the ideas of Monsky-Washnitzer, not crystalline cohomology, and Hsie's approach was the most natural one I could find. Does such an interpretation exist, and if so, where can I read about it? What did Coleman and Iovita have in mind here? 

If my only recourse is using crystalline cohomology, where can I find the most accessible proof of the de Rham-crystalline comparison theorem, and can the isomorphism be made explicit enough for practical computations (say in the case of $G$ an elliptic curve)?

References:

Robert Coleman. Adrian Iovita. "The Frobenius and monodromy operators for curves and abelian varieties." Duke Math. J. 97 (1) 171 - 215, 15 March 1999. https://doi.org/10.1215/S0012-7094-99-09708-9

BinYong Hsie. (2018). The Monsky-Washnitzer cohomology and the de Rham cohomology. https://synthical.com/article/506aac66-ffb1-11ed-9b54-72eb57fa10b3