Caro's conjecture on direct images of overconvergent isocrystals

Suppose that $f:(X,\overline{X})\to(S,\overline{S})$ is a Cartesian morphism of properly $d$-realisable pairs over $k$, with $\overline X\to\overline S$ proper and $X\to S$ smooth. The direct-image functor on arithmetic $\mathcal{D}$-modules is expected to preserve the subcategory of isocrystals.

Caro's conjecture. The functor

$$f_+:(F\text{-})D^b_{\mathrm{surcoh}}(\mathcal{D}^\dagger_{(X,\overline X)/K})\to(F\text{-})D^b_{\mathrm{surcoh}}(\mathcal{D}^\dagger_{(S,\overline S)/K})$$

sends $(F\text{-})D^b_{\mathrm{isoc}}(\mathcal{D}^\dagger_{(X,\overline X)/K})$ into $(F\text{-})D^b_{\mathrm{isoc}}(\mathcal{D}^\dagger_{(S,\overline S)/K})$.

The paper says this version has essentially been proved by Caro, although it is retained as a conjectural formulation for exposition.