Compatibility of characteristic cycles with proper push-forward

Let $f\colon X\to Y$ be a morphism of smooth schemes over a perfect field $k$. Assume that every irreducible component of $X$ has dimension $n$, and every irreducible component of $Y$ has dimension $m$. Let ${\cal F}$ be a constructible complex on $X$, with singular support $C=SS{\cal F}\subset T^*X$, and assume that $f$ is proper on the support of ${\cal F}$. Write $f_\circ C\subset T^*Y$ for the image of $df^{-1}(C)$ under the canonical correspondence.

Characteristic-cycle push-forward conjecture. We have

$$CCRf_*{\cal F}=f_*CC{\cal F}$$

in $CH_m(f_\circ C)$. In particular, if every irreducible component of $f_\circ C$ has dimension $m$, the corresponding equality holds as cycles.

This predicts that the characteristic-cycle operation $CCRf_*{\cal F}$ agrees with the direct image of the characteristic cycle under the cotangent correspondence. The supplied text does not indicate whether the assertion has been proved or remains open.