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
bc40eda7
Commit
bc40eda7
authored
Sep 30, 2019
by
Benoit Viguier
Browse files
Small typos
parent
7ee3cf60
Changes
2
Hide whitespace changes
Inline
Side-by-side
paper/4_lowlevel.tex
View file @
bc40eda7
...
...
@@ -382,10 +382,10 @@ applied (chapter 15 in \cite{CpdtJFR}).
The idea is to
\emph
{
reflect
}
the goal into a decidable environment.
We show that for a property
$
P
$
, we can define a decidable Boolean property
$
P
_{
bool
}$
such that if
$
P
_{
bool
}$
is
\Coqe
{
true
}
then
$
P
$
holds.
$$
reify
\_
P : P
_{
bool
}
=
true
\implies
P
$$
By applying
$
reify
\_
P
$
on
$
P
$
our goal become
$
P
_{
bool
}
=
true
$
.
$$
\text
{
\textit
{
reify
\_
P
}}
: P
_{
bool
}
=
\text
{
\textit
{
true
}}
\implies
P
$$
By applying
\textit
{
reify
\_
P
}
on
$
P
$
our goal become
$
P
_{
bool
}
=
true
$
.
We then compute the result of
$
P
_{
bool
}$
. If the decision goes well we are
left with the tautology
$
true
=
true
$
.
left with the tautology
$
\text
{
\textit
{
true
}}
=
\text
{
\textit
{
true
}}
$
.
With this technique we prove the functional correctness of the inversion over
\Zfield
.
\begin{lemma}
...
...
paper/5_highlevel.tex
View file @
bc40eda7
...
...
@@ -187,6 +187,8 @@ Definition ec_of_mc p :=
Lemma ec
_
of
_
mc
_
bij : bijective ec
_
of
_
mc.
\end{lstlisting}
% We use this isomorphism to derive that $(M_{a,b}(\K), + )$ is a group.
\subsubsection
{
Projective coordinates
}
\label
{
subsec:ECC-projective
}
...
...
@@ -272,7 +274,7 @@ we can define a ladder similar to the one used in TweetNaCl (See \aref{alg:montg
\ENSURE
{$
a
/
c
=
\chi
_
0
(
n
\cdot
P
)
$
for any
$
P
$
such that
$
\chi
_
0
(
P
)
=
x
$}
\STATE
$
(
a,c
)
\leftarrow
(
1
,
0
)
$
~~~~~~~~~~~~~~~
{
\color
{
gray
}
\textit
{$
\chi
_
0
(
\Oinf
)
=
(
1
:
0
)
$}}
\STATE
$
(
b,d
)
\leftarrow
(
x,
1
)
$
~~~~~~~~~~~~~~~
{
\color
{
gray
}
\textit
{$
\chi
_
0
(
P
)
=
(
x:
1
)
$}}
\FOR
{$
k
$
:=
$
m
$
downto
$
1
$}
\FOR
{$
k
$
:=
$
m
$
\textbf
{
downto
}
$
1
$}
\IF
{$
k
^{
\text
{
th
}}$
bit of
$
n
$
is
$
1
$}
\STATE
$
(
a,b
)
\leftarrow
(
b,a
)
$
\STATE
$
(
c,d
)
\leftarrow
(
d,c
)
$
...
...
@@ -493,7 +495,7 @@ of formulas by using rewrite rules:
\qquad
\begin{split}
(a,0)
\cdot
(b,0)
&
= (a
\cdot
b, 0)
\\
(0,a)
^{
-1
}
&
= ((2
\cdot
a)
^{
-1
}
,0
)
\\
(0,a)
^{
-1
}
&
= (
0,
(2
\cdot
a)
^{
-1
}
)
\\
% (0, a)\cdot (0,b) &= (2\cdot a\cdot b, 0)\\
~
\\
\end{split}
...
...
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