Commit 5f42e498 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

generate the tex file via python: order of files is determined by their name.

parent 3251f5af
\documentclass{article}
\usepackage{geometry}
\geometry{
a4paper,
total={190mm,257mm},
left=10mm,
top=20mm,
}
\usepackage{epsfig}
\usepackage{setup}
\input{macros}
\begin{document}
Generic definition of the ladder:
\begin{lstlisting}[language=Coq]
(* Define a typeclass to encapsulate the operations *)
Class Ops (T T': Type) (Mod: T -> T):=
{
+ : T -> T -> T; (* Add *)
* : T -> T -> T; (* Mult *)
- : T -> T -> T; (* Sub *)
x^2 : T -> T; (* Square *)
C_0 : T; (* Const 0 *)
C_1 : T; (* Const 1 *)
C_121665: T; (* const (a-2)/4 *)
Sel25519: Z -> T -> T -> T;(* CSWAP *)
Getbit: Z -> T' -> Z; (* ith bit *)
}.
Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *)
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(T * T * T * T * T * T) :=
match m with
| 0%nat => (a,b,c,d,e,f)
| S n =>
let r := Getbit (Z.of_nat n) z in
(* k_t = (k >> t) & 1 *)
(* swap <- k_t *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2 + z_2 *)
let a := a - c in (* B = x_2 - z_2 *)
let c := b + d in (* C = x_3 + z_3 *)
let b := b - d in (* D = x_3 - z_3 *)
let d := e ^2 in (* AA = A^2 *)
let f := a ^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3 = (DA + CB)^2 --- (1/2) *)
let a := a - c in (* z_3 = x_1 * (DA - CB)^2 --- (1/3) *)
let b := a ^2 in (* z_3 = x_1 * (DA - CB)^2 --- (2/3) *)
let c := d - f in (* E = AA - BB *)
let a := c * C_121665 in (* z_2 = E * (AA + a24 * E) --- (1/3) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) --- (2/3) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) --- (3/3) *)
let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1 * (DA - CB)^2 --- (3/3) *)
let b := e ^2 in (* x_3 = (DA + CB)^2 --- (2/2) *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
montgomery_rec n z a b c d e f x
end.
Definition get_a (t:(T * T * T * T * T * T)) : T :=
match t with
(a,b,c,d,e,f) => a
end.
Definition get_c (t:(T * T * T * T * T * T)) : T :=
match t with
(a,b,c,d,e,f) => c
end.
\end{lstlisting}
\newpage
Instanciation of the Class \Coqe{Ops} with operations over $\Z$ and modulo \p.
\begin{lstlisting}[language=Coq]
Definition modP x := Z.modulo x (Z.pow 2 255 - 19).
(* Encapsulate in a module. *)
Module Mid.
Definition getCarry (m:Z) : Z := Z.shiftr m n.
Definition getResidue (m:Z) : Z := m - Z.shiftl (getCarry m) n.
Definition car25519 (n:Z) : Z := 38 * getCarry 256 n + getResidue 256 n.
(* The carry operation is invariant under modulo *)
Lemma Zcar25519_correct: forall n, n:GF = (Mid.car25519 n) :GF.
(* Define Mid.A, Mid.M ... *)
Definition A a b := Z.add a b.
Definition M a b := Mid.car25519 (Mid.car25519 (Z.mul a b)).
Definition Zub a b := Z.sub a b.
Definition Sq a := M a a.
Definition C_0 := 0.
Definition C_1 := 1.
Definition C_121665 := 121665.
Definition Sel25519 (b p q:Z) := if (Z.eqb b 0) then p else q.
Definition getbit (i:Z) (a: Z) :=
if (Z.ltb a 0) then
0
else
if (Z.ltb i 0) then
Z.land a 1
else
Z.land (Z.shiftr a i) 1.
End Mid.
Definition ZPack25519 n :=
Z.modulo n (Z.pow 2 255 - 19).
Definition Zclamp (n : Z) : Z :=
(Z.lor (Z.land n (Z.land (Z.ones 255) (-8))) (Z.shiftl 64 (31 * 8))).
(* x^{p - 2} *)
Definition ZInv25519 (x:Z) : Z := Z.pow x (Z.pow 2 255 - 21).
(* instantiate over Z *)
Instance Z_Ops : (Ops Z Z modP) := {}.
Proof.
apply Mid.A. (* instantiate + *)
apply Mid.M. (* instantiate * *)
apply Mid.Zub. (* instantiate - *)
apply Mid.Sq. (* instantiate x^2 *)
apply Mid.C_0. (* instantiate Const 0 *)
apply Mid.C_1. (* instantiate Const 1 *)
apply Mid.C_121665. (* instantiate (a-2)/4 *)
apply Mid.Sel25519. (* instantiate CSWAP *)
apply Mid.getbit. (* instantiate ith bit *)
Defined.
(* instantiate montgomery_rec with Z_Ops *)
Definition ZCrypto_Scalarmult n p :=
let t := montgomery_rec
255 (* iterate 255 times *)
(Zclamp n) (* clamped n *)
1 (* x_2 *)
(ZUnpack25519 p) (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
(ZUnpack25519 p) (* x_1 *) in
ZPack25519 (Z.mul (get_a t) (ZInv25519 (get_c t))).
\end{lstlisting}
\newpage
\begin{lstlisting}[language=Coq]
Definition Crypto_Scalarmult n p :=
let t := (montgomery_rec 255
(clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1
Low.C_0 Low.C_0 (Unpack25519 p)) in
let a := get_a t in
let c := get_c t in
Pack25519 (Low.M a (Inv25519 c)).
Definition CSM := Crypto_Scalarmult.
Theorem Crypto_Scalarmult_Eq : forall (n p:list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p ->
ZofList 8 (Crypto_Scalarmult n p) =
ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
\end{lstlisting}
\end{document}
TEX := $(wildcard *.tex)
TEX := $(filter-out tweetverif.tex,$(wildcard *.tex))
FILES := $(TEX) $(wildcard tikz/*.tex) $(wildcard *.sty)
tweetverif.pdf: FORCE tweetverif.tex
python3 latexrun.py tweetverif.tex
tweetverif.tex: FORCE $(FILES) collection.bib
python3 gen.py tweetverif.tex
tweetverif.pdf: FORCE $(FILES) collection.bib
./latexrun.py tweetverif.tex
depend:
@echo $(FILES)
......
......@@ -12,7 +12,7 @@
\newif\iffull
\fulltrue
\input{macros}
\input{_macros}
\begin{document}
......@@ -57,23 +57,3 @@ The Netherlands}
%}
%\thispagestyle{empty}
\input{abstract.tex}
\input{intro.tex}
\input{preliminaries.tex}
\input{lowlevel.tex}
\input{highlevel.tex}
\input{conclusion.tex}
\vspace*{1cm}
{\footnotesize \bibliographystyle{IEEEtran}
\bibliography{collection}}
\begin{appendix}
\input{code-tweetnacl.tex}
\input{coq.tex}
\input{proofs.tex}
\input{files.tex}
\end{appendix}
\end{document}
......@@ -24,13 +24,12 @@
\hskip1.5em plus0em minus0.5em \fi \nobreak
\vrule height0.75em width0.5em depth0.25em\fi}
\newcommand{\sref}[1]{Section~\ref{#1}}
\newcommand{\tref}[1]{Theorem~\ref{#1}}
\newcommand{\lref}[1]{Lemma~\ref{#1}}
\newcommand{\fref}[1]{Figure~\ref{#1}}
\newcommand{\aref}[1]{Algorithm~\ref{#1}}
\newcommand{\sref}[1]{Section~\ref{#1}}
\newcommand{\tref}[1]{Theorem~\ref{#1}}
\newcommand{\lref}[1]{Lemma~\ref{#1}}
\newcommand{\fref}[1]{Figure~\ref{#1}}
\newcommand{\aref}[1]{Algorithm~\ref{#1}}
\usepackage{soul}\let\strikethrough\st\let\st\undefined
% \DeclareMathOperator*{\argmin}{arg\,min}
% \DeclareMathOperator*{\Vol}{Vol}
......@@ -165,11 +164,6 @@
% \def\gets{{\leftarrow}}
% \newcommand{\Uniform}{\mathcal{U}}
% \newcommand{\UniRk}[1]{\Rqk{#1}}
% \newcommand{\UniRq}{\Rq}
\newcommand{\zeropo}{{\bf 0}}
\newcommand{\Apo}{{\bf A\xspace}}
\newcommand{\Bpo}{{\bf B\xspace}}
......@@ -205,14 +199,6 @@
\newcommand{\Spo}{{\bf S}}
\newcommand{\Ypo}{{\bf Y}}
% \newcommand{\algo}[1]{\textsf{#1}}
% \newcommand{\PeikertDBL}{\algo{dbl}}
% \newcommand{\PeikertREC}{\algo{rec}}
% \newcommand{\PowMul}{{\text{\sf PowMul}}}
% \newcommand{\PowMulPsi}{{\text{\sf PowMul}_{\psi}}}
\newcommand{\ie}{{\textit{i.e.}}\;}
\newcommand{\eg}{{\textit{e.g.}}\;}
\newcommand{\p}{\ensuremath{2^{255}-19}}
......
#!/usr/bin/env python3
import os
import argparse
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 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 os.listdir('.') if not is_ignored(x) and is_tex(x) and not (x == fn)]
appendices = [x for x in files if is_tex(x) and is_appendix(x)]
main = [x for x in files if x not in appendices]
main.sort()
appendices.sort()
output = read('_head.tex')
output += "\n"
for f in main:
output += "\\input{{{}}}\n".format(f)
output += "\n"
output += "\\vspace*{1cm}\n"
output += "{\\footnotesize \\bibliographystyle{IEEEtran}\n"
output += "\\bibliography{collection}}\n"
output += "\n"
output += "\\begin{appendix}\n"
for f in appendices:
output += " \\input{{{}}}\n".format(f)
output += "\\end{appendix}\n"
output += "\n"
output += "\\end{document}\n"
# print(output)
save(fn, output)
main()
......@@ -17,6 +17,7 @@
\usepackage{textcomp}
\usepackage{bussproofs}
\usepackage{xcolor}
\usepackage{soul}\let\strikethrough\st\let\st\undefined
\definecolor{linkcolor}{rgb}{0.65,0,0}
\definecolor{citecolor}{rgb}{0,0.45,0}
......
Supports Markdown
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