https://github.com/EasyCrypt/easycrypt
Revision a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC, committed by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
1 parent 423a921
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
defs.tex
% !TeX root = easycrypt.tex
%% Names
% Tools
\newcommand{\EasyCrypt}{\textsf{EasyCrypt}\xspace}
\newcommand{\CertiCrypt}{\textsf{CertiCrypt}\xspace}
\newcommand{\CertiPriv}{\textsf{CertiPriv}\xspace}
\newcommand{\SsReflect}{\textsf{SsReflect}\xspace}
\newcommand{\Coq}{\textsf{Coq}\xspace}
\newcommand{\WhyThree}{\textsf{Why3}\xspace}
\newcommand{\SMT}{\textsf{SMT}\xspace}
% Languages and Logics
\newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace}
\newcommand{\pRHL}{\textsf{pRHL}\xspace}
% Version numbers
\newcommand{\ECversion}{1.0\xspace}
%% Misc
\newcommand{\DONE}{}% {{\color{red}DONE}}
\newcommand{\Example}{\paragraph*{Example}}
\newcommand{\Syntax}{\paragraph*{Syntax}}
\newcommand{\Description}{\paragraph*{Description}}
\setcounter{secnumdepth}{3}
\renewcommand{\thesubsubsection}{\arabic{chapter}.\arabic{section}.\arabic{subsection}.\arabic{subsubsection}}
\newbox\minicodebox
\newenvironment{minicode}[1]{%
\minipage[t]{#1\linewidth} %
\centering %
\verbatim %
}{%
\endverbatim %
\endminipage%
}
\newcounter{alarmcounter}
\setcounter{alarmcounter}{1}
\newcommand{\alarm}[1]
{\begingroup
\def\thefootnote{{\normalsize\color{red}(\arabic{footnote})}}
\footnote{\textsf{\textbf{{\color{red}\sc \bf ALARM:}
#1}}}\endgroup}
\newcommand{\infr}[2]{
{\renewcommand{\arraystretch}{1.1}
\begin{array}{c}
{#1}\\
\hline
{#2}
\end{array}}}
%% Indexing
\newcommand{\define}[2][]{\emph{#2}\index{easycrypt}{\ifx\else#1\fi}}
%% Cross-referencing
% \providecommand{\eqref}[1]{\textup{(\ref{#1})}}
% \providecommand{\eqdef}{\raisebox{-.2ex}[.2ex]{$\stackrel{\textrm{\tiny def}}{~=~}$}}
%% IDK
\newcommand{\rname}[1]{[\textsc{#1}]}
\newcommand{\result}{\mathsf{res}}
%% Security properties and schemes
\newcommand{\INDCPA}{\textsf{IND-CPA}\xspace}
\newcommand{\INDCCAone}{\textsf{IND-CCA1}\xspace}
\newcommand{\INDCCA}{\textsf{IND-CCA}\xspace}
\newcommand{\EFCMA}{\textsf{EF-CMA}\xspace}
\newcommand{\LCDH}{\ensuremath{\mathsf{LCDH}}\xspace}
\newcommand{\CDH}{\textsf{CDH}\xspace}
\newcommand{\DDH}{\textsf{DDH}\xspace}
\newcommand{\ElGamal}{\textsf{ElGamal}\xspace}
\newcommand{\HElGamal}{\textsf{HElGamal}\xspace}
\newcommand{\RSA}{\textsf{RSA}\xspace}
\newcommand{\OAEP}{\textsf{OAEP}\xspace}
\newcommand{\FDH}{\textsf{FDH}\xspace}
\newcommand{\HMAC}{\textsf{HMAC}\xspace}
\newcommand{\CS}{\textsf{CS}\xspace}
\newcommand{\Skein}{\textsf{Skein}\xspace}
\newcommand{\TCR}{\textsf{TCR}\xspace}
\newcommand{\KG}{\mathcal{KG}}
\newcommand{\Enc}{\mathcal{E}}
\newcommand{\Dec}{\mathcal{D}}
%% Complexity and termination
\newcommand{\lossless}{\mathsf{lossless}}
%% Sets
\newcommand{\zeroone}{[0,1]}
\newcommand{\bit}{\{0,1\}}
\newcommand{\bitstring}[1]{\ensuremath{\bit^{#1}}}
\newcommand{\bool}{\mathbb{B}}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\real}{\mathbb{R}}
\newcommand{\option}[1]{#1_\bot}
%% Mathematics
\newcommand{\conv}[1][]{\mathrel{\leftrightarrow^*_{#1}}}
\renewcommand{\Pr}[2]{\mathrm{Pr}\left[#1 : #2\right]}
\newcommand{\Prm}[3]{\mathrm{Pr}\left[#1,#3 : #2\right]}
\newcommand{\labs}{\left\lvert}
\newcommand{\rabs}{\right\rvert}
\newcommand{\charfun}{\mathds{1}}
%% Distribution monad
\newcommand{\supp}{\mathsf{support}}
\newcommand{\range}[2]{\mathsf{range}~{#1}~{#2}}
%% Semantics
% \newcommand{\sem}[1]{\llbracket #1 \rrbracket}
\newcommand{\subst}[2]{\left[{}^{#2}/{}_{#1}\right]}
\newcommand{\fv}{\mathsf{fv}}
\newcommand{\modifies}{\mathsf{mod}}
\newcommand{\glob}{\mathsf{glob}}
\newcommand{\Env}{\mathcal{E}}
%% Well-formed adversaries
%% Program Judgements
\newcommand{\Hoare}[3]{\left[{#1}:{#2}\Longrightarrow{#3}\right]}
\newcommand{\Equiv}[4]{\left[{#1}\sim{#2}:{#3}\Longrightarrow{#4}\right]}
\newcommand{\bdHoareS}[5]{{\Hoare{#1}{#2}{#3}}\,{#4}\,{#5}}
\newcommand{\HoareLe}[4]{\bdHoareS{#1}{#2}{#3}{\leq}{#4}}
\newcommand{\HoareEq}[4]{\bdHoareS{#1}{#2}{#3}{=}{#4}}
\newcommand{\HoareGe}[4]{\bdHoareS{#1}{#2}{#3}{\geq}{#4}}
% \newcommand{\Equiv}[4]{\models {#1} \sim {#2} : {#3} \Longrightarrow {#4}}
% \newcommand{\AEquiv}[6]{\models {#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}}
% \newcommand{\JAEquiv}[6]{{#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}}
% \newcommand{\EquivMem}[2]{\models {#1} \equiv {#2}}
% \newcommand{\EqObs}[4]{\models {#1} \simeq^{#3}_{#4} {#2}}
% \newcommand{\AEqObs}[5]{\models {#1} \simeq^{#3}_{{#4}} {#2} \preceq {#5}}
% \newcommand{\ACEqObs}[7]
% {\AEqObs{\left[ #1 \right]_{#6}}{\left[ #2 \right]_{#7}}{#3}{#4}{#5}}
% \newcommand{\Triple}[3]{\sem{#2} {#3} \preceq {#1}}
% \newcommand{\DTriple}[3]{\sem{#2} {#3} \succeq {#1}}
% \newcommand{\dequiv}[3]{{#1} \simeq_{#3} {#2}}
% \newcommand{\fequiv}[3]{{#1} =_{#3} {#2}}
% \newcommand{\Pre}{\Psi}
% \newcommand{\Post}{\Phi}
% \newcommand{\Inv}{\Phi}
\newcommand{\side}[1]{\langle #1 \rangle}
\newcommand{\sidel}{\side{1}}
\newcommand{\sider}{\side{2}}
% \newcommand{\eqobsin}{\mathsf{eqobs\_in}}
% \newcommand{\eqobsout}{\mathsf{eqobs\_out}}
\newcommand{\pre}{\Psi}
\newcommand{\post}{\Phi}
\newcommand{\bound}{\delta}
\newcommand{\ECinsupp}[2]{\mathec{Distr.in_supp}\,{#1}\,{#2}}
\newcommand{\insupp}[2]{{#1}\in\mathec{supp}\,{#2}}
%% Variables
% \newcommand{\LH}{\gl{L}_H}
% \newcommand{\LD}{\gl{L}_\Dec}
% \newcommand{\cdef}{\gl{\gamma_\mathsf{def}}}
\newcommand{\var}[1]{\ensuremath{\mathit{#1}} \xspace}
%% Constants and operators
% TODO: Update!
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
\newcommand{\nil}{\mathsf{nil}}
\newcommand{\hd}{\mathsf{hd}}
\newcommand{\tl}{\mathsf{tl}}
\newcommand{\app}{\mathbin{+\mkern-7mu+}}
\newcommand{\concat}{\parallel}
\newcommand{\xor}{\oplus}
\newcommand{\msb}[2]{[#1]^{#2}}
\newcommand{\lsb}[2]{[#1]_{#2}}
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\ran}{\mathsf{ran}}
\newcommand{\fst}{\mathsf{fst}}
\newcommand{\snd}{\mathsf{snd}}
\newcommand{\some}[1]{#1}
\newcommand{\none}{\bot}
\newcommand{\Int}{\mathsf{Int}}
\newcommand{\tint}{\mathsf{int}}
\newcommand{\tbool}{\mathsf{bool}}
%% Language
% TODO: Update!
\newcommand{\Skip}{\mathsf{skip}}
\newcommand{\Seq}[2]{#1;\ #2}
\newcommand{\Ass}[2]{#1 \leftarrow #2}
\newcommand{\Rand}[2]{#1 \stackrel{\raisebox{-.25ex}[.25ex]%
{\tiny $\mathdollar$}}{\raisebox{-.2ex}[.2ex]{$\leftarrow$}} #2}
\newcommand{\Randi}[2]{\Rand{#1}{[0..#2]}}
\newcommand{\Randb}[1]{\Rand{#1}{\bit}}
\newcommand{\Randbs}[2]{\Rand{#1}{\bitstring{#2}}}
\newcommand{\Cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
\newcommand{\Condt}[2]{\mathsf{if}\ #1\ \mathsf{then}\ #2}
\newcommand{\Else}{\mathsf{else}\ }
\newcommand{\Elsif}{\mathsf{elsif}\ }
\newcommand{\nWhile}[3]{\mathsf{while}_{#1}\ #2\ \mathsf{do}\ #3}
\newcommand{\While}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
\newcommand{\Call}[3]{#1 \leftarrow #2\mathsf{(}#3\mathsf{)}}
\newcommand{\Return}{\mathsf{return}}
% \newcommand{\Assert}[1]{\mathsf{assert}~#1}
%% Tactics
\newcommand{\tacname}{Error tacname}
\newcommand{\vtacname}{Error tacname}
\newcommand{\vararg}[1]{\ec{#1}}
\newcommand{\cstarg}[1]{\ec{#1}}
\newcommand{\typarg}[1]{\textit{#1}}
\newcommand{\tacarg}[2]{(\vararg{#1}:\typarg{#2})}
\newcommand{\addTacticIdx}[2]{\index{#1}{#2@\rawec{#2}}}
\newcommand{\addTacticNoIdx}[2]{
\renewcommand{\tacname}{\rawec{#1}}
\renewcommand{\vtacname}{#1}
\subsubsection{#1}
\Syntax \ec{#1} #2
\Description}
\newcommand{\addTacticPlain}[2]{
\renewcommand{\tacname}{\rawec{#1}}
\renewcommand{\vtacname}{#1}
\subsubsection{#1}
\Syntax {#2}
\Description}
\newcommand{\addTactic}[3]{
\addTacticIdx{#1}{#2}
\addTacticNoIdx{#2}{#3}}
%% Language definition
\lstnewenvironment{easycrypt}[2][]%
{\lstset{language=easycrypt,caption={#2},#1}}%
{}
\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline[language=easycrypt,#1]{#2}}
\newcommand{\mathec}[1]{\mbox{\rawec{#1}}}
\newcommand{\ec}[2][basicstyle=\normalsize\sffamily]{\lstinline[language=easycrypt,style=easycrypt-pretty,#1]{#2}}
\newcommand{\ecimport}[4][]{\lstinputlisting[language=easycrypt,linerange=#4,caption=#2,#1]{#3}}
\lstdefinelanguage{easycrypt}{
style=easycrypt-default,
% procnamekeys={op,pred,fun},
% procnamestyle={\sffamily\itshape},
keywordsprefix={'},
morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word},
morekeywords=[2]{type,op,axiom,lemma,module,pred,const,declare},
morekeywords=[3]{var,fun},
morekeywords=[4]{while,if},
morekeywords=[5]{theory,end,clone,import,export,as,with,section},
morekeywords=[6]{forall,exists,lambda},
morekeywords=[7]{idtac,change,beta,iota,zeta,logic,delta,simplify,congr,generalize,
pose,split,left,right,case,intros,cut,elim,apply,rewrite,elimT,subst,
progress,trivial},
morekeywords=[8]{by,assumption,smt,reflexivity},
morekeywords=[9]{first,last,do,try},
% moredirectives={prover,print}, % Incomplete
morecomment=[n][\itshape]{(*}{*)},
morecomment=[n][\bfseries]{(**}{*)}
}
\lstdefinestyle{easycrypt-default}{
columns=fullflexible,
captionpos=b,
frame=tb,
xleftmargin=.1\textwidth,
xrightmargin=.1\textwidth,
rangebeginprefix={(**\ begin\ },
rangeendprefix={(**\ end\ },
rangesuffix={\ *)},
includerangemarker=false,
basicstyle=\small\sffamily,
identifierstyle={},
keywordstyle=[1]{\itshape\color{OliveGreen}},
keywordstyle=[2]{\bfseries\color{Blue}},
keywordstyle=[3]{\bfseries},
keywordstyle=[4]{\bfseries},
keywordstyle=[5]{\bfseries\color{OliveGreen}},
keywordstyle=[6]{\itshape\color{Blue}},
keywordstyle=[7]{\color{Blue}},
keywordstyle=[8]{\color{Red}},
keywordstyle=[9]{\color{OliveGreen}},
literate={phi}{{$\!\phi\,$}}1
{phi1}{{$\!\phi_1$}}1
{phi2}{{$\!\phi_2$}}1
{phi3}{{$\!\phi_3$}}1
{phin}{{$\!\phi_n$}}1
}
\lstdefinestyle{easycrypt-pretty}{
basicstyle=\small\sffamily,
literate={:=}{{$\mathrel{\gets}\;$}}1
{<=}{{$\mathrel{\leq}\;$}}1
{>=}{{$\mathrel{\geq}\;$}}1
{<>}{{$\mathrel{\neq}\;$}}1
{=\$}{{$\stackrel{\$}{\gets}\;$}}1
{forall}{{$\forall\;$}}1
{exists}{{$\exists\;$}}1
{->}{{$\rightarrow\;$}}1
{<-}{{$\leftarrow\;$}}1
{<->}{{$\leftrightarrow\;$}}1
{<=>}{{$\Leftrightarrow\;$}}1
{=>}{{$\Rightarrow\;$}}1
{==>}{{$\Rrightarrow\;$}}1
{\/\\}{{$\wedge\;$}}1
{\\\/}{{$\vee\;$}}1
{.\[}{{[}}1
{''ora}{{$\mathrel{||}$}}1 %needed for correct display in index
{'a}{{\color{OliveGreen}$\alpha\,$}}1
{'b}{{\color{OliveGreen}$\beta\,$}}1
{'c}{{\color{OliveGreen}$\gamma\,$}}1
{'t}{{\color{OliveGreen}$\tau\,$}}1
{'x}{{\color{OliveGreen}$\chi\,$}}1
}
%% Typesetting
\newcommand{\titledbox}[4]{{\color{#1}\fbox{\begin{minipage}{#2}{\textbf{#3:} \color{black}#4}\end{minipage}}}}
\newcommand{\warningbox}[1]{\titledbox{red}{.9\textwidth}{Warning}{#1}}
\newcommand{\futurebox}[1]{\titledbox{blue}{.9\textwidth}{Future}{#1}}
\newcommand{\NotDocumented}{
\begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering
\textbf{Not yet documented}}
\end{minipage}}}\end{center}}
\newcommand{\NotImplemented}{
\begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering
\textbf{Not yet implemented}}
\end{minipage}}}\end{center}}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "easycrypt"
%%% End:
Computing file changes ...