Commit inicial: Introducción

1 files changed, 340 insertions, 0 deletions

diff --git a/defs.tex b/defs.tex
new file mode 100755
index 0000000..7a9c73d
--- /dev/null
+++ b/defs.tex
@@ -0,0 +1,340 @@
+% Source: EasyCrypt manual (https://www.easycrypt.info)
+
+% !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}
+
+% Languages and Logics
+ \newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace}
+ \newcommand{\pRHL}{\textsf{pRHL}\xspace}
+
+% Version numbers
+ \newcommand{\ECversion}{0.$\beta$\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&#1&#2\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,datatype,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
+              {lambda}{{$\lambda\,$}}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: 
\ No newline at end of file