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
7dece01e
Commit
7dece01e
authored
Sep 30, 2019
by
Benoit Viguier
Browse files
fix spec_map
parent
af8b4e4d
Changes
3
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
7dece01e
DIST
=
coq-verif-tweetnacl
NO_COLOR
=
"
\0
33[0m"
RED
=
"
\0
33[38;5;009m"
GREEN
=
"
\0
33[38;5;010m"
YELLOW
=
"
\0
33[38;5;011m"
ORANGE
=
"
\0
33[38;5;214m"
LIGHTPURPLE
=
"
\0
33[38;5;177m"
PURPLE
=
"
\0
33[38;5;135m"
CYAN
=
"
\0
33[38;5;014m"
LIGHTGRAY
=
"
\0
33[38;5;252m"
DARKGRAY
=
"
\0
33[38;5;242m"
BRIGHTRED
=
"
\0
33[91m"
BOLD
=
"
\0
33[1m"
all
:
coq-tweetnacl-spec coq-tweetnacl-vst
readme
:
less README.md
...
...
@@ -50,9 +63,16 @@ clean-paper:
# generate artefact
$(DIST)
:
@
echo
$(BOLD)$(ORANGE)
"Creating
$(DIST)
"
$(NO_COLOR)$(DARKGRAY)
mkdir
$(DIST)
dist
:
$(DIST)
$(DIST)/specs_map.pdf
:
@
echo
$(BOLD)$(YELLOW)
"Building map for specs"
$(NO_COLOR)$(DARKGRAY)
cd
paper
&&
$(MAKE)
specs_map.pdf
mv
specs_map.pdf
$(DIST)
/specs_map.pdf
dist
:
$(DIST) $(DIST)/specs_map.pdf
@
echo
$(BOLD)$(YELLOW)
"Preparing
$(DIST)
"
$(NO_COLOR)$(DARKGRAY)
cp
-r
proofs
$(DIST)
mkdir
$(DIST)
/packages
cp
-r
packages/coq-compcert
$(DIST)
/packages/
...
...
@@ -64,8 +84,12 @@ dist: $(DIST)
cp
README.md
$(DIST)
/
cp
Makefile
$(DIST)
/
cp
opam
$(DIST)
/
@
echo
$(BOLD)$(LIGHTPURPLE)
"Building
$(DIST)
.tar.gz"
$(NO_COLOR)$(DARKGRAY)
tar
-czvf
$(DIST)
.tar.gz
$(DIST)
@
echo
$(BOLD)$(GREEN)
"Done."
$(NO_COLOR)
clean-dist
:
$(DIST)
clean-dist
:
@
echo
$(BOLD)$(YELLOW)
"removing
$(DIST)
"
$(NO_COLOR)$(DARKGRAY)
rm
-r
$(DIST)
-
rm
$(DIST)
.tar.gz
rm
$(DIST)
.tar.gz
@
echo
$(BOLD)$(GREEN)
"Done."
$(NO_COLOR)
paper/Makefile
View file @
7dece01e
...
...
@@ -2,26 +2,39 @@ TEX := $(filter-out tweetverif.tex,$(wildcard *.tex))
FILES
:=
$(TEX)
$(
wildcard
tikz/
*
.tex
)
$(
wildcard
*
.sty
)
NO_COLOR
=
"
\0
33[0m"
RED
=
"
\0
33[31m"
RED
=
"
\0
33[38;5;009m"
GREEN
=
"
\0
33[38;5;010m"
YELLOW
=
"
\0
33[38;5;011m"
ORANGE
=
"
\0
33[38;5;214m"
LIGHTPURPLE
=
"
\0
33[38;5;177m"
PURPLE
=
"
\0
33[38;5;135m"
CYAN
=
"
\0
33[38;5;014m"
LIGHTGRAY
=
"
\0
33[38;5;252m"
DARKGRAY
=
"
\0
33[38;5;242m"
BRIGHTRED
=
"
\0
33[91m"
YELLOW
=
"
\0
33[93m"
ORANGE
=
"
\0
33[33m"
GRAY
=
"
\0
33[37m"
GREEN
=
"
\0
33[32m"
BOLD
=
"
\0
33[1m"
tweetverif.pdf
:
FORCE tweetverif.tex
@
echo
$(BOLD)$(GREEN)
"Building tweetverif.pdf"
$(NO_COLOR)
@
echo
$(BOLD)$(GREEN)
"Building tweetverif.pdf"
$(NO_COLOR)
$(DARKGRAY)
python3 latexrun.py tweetverif.tex
tweetverif.tex
:
FORCE $(FILES) collection.bib
@
echo
$(BOLD)$(YELLOW)
"Generating tweetverif.tex"
$(NO_COLOR)
@
echo
$(BOLD)$(YELLOW)
"Generating tweetverif.tex"
$(NO_COLOR)
$(DARKGRAY)
python3 gen.py tweetverif.tex
@
echo
$(BOLD)$(GREEN)
"Done."
$(NO_COLOR)
specs_map.pdf
:
FORCE _files.tex
@
echo
$(BOLD)$(GREEN)
"Building specs_map.pdf"
$(NO_COLOR)$(DARKGRAY)
python3 latexrun.py _files.tex
@
echo
$(BOLD)$(ORANGE)
"Moving specs_map.pdf to ../"
$(NO_COLOR)$(DARKGRAY)
@
mv
_files.pdf ../specs_map.pdf
depend
:
@
echo
$(FILES)
@
for
f
in
$(FILES)
;
do
\
echo
$$
f
;
\
done
.PHONY
:
clean FORCE
...
...
@@ -44,6 +57,6 @@ clean:
@
rm
tweetverif.tex 2> /dev/null
||
true
spell
:
for
f
in
$(TEX)
;
do
\
@
for
f
in
$(TEX)
;
do
\
aspell
-t
-c
$$
f
;
\
done
paper/_
A4_
files.tex
→
paper/_files.tex
View file @
7dece01e
% \todo{I don't think this belongs to the paper but more to the associated materials}
\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
}
% \subsection{Content of the proof files}
% \label{appendix:proof-files}
%
% We provide below the location of the most important definitions and lemmas of our proofs.
\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
}
% \subsubsection{Definitions}
% ~
\begin{document}
\begin{table*}
[h]
% \caption{Definitions}
% \label{table:specs}
\centering
\begin{tabular}
{
l | l | l
}
Definition
&
File
&
Description
\\
\hline
...
...
@@ -111,191 +120,4 @@
\hline
\end{tabular}
\end{table*}
% \subsubsection{Lemmas and Theorems}
% ~
% \begin{table}[h]
% \begin{tabular}{ l | l | l }
% Definition & File & Description \\
% \hline
% \end{tabular}
% \end{table}
% \subsection{Files}
%
% \begin{table}
% \begin{tabular}{ l | l }
% File & Content \\
% \hline
% \texttt{Gen/ABCDEF\_eq.v} & ... \\
% \texttt{Gen/ABCDEF.v} & ... \\
% \texttt{Gen/abstract\_fn\_rev\_abcdef.v} & ... \\
% \texttt{Gen/abstract\_fn\_rev\_eq.v} & ... \\
% \texttt{Gen/abstract\_fn\_rev.v} & ... \\
% \texttt{Gen/abstract\_rec\_rev\_abcdef.v} & ... \\
% \texttt{Gen/abstract\_rec\_rev\_eq.v} & ... \\
% \texttt{Gen/abstract\_rec\_rev.v} & ... \\
% \texttt{Gen/abstract\_rec.v} & ... \\
% \texttt{Gen/AMZubSqSel\_List.v} & ... \\
% \texttt{Gen/AMZubSqSel\_Prop.v} & ... \\
% \texttt{Gen/AMZubSqSel.v} & ... \\
% \texttt{Gen/Get\_abcdef.v} & ... \\
% \texttt{Gen/montgomery\_rec\_eq.v} & ... \\
% \texttt{Gen/montgomery\_rec.v} & ... \\
% \texttt{Gen/montgomery\_step\_gen.v} & ... \\
% \texttt{Gen/rec\_f\_extr.v} & ... \\
% \texttt{Gen/step\_gen.v} & ... \\
% \texttt{High/curve25519\_Fp2.v} & ... \\
% \texttt{High/curve25519\_Fp\_incl\_Fp2.v} & ... \\
% \texttt{High/curve25519\_Fp\_twist25519\_Fp\_eq.v} & ... \\
% \texttt{High/curve25519\_Fp.v} & ... \\
% \texttt{High/curve25519\_twist25519\_Fp\_incl\_Fp2.v} & ... \\
% \texttt{High/fermat.v} & ... \\
% \texttt{High/GRing\_tools.v} & ... \\
% \texttt{High/ladder.v} & ... \\
% \texttt{High/mcgroup.v} & ... \\
% \texttt{High/mc.v} & ... \\
% \texttt{High/montgomery.v} & ... \\
% \texttt{High/opt\_ladder\_extr.v} & ... \\
% \texttt{High/opt\_ladder.v} & ... \\
% \texttt{High/prime\_and\_legendre.v} & ... \\
% \texttt{High/prime\_cert.v} & ... \\
% \texttt{High/prime\_ssrprime.v} & ... \\
% \texttt{High/twist25519\_Fp\_incl\_Fp2.v} & ... \\
% \texttt{High/twist25519\_Fp.v} & ... \\
% \texttt{High/Zmodp2\_rules.v} & ... \\
% \texttt{High/Zmodp2.v} & ... \\
% \texttt{High/Zmodp\_Ring.v} & ... \\
% \texttt{High/Zmodp.v} & ... \\
% \texttt{Libs/Bound\_Decidable.v} & ... \\
% \texttt{Libs/Decidable.v} & ... \\
% \texttt{Libs/Export.v} & ... \\
% \texttt{Libs/Expr\_Decidable.v} & ... \\
% \texttt{Libs/Forall\_extended.v} & ... \\
% \texttt{Libs/Formula\_Decidable.v} & ... \\
% \texttt{Libs/Fun\_Decidable.v} & ... \\
% \texttt{Libs/HeadTailRec.v} & ... \\
% \texttt{Libs/LibTactics\_Rennes.v} & ... \\
% \texttt{Libs/LibTactics\_SF.v} & ... \\
% \texttt{Libs/LibTactics.v} & ... \\
% \texttt{Libs/List\_Decidable.v} & ... \\
% \texttt{Libs/List\_ext\_Decidable.v} & ... \\
% \texttt{Libs/List\_Ltac.v} & ... \\
% \texttt{Libs/Lists\_extended.v} & ... \\
% \texttt{Libs/Logic\_extended.v} & ... \\
% \texttt{Libs/Relations.v} & ... \\
% \texttt{Libs/Term\_Decidable.v} & ... \\
% \texttt{Libs/ZArith\_extended.v} & ... \\
% \texttt{ListsOp/Export.v} & ... \\
% \texttt{ListsOp/Forall\_ZofList.v} & ... \\
% \texttt{ListsOp/Forall\_ZopList.v} & ... \\
% \texttt{ListsOp/LogicalList.v} & ... \\
% \texttt{ListsOp/Zipp.v} & ... \\
% \texttt{ListsOp/ZofList.v} & ... \\
% \texttt{ListsOp/ZunopList.v} & ... \\
% \texttt{Low/AMZubSqSel\_Correct.v} & ... \\
% \texttt{Low/A.v} & ... \\
% \texttt{Low/BackCarry.v} & ... \\
% \texttt{Low/Binary\_select.v} & ... \\
% \texttt{Low/Car25519\_bounds.v} & ... \\
% \texttt{Low/Car25519.v} & ... \\
% \texttt{Low/Carry\_n.v} & ... \\
% \texttt{Low/Carry.v} & ... \\
% \texttt{Low/Constant.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_lemmas\_List\_List16.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_lemmas.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_lemmas\_Z\_List16.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_.v} & ... \\
% \texttt{Low/Export.v} & ... \\
% \texttt{Low/Get\_abcdef.v} & ... \\
% \texttt{Low/GetBit\_pack25519.v} & ... \\
% \texttt{Low/GetBit.v} & ... \\
% \texttt{Low/Inner\_M1.v} & ... \\
% \texttt{Low/Inv25519\_gen.v} & ... \\
% \texttt{Low/Inv25519.v} & ... \\
% \texttt{Low/List16.v} & ... \\
% \texttt{Low/M\_low\_level\_compute.v} & ... \\
% \texttt{Low/M.v} & ... \\
% \texttt{Low/Outer\_M1.v} & ... \\
% \texttt{Low/Pack25519.v} & ... \\
% \texttt{Low/Pack.v} & ... \\
% \texttt{Low/Prep\_n.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_aux.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_1b.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_1.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_2b.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_2.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_step.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose.v} & ... \\
% \texttt{Low/Reduce\_by\_P.v} & ... \\
% \texttt{Low/ScalarMult\_gen\_small.v} & ... \\
% \texttt{Low/ScalarMult\_rev\_fn\_gen.v} & ... \\
% \texttt{Low/ScalarMult\_rev.v} & ... \\
% \texttt{Low/Sel25519.v} & ... \\
% \texttt{Low/S.v} & ... \\
% \texttt{Low/Unpack25519.v} & ... \\
% \texttt{Low/Z.v} & ... \\
% \texttt{Mid/AMZubSqSel.v} & ... \\
% \texttt{Mid/Car25519.v} & ... \\
% \texttt{Mid/Crypto\_Scalarmult\_Fp.v} & ... \\
% \texttt{Mid/Crypto\_Scalarmult\_Mod.v} & ... \\
% \texttt{Mid/Crypto\_Scalarmult.v} & ... \\
% \texttt{Mid/Export.v} & ... \\
% \texttt{Mid/GetBit\_bitn.v} & ... \\
% \texttt{Mid/GetBit.v} & ... \\
% \texttt{Mid/Instances.v} & ... \\
% \texttt{Mid/Inv25519.v} & ... \\
% \texttt{Mid/MinusList.v} & ... \\
% \texttt{Mid/M\_low\_level.v} & ... \\
% \texttt{Mid/Mod.v} & ... \\
% \texttt{Mid/M.v} & ... \\
% \texttt{Mid/Pack25519.v} & ... \\
% \texttt{Mid/Prep\_n.v} & ... \\
% \texttt{Mid/Reduce.v} & ... \\
% \texttt{Mid/ScalMult.v} & ... \\
% \texttt{Mid/SubList.v} & ... \\
% \texttt{Mid/SumList.v} & ... \\
% \texttt{Mid/Unpack25519.v} & ... \\
% \texttt{Mid/ZCarry.v} & ... \\
% \end{tabular}
% \end{table}
%
% \begin{table}
% \begin{tabular}{ l | l }
% File & Content \\
% \hline
% \texttt{c/tweetnaclVerifiableC.v} & \\
% \texttt{init/init\_tweetnacl.v} & \\
% \texttt{init/missing\_lemmae.v} & \\
% \texttt{proofs/split\_array\_lemmas.v} & \\
% \texttt{proofs/verif\_A.v} & \\
% \texttt{proofs/verif\_car25519\_compute.v} & \\
% \texttt{proofs/verif\_car25519.v} & \\
% \texttt{proofs/verif\_crypto\_scalarmult\_lemmas.v} & \\
% \texttt{proofs/verif\_crypto\_scalarmult.v} & \\
% \texttt{proofs/verif\_inv25519.v} & \\
% \texttt{proofs/verif\_M\_compute\_pre.v} & \\
% \texttt{proofs/verif\_M\_compute.v} & \\
% \texttt{proofs/verif\_M\_lemmas.v} & \\
% \texttt{proofs/verif\_M.v} & \\
% \texttt{proofs/verif\_pack25519\_lemmas.v} & \\
% \texttt{proofs/verif\_pack25519.v} & \\
% \texttt{proofs/verif\_sel25519.v} & \\
% \texttt{proofs/verif\_set25519.v} & \\
% \texttt{proofs/verif\_S.v} & \\
% \texttt{proofs/verif\_unpack25519.v} & \\
% \texttt{proofs/verif\_Z.v} & \\
% \texttt{spec/spec\_A.v} & \\
% \texttt{spec/spec\_car25519.v} & \\
% \texttt{spec/spec\_crypto\_scalarmult.v} & \\
% \texttt{spec/spec\_inv25519.v} & \\
% \texttt{spec/spec\_M.v} & \\
% \texttt{spec/spec\_pack25519.v} & \\
% \texttt{spec/spec\_sel25519.v} & \\
% \texttt{spec/spec\_set25519.v} & \\
% \texttt{spec/spec\_S.v} & \\
% \texttt{spec/spec\_unpack25519.v} & \\
% \texttt{spec/spec\_Z.v} & \\
% \end{tabular}
% \end{table}
\end{document}
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