DecodingFunction #
This file exposes the total field-to-curve map from Definition 2 of the Elligator paper under the
name DecodingFunction. The underlying construction is ϕ: it maps t = ±1 to (0, 1) and,
for every other t, returns the coordinates constructed in Theorem 1.
Main results #
DecodingFunction: the Elligator 1 decoding mapF → F × F, obtained from the curve-valued mapϕby forgetting its proof of curve membership.
References #
See [bernstein2013a], Section 3.2, Definition 2.
def
Elligator.Elligator1.DecodingFunction
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{s : F}
{q : ℕ}
(t : F)
(hs_ne_zero : s ≠ 0)
(sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(hq_card : Fintype.card F = q)
(hq_mod : q % 4 = 3)
:
The decoding function for the complete Edwards curve
Equations
- Elligator.Elligator1.DecodingFunction t hs_ne_zero sq_ne_pm_two hq_card hq_mod = ↑(Elligator.Elligator1.ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod)