Add a missing cross reference for Jubjub.

Signed-off-by: Daira Hopwood <daira@jacaranda.org>
This commit is contained in:
Daira Hopwood 2020-07-06 22:57:41 +01:00
parent 5e8ae9bb89
commit 4d148920ae
1 changed files with 2 additions and 1 deletions

View File

@ -7919,7 +7919,8 @@ Let $\ellJ := 256$.
\introlist
Define $\ItoLEBSP{} \typecolon (\ell \typecolon \Nat) \times \binaryrange{\ell} \rightarrow \bitseq{\ell}$
as in \crossref{endian}.
as in \crossref{endian}, and similarly for
$\LEBStoIP{} \typecolon (\ell \typecolon \Nat) \times \bitseq{\ell} \rightarrow \binaryrange{\ell}$.
Define $\reprJ \typecolon \GroupJ \rightarrow \ReprJ$ such
that $\reprJ\Of{u, \varv} = \ItoLEBSP{256}\big(\varv + 2^{255} \smult \tilde{u}\big)$, where