Conjecture on restriction functors and full faithfulness of specialization

Let $Y_0$ be a $k$-scheme, let $X_0$ be a smooth ambient scheme when specified, and let $\rho_{Y_0,X_0}:\mathrm{Isoc}^{\dag}(Y_0/K)\to\mathrm{Isoc}^{\dag}(Y_0,X_0/K)$ and $\mathrm{cv}:\mathrm{Isoc}^{\dag}(Y_0,X_0/K)\to\mathrm{Isoc}(Y_0/K)$ be the restriction functors, with their $F$-variants defined similarly. Restriction and specialization conjectures. The functors $\rho_{Y_0,X_0}$ and $\mathrm{cv}$ should be fully faithful. Moreover: (a) when $X_0$ is smooth, for every overconvergent isocrystal $E$ on $Y_0$, there is a functorial isomorphism in $E$

$$\mathrm{sp}_{Y^{\dag}\hookrightarrow U^{\dag},T_0,+}(E)\simeq \mathrm{sp}_{X_0\hookrightarrow\mathcal{P},T_0+}\circ\rho_{Y_0,X_0}(E);$$

(b) the functor $\mathrm{sp}_{Y^{\dag}\hookrightarrow U^{\dag},T_0,+}$ is fully faithful. The source notes that part (a) is proved when a Frobenius structure is available. These claims concern the comparison between overconvergent isocrystals and arithmetic $\mathcal{D}$-modules, while the full faithfulness assertions and part (b) remain conjectural in the stated context.