_files.tex 6.86 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
\documentclass[8pt]{extarticle}
\usepackage[a4paper,margin=1cm]{geometry}
\usepackage{epsfig}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[switch]{lineno}
\usepackage[pdf]{pstricks}
\usepackage{amsfonts,amsmath,amscd,amscd,amssymb,array}
\usepackage{xspace}

\newcommand{\p}{\ensuremath{2^{255}-19}}
\newcommand{\Zfield}{\ensuremath{\mathbb{Z}_{\p}}}
\newcommand{\Ffield}{\ensuremath{\mathbb{F}_{\p}}}
\newcommand{\Z}{\ensuremath{\mathbb{Z}}\xspace}
\newcommand{\K}{\ensuremath{\mathbb{K}}\xspace}
\newcommand{\F}[1]{\ensuremath{\mathbb{F}_{#1}}\xspace}
\pagenumbering{gobble}

\begin{document}
\begin{table*}[h]
  \centering
  \begin{tabular}{ l | l | l }
    Definition & File & Description \\
    \hline
    \texttt{ZofList} & \texttt{ListsOp/ZofList.v} & \Z $\rightarrow$ List \Z $\rightarrow$ \Z\\
    \texttt{ListofZ32} & \texttt{ListsOp/ListofZ.v} & \Z $\rightarrow$  \Z $\rightarrow$ list \Z\\
    \hline
    \multicolumn{3}{c}{Elliptic Curve \& Fields }\\
    \hline
    \texttt{mcuType} & \texttt{High/mc.v} & $M_{a,b}$ \\
    % \texttt{oncurve} & \texttt{High/mc.v} & Boolean decision of a point on a curve \\
    \texttt{mc} & \texttt{High/mc.v} & $M_{a,b}(\K)$ \\
    \texttt{neg} & \texttt{High/mc.v} & Negation \\
    \texttt{add} & \texttt{High/mc.v} & Addition \\
    \texttt{ec\_of\_mc} & \texttt{High/mcgroup.v} & $M_{a,b}(\K) \mapsto E(\K)$ \\
    \texttt{mc\_of\_ec} & \texttt{High/mcgroup.v} & $E(\K) \mapsto M_{a,b}(\K)$ \\
    \texttt{point\_x0} & \texttt{High/montgomery.v} & $\chi_0 : M_{a,b}(\K) \to \K$ \\
    \texttt{point\_x} & \texttt{High/montgomery.v} & $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$ \\
    % \texttt{mcu\_no\_square} & \texttt{High/montgomery.v} & $a^2-4$ is not a square in \K \\
    \texttt{cswap} & \texttt{High/opt\_ladder.v} & Conditional swap \\
    \texttt{opt\_montgomery} & \texttt{High/opt\_ladder.v} & Montgomery over \K \\
    % \texttt{mcu\_no\_square} & \texttt{High/opt\_ladder.v} & $a^2-4$ is not a square in \K \\
    \texttt{Zmodp.type} & \texttt{High/Zmodp.v} & $\F{p}$ with $p = \p$ \\
    \texttt{Zmodp2.type} & \texttt{High/Zmodp2.v} & $\F{p^2}$ with $p = \p$ \\
    \texttt{curve25519\_Fp\_ladder} & \texttt{High/curve25519\_Fp.v} & Montgomery ladder for the curve $M_{486662,1}$ over \F{p} \\
    \texttt{curve25519\_Fp\_to\_Fp2} & \texttt{High/curve25519\_Fp\_incl\_Fp2.v} & $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$ \\
    \texttt{twist25519\_Fp\_ladder} & \texttt{High/twist25519\_Fp.v} & Montgomery ladder for the quadratic twist $M_{486662,2}$ over \F{p} \\
    \texttt{twist25519\_Fp\_to\_Fp2} & \texttt{High/twist25519\_Fp\_incl\_Fp2.v} & $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$ \\
    % \texttt{primo} & \texttt{High/prime\_cert.v} & $\p$ is prime \\
    \hline
    \multicolumn{3}{c}{Generic ladder}\\
    \hline
    \texttt{get\_a} & \texttt{Gen/Get\_abcdef.v} & $(a,b,c,d,e,f) \mapsto a$ \\
    \texttt{get\_c} & \texttt{Gen/Get\_abcdef.v} & $(a,b,c,d,e,f) \mapsto c$ \\
    \texttt{Ops.A} & \texttt{Gen/AMZubSqSel.v} & Addition \\
    \texttt{Ops.M} & \texttt{Gen/AMZubSqSel.v} & Multiplication \\
    \texttt{Ops.Zub} & \texttt{Gen/AMZubSqSel.v} & Subtraction \\
    \texttt{Ops.Sq} & \texttt{Gen/AMZubSqSel.v} & Squaring \\
    \texttt{Ops.C\_0} & \texttt{Gen/AMZubSqSel.v} & Constant $0$ \\
    \texttt{Ops.C\_1} & \texttt{Gen/AMZubSqSel.v} & Constant $1$ \\
    \texttt{Ops.C\_121665} & \texttt{Gen/AMZubSqSel.v} & Constant $121665$ \\
    \texttt{Ops.Sel25519} & \texttt{Gen/AMZubSqSel.v} & Conditional swap \\
    \texttt{Ops.Getbit} & \texttt{Gen/GetBit.v} & Bit selection \\
    \texttt{montgomery\_rec} & \texttt{Gen/montgomery\_rec.v} & Montgomery ladder \\
    \hline
    \multicolumn{3}{c}{Operations over \Z and \Zfield}\\
    \hline
    \texttt{Mid.A} & \texttt{Mid/AMZubSqSel.v} & Addition \\
    \texttt{Mid.M} & \texttt{Mid/AMZubSqSel.v} & Multiplication \\
    \texttt{Mid.Zub} & \texttt{Mid/AMZubSqSel.v} & Subtraction \\
    \texttt{Mid.Sq} & \texttt{Mid/AMZubSqSel.v} & Squaring \\
    \texttt{Mid.C\_0} & \texttt{Mid/AMZubSqSel.v} & Constant $0$ \\
    \texttt{Mid.C\_1} & \texttt{Mid/AMZubSqSel.v} & Constant $1$ \\
    \texttt{Mid.C\_121665} & \texttt{Mid/AMZubSqSel.v} & Constant $121665$ \\
    \texttt{Mid.Sel25519} & \texttt{Mid/AMZubSqSel.v} & Conditional swap \\
    \texttt{Mid.car25519} & \texttt{Mid/Car25519.v} & Carry propagation \\
    \texttt{Mid.getbit} & \texttt{Mid/GetBit.v} & Bit selection \\
    \texttt{Inv25519\_Z} & \texttt{Mid/Inv25519.v} & $x^{2^{255}-21}$ \\
    \texttt{ZInv25519} & \texttt{Mid/Inv25519.v} & power computed recursively \\
    \texttt{modP} & \texttt{Mid/Mod.v} & mod \p\\
    \texttt{ZPack25519} & \texttt{Mid/Pack25519.v} & packing mod \p\\
    \texttt{Zclamp} & \texttt{Mid/Prep\_n.v} & Clamping \\
    \texttt{ZUnpack25519} & \texttt{Mid/Unpack25519.v} & unpacking (mod $2^{255}$)\\
    \hline
    \multicolumn{3}{c}{Operations over list of \Z}\\
    \hline
    \texttt{Low.A} & \texttt{Low/A.v} & Addition \\
    \texttt{Low.M} & \texttt{Low/M.v} & Multiplication \\
    \texttt{Low.Z} & \texttt{Low/Z.v} & Subtraction \\
    \texttt{Low.S} & \texttt{Low/S.v} & Squaring \\
    \texttt{Low.C\_0} & \texttt{Low/Constant.v} & Constant $0$ \\
    \texttt{Low.C\_1} & \texttt{Low/Constant.v} & Constant $1$\\
    \texttt{Low.C\_121665} & \texttt{Low/Constant.v} & Constant $121665$\\
    \texttt{Low.C\_25519} & \texttt{Low/Constant.v} & Constant $2^{255}-19$\\
    \texttt{Low.Sel25519} & \texttt{Low/Sel25519.v} & Conditional swap \\
    \texttt{car25519} & \texttt{Low/Car25519.v} & Carry propagation \\
    \texttt{Low.getbit} & \texttt{Low/GetBit.v} & Bit selection \\
    \texttt{Inv25519} & \texttt{Low/Inv25519.v} & Recursive power \\
    \texttt{Pack25519} & \texttt{Low/Pack25519.v} & packing mod \p\\
    \texttt{clamp} & \texttt{Low/Prep\_n.v} & Clamping \\
    \texttt{Unpack25519} & \texttt{Low/Unpack25519.v} & unpacking (mod $2^{255}$)\\
    \hline
Benoit Viguier's avatar
Benoit Viguier committed
103
    \multicolumn{3}{c}{Instantiation of \texttt{Ops}}\\
Benoit Viguier's avatar
Benoit Viguier committed
104
    \hline
Benoit Viguier's avatar
Benoit Viguier committed
105
106
107
    \texttt{Z25519\_Ops} & \texttt{Mid/Instances.v} & Instantiation over \F{p} with $p = \p$\\
    \texttt{Z\_Ops} & \texttt{Mid/Instances.v} & Instantiation over $\Zfield$ \\
    \texttt{List\_Z\_Ops} & \texttt{Mid/Instances.v} & Instantiation lists of \Z \\
Benoit Viguier's avatar
Benoit Viguier committed
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
    \hline
    \multicolumn{3}{c}{X25519 over \Z and list of \Z}\\
    \hline
    \texttt{ZCrypto\_Scalarmult} & \texttt{Mid/Crypto\_Scalarmult.v} & integers specification of X25519\\
    \texttt{Crypto\_Scalarmult} & \texttt{Low/Crypto\_Scalarmult.v} & list specification of X25519\\
    \hline
    \multicolumn{3}{c}{RFC~7748}\\
    \hline
    \texttt{decodeScalar25519} & \texttt{rfc/rfc.v} & Decode the scalar\\
    \texttt{decodeUCoordinate} & \texttt{rfc/rfc.v} & Decode the x-coordinate\\
    \texttt{encodeUCoordinate} & \texttt{rfc/rfc.v} & Encode the resulting x-coordinate\\
    \texttt{RFC} & \texttt{rfc/rfc.v} & specification of X25519 as in RFC~7748\\
    \hline
\end{tabular}
\end{table*}
\end{document}