That is, prove the concrete indifferentiability relation $\mathsf{mapHashOutputsToCurve} \circ \mathsf{hash\_to\_field}(·, 2) {\large ⊏}_c \mathsf{hash\_to\_field}(·, 2)$, where $\mathsf{hash\_to\_field}(·, 2) ⦂ \mathcal{D} \rightarrow (\mathbb{F}_{q_{\mathbb{G}}})^2$ for $\mathcal{D}$ a suitable input type (domain separator and byte sequence), and $\mathsf{mapHashOutputsToCurve}$ as formalized in #19. This follows Brier et al.'s Theorem 1; it will require the form of the Weil bound defined in Curves.Hashing.WellDistributed as a named hypothesis, and consume TwoTermUniformity as the regularity half.
That is, prove the concrete indifferentiability relation$\mathsf{mapHashOutputsToCurve} \circ \mathsf{hash\_to\_field}(·, 2) {\large ⊏}_c \mathsf{hash\_to\_field}(·, 2)$ , where $\mathsf{hash\_to\_field}(·, 2) ⦂ \mathcal{D} \rightarrow (\mathbb{F}_{q_{\mathbb{G}}})^2$ for $\mathcal{D}$ a suitable input type (domain separator and byte sequence), and $\mathsf{mapHashOutputsToCurve}$ as formalized in #19. This follows Brier et al.'s Theorem 1; it will require the form of the Weil bound defined in
Curves.Hashing.WellDistributedas a named hypothesis, and consumeTwoTermUniformityas the regularity half.