Shiho's conjecture on relative overconvergent isocrystals

Suppose that $(X,\overline{X})\to(S,\overline{S})$ is a Cartesian morphism of pairs over $k$, with $\overline{X}\to\overline{S}$ proper and $X\to S$ smooth. Let $E$ be an overconvergent $(F)$-isocrystal on $(X,\overline{X})/K$, and let $q\geq0$. For every frame $(T,\overline{T},\mathfrak{T})$ over $S$, with $\mathfrak{T}$ smooth over $\mathcal{V}$ near $T$, the indicated comparison isomorphisms define the realization of a unique object on $(S,\overline{S})$.

Shiho's conjecture. There exists a unique overconvergent $(F)$-isocrystal $\widetilde E$ on $(S,\overline{S})$ whose restriction to $\mathrm{Strat}^\dagger(T,\overline{T},\mathfrak{T})$ is

$$p_2^*\mathbf{R}^qf'_{\mathfrak{T},\mathrm{rig}*}E|_{(X_T,\overline{X}_{\overline{T}})}\cong\mathbf{R}^qf'_{\mathfrak{T}\times_{\mathcal{V}}\mathfrak{T},\mathrm{rig}*}E|_{(X_T,\overline{X}_{\overline{T}})}\cong p_1^*\mathbf{R}^qf'_{\mathfrak{T},\mathrm{rig}*}E|_{(X_T,\overline{X}_{\overline{T}})}.$$

If $\overline{S}$ is proper, $\widetilde E$ depends only on $f:X\to S$ and $E$.

This is a stratification-based formulation of Berthelot's conjecture and is presented in the source as open.