The local integral-model conjecture for $\Gamma_1(p)$-level local Shimura varieties

Let $(G,\{\mu\},b)$ be a local Shimura datum, let ${\mathcal G}$ be parahoric, set $K_0={\mathcal G}(\mathbb Z_p)$, and let $K_1$ be the kernel of the reduction map to the reductive abelian quotient over $\mathbb F_p$. Choose $S\subset S_{{\mathcal G},\mu}\subset X^*(T_{\mathcal G})$. The local $\Gamma_1(p)$-integral-model conjecture. There exists a formal scheme ${\mathcal M}^{\rm \int}_{K_1,S}$ over $\operatorname{Spf}(O_{\breve E})$ with rigid generic fiber ${\rm Sht}_{K_1}(G,\mu,b)$, together with a morphism to ${\mathcal M}^{\rm \int}_{K_0}$ extending the generic-fiber cover, an extended $T_{\mathcal G}(\mathbb F_p)$-action identifying the quotient with ${\mathcal M}^{\rm \int}_{K_0}$, and a morphism to $[\mathcal G\backslash{\rm M}^{\sqrt S}_{{\mathcal G},\mu}]$ fitting into the stated $2$-commutative diagram and inducing the stated isomorphism of formal stacks. This is the local analogue of the global conjecture; the local-model map is known in at least the PEL case, but the asserted level-$K_1$ formal model is left conjectural.