Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
bb892287
Commit
bb892287
authored
Feb 15, 2020
by
Benoit Viguier
Browse files
small fixes
parent
bd36aef0
Changes
2
Hide whitespace changes
Inline
Side-by-side
paper/A4_reviews.tex
View file @
bb892287
...
...
@@ -444,7 +444,7 @@ specification.
\centering
\include
{
tikz/mit
}
\caption
{
Our approach vs
\mitp
}
\label
{
tikz:
Low
VST
}
\label
{
tikz:
Mit
VST
}
\end{figure}
\end{answer}
...
...
paper/_files.tex
View file @
bb892287
...
...
@@ -25,6 +25,22 @@
\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
}{
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
\\
\texttt
{
montgomery
\_
rec
\_
swap
}
&
\texttt
{
Gen/montgomery
\_
rec
\_
swap.v
}
&
Montgomery ladder
\\
\hline
\multicolumn
{
3
}{
c
}{
Elliptic Curve
\&
Fields
}
\\
\hline
\texttt
{
mcuType
}
&
\texttt
{
High/mc.v
}
&
$
M
_{
a,b
}$
\\
...
...
@@ -48,21 +64,6 @@
\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
\\
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment