Skip to content

GitLab

Commit b4906681 authored by benoit's avatar benoit
Browse files

minor fixes, remove generation script for _reviews.tex

parent 040187ba
Hide whitespace changes
Inline Side-by-side
paper/1-intro.tex
View file @ b4906681
......@@ -136,11 +136,10 @@ effort required to extend our work to other elliptic-curve software.
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
C source files are represented by {\color{doc@lstfunctions}.C} while
{\color{doc@lstfunctions}.V} corresponds to Coq files.
\todo{Double Check (new)}
In a nutshell, we formalize X25519 into a Coq function \texttt{RFC},
and we write a specification in Separation logic with VST.
The first step of CompCert compilation (clightgen) is used to translates
the C source code into a DSL (CLight). By using VST,
the C source code into a DSL in Coq (CLight). By using VST,
we step through the translated instructions and verify that the program satisfies the specifications.
Additionally we formally define the scalar multiplication over elliptic curves and show that,
under the same preconditions as used in the specification, \texttt{RFC} computes the desired results
......
paper/4.1-VST.tex
View file @ b4906681
......@@ -9,9 +9,7 @@
\subheading{Specifications.}
We show the soundness of TweetNaCl by proving a correspondence between
the C version of TweetNaCl and the same code as a pure Coq function.
\todo{same code => to fix}
the C version of TweetNaCl and a pure function in Coq formalizing the RFC.
% why "pure" ?
% A pure function is a function where the return value is only determined by its
% input values, without observable side effects (Side effect are e.g. printing)
......
paper/5-highlevel.tex
View file @ b4906681
......@@ -34,7 +34,7 @@ with it in the proofs (\ref{subsec:curvep2}).
\label{subsec:ECC}
\fref{tikz:ProofHighLevel1} presents the structure of the proof of the ladder's
correctness. The white tiles are definitions, the orange one are hypothesis and
correctness. The white tiles are definitions, the orange ones are hypothesis and
the green tiles represent major lemmas and theorems.
We consider elliptic curves over a field $\K$. We assume that the
......@@ -51,6 +51,7 @@ $a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref
\label{tikz:ProofHighLevel1}
\end{figure}
We now turn our attention to the details of the proof.
\begin{dfn}
Given a field $\K$,
......
paper/Makefile
View file @ b4906681
TEX := $(filter-out tweetverif.tex,$(wildcard *.tex))
FILES := $(TEX) $(wildcard tikz/*.tex) $(wildcard *.sty)
REVIEWS := $(filter-out _reviews.tex,$(TEX)) $(wildcard _reviews/*.tex) $(wildcard *.sty)
REVIEWS := _reviews.tex $(wildcard _reviews/*.tex) $(wildcard *.sty)
NO_COLOR="\033[0m"
RED = "\033[38;5;009m"
......@@ -69,7 +69,6 @@ clean:
@rm */*.aux 2> /dev/null || true
@rm tweetverif.tex 2> /dev/null || true
@rm tweetnacl.diff 2> /dev/null || true
@rm _reviews.tex 2> /dev/null || true
# CHECK SPELLING
spell:
......@@ -84,16 +83,11 @@ feedback.pdf:
python3 latexrun.py _includes/_feedback.tex
@mv _feedback.pdf feedback.pdf
reviews.pdf: FORCE _reviews.tex _tpl_reviews.tex $(REVIEWS)
reviews.pdf: FORCE _reviews.tex $(REVIEWS)
@echo $(BOLD)$(LIGHTPURPLE)"Building reviews.pdf"$(NO_COLOR)$(DARKGRAY)
python3 latexrun.py _reviews.tex
@mv _reviews.pdf reviews.pdf
_reviews.tex: FORCE _tpl_reviews.tex $(REVIEWS)
@echo $(BOLD)$(YELLOW)"Generating _reviews.tex"$(NO_COLOR)$(DARKGRAY)
python3 gen_reviews.py _reviews.tex
# SPEC MAPS
specs_map.pdf: FORCE _files.tex
@echo $(BOLD)$(LIGHTPURPLE)"Building specs_map.pdf"$(NO_COLOR)$(DARKGRAY)
......
paper/_reviews/A4_reviews-UsenixA.tex
View file @ b4906681
......@@ -140,13 +140,11 @@ Here are a few linear comments:
\item \textbf{page 6, column 1:}\\
In ListofZn\_fp $\rightarrow$ The use of fuel might deserve a comment. Don't you end up having to prove at some point that you can always compute ahead of time an overapproximation of the fuel needed? Wouldn't it have been simple to use the strong recursion principle of naturals to define the function?
\end{itemize}
\begin{answer}{EEEEEE}
In our case the fuel is used to garantee to have as an output a list of 32 elements. This allows to prove that for all List of 32 bytes, ListofZn\_fp (ZofList L) = L. With this lemma at hand we can later simplify some of the expressions.
\end{answer}
\begin{answer}{EEEEEE}
In our case the fuel is used to garantee to have as an output a list of 32 elements. This allows to prove that for all List of 32 bytes, ListofZn\_fp (ZofList L) = L. With this lemma at hand we can later simplify some of the expressions.
\end{answer}
\begin{itemize}
\item \textbf{page 6, column 2:}\\
"and the same code as a pure Coq function" $\rightarrow$ I would rephrase, the term "same code" is misleading.
Specification: I think explaining the structure of a VST statement would be necessary to help an unfamiliar reader understand this specification.
......
paper/_tpl_reviews.tex deleted 100644 → 0
View file @ 040187ba
\documentclass{article}
\usepackage[a4paper, total={6in, 8in}]{geometry}
\newif\ifusenix
\newif\ifacm
\newif\ifieee
\newif\ifpublic
\usenixfalse
\acmfalse
\ieeetrue
\usepackage[final]{pdfpages}
\usepackage{epsfig}
\usepackage{setup}
\input{_macros}
\begin{document}
\input{_todo}
%don't want date printed
\date{}
\intput{main}
\newpage
\pagestyle{empty}
\includepdf[pages=1,pagecommand=\label{paper:usenix}]{tweetverif-USENIX.pdf}
\includepdf[pages=2-]{tweetverif-USENIX.pdf}
\end{document}
paper/gen_reviews.py deleted 100644 → 0
View file @ 040187ba
#!/usr/bin/env python3
import os
import glob
import argparse
from string import Template
def save(fn, z):
# print(z)
d = open(fn, 'w', encoding="utf-8")
d.write(z)
d.close()
def read(fn):
data = ''
with open(fn, 'r', encoding="utf-8") as file:
data = file.read()
return data
def is_tex(fn):
return fn[-4:] == '.tex'
def is_ignored(fn):
return fn[0:1] == '_'
def is_appendix(fn):
return fn[0:1] == 'A'
def is_not_tex(s):
return s != '' and s[-4:] != '.tex'
def is_not_tikz(s):
return "tikz/" not in s
def check_tex(s):
if is_not_tex(s):
msg = "%r is not a .tex" % s
raise argparse.ArgumentTypeError(msg)
return s
def parse_arguments():
parser = argparse.ArgumentParser(description='Generate paper.')
parser.add_argument('input', nargs=1, default='', help='input: paper.tex', type=check_tex)
args = parser.parse_args()
return args.input[0]
def main():
fn = parse_arguments()
files = [x for x in glob.glob("_reviews/*.tex", recursive=True) if is_tex(x) and not (x == fn) and is_not_tikz(x)]
# for f in files:
# print(f)
files.sort()
main_output = ''
for f in files:
main_output += "\\input{{{}}}\n".format(f)
appendix_output = ''
output = read('_tpl' + fn)
output = output.replace('\\intput{main}\n', '$main_output')
output = Template(output)
output = output.safe_substitute(main_output = main_output, appendix_output = appendix_output)
# print(output)
save(fn, output)
main()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment