Skip to content

Commit

Permalink
make \ecinput macro a bit more robust
Browse files Browse the repository at this point in the history
  • Loading branch information
@strub
strub committed Sep 27, 2024
1 parent b46d5c2 commit b1e5f06
Show file tree
Hide file tree
Showing 63 changed files with 793 additions and 785 deletions.
8 changes: 4 additions & 4 deletions common/easycrypt-common.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,11 +48,11 @@
{\lstset{language=easycrypt,float=tp,caption={#2},label={#3},#1}}%
{}

\newcommand{\ecinput}[5][]%
{\lstinputlisting[language=easycrypt,linerange={#4},caption={#3},label={#5},#1]{#2}}
\newcommand{\ecinput}[2][]%
{\lstinputlisting[language=easycrypt,#1]{#2}}

\newcommand{\ecinputfloat}[4]%
{\lstinputlisting[language=easycrypt,float=tp,linerange={#3},caption={#2},label={#4}]{#1}}
\newcommand{\ecinputfloat}[1]%
{\lstinputlisting[language=easycrypt,float=tp]{#1}}

\def\ls{\lstinline}
\def\ec#1{\lstinline[language=easycrypt-math]"#1"}
Expand Down
39 changes: 12 additions & 27 deletions refman/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,49 +3,34 @@
# --------------------------------------------------------------------
.PHONY: all clean __force__

LATEXMK := latexmk -bibtex -output-directory=_build -silent
EXTRAMK ?=
LATEXMK := latexmk -bibtex -auxdir=_build -silent
LATEXMK += -latex="latex --shell-escape %O %S"
LATEXMK += -pdflatex="pdflatex --shell-escape %O %S"
LATEXMK += -synctex=1
LATEXMK += -synctex=1 -halt-on-error -interaction=nonstopmode
LATEXMK += $(EXTRAMK)
LATEXKO :=
EXTRAMK ?=
ITMODE ?= errorstopmode
LINKS := log synctex.gz
MAIN := refman

ifneq (${DRAFT},)
LATEXMK += -e '$$max_repeat = 1'
LATEXKO += -
endif

LATEXMK += -interaction=$(ITMODE) $(EXTRAMK)

export TEXINPUTS := ../common:.:${TEXINPUTS}

# --------------------------------------------------------------------
.PHONY: all links force scratch clean purge __force__
.PHONY: all force scratch clean

define latex
$(LATEXMK) -pdf $* $(MAIN); err=$$?; \
[ -f _build/$(MAIN).pdf ] && cp _build/$(MAIN).pdf .; \
exit $$err
endef
all:
$(LATEXKO)$(LATEXMK) -pdf $(MAIN)

all: prepare __force__
$(LATEXKO)$(call latex)
force:
$(LATEXKO)$(LATEXMK) -pdf -g $(MAIN)

force: prepare __force__
$(LATEXKO)$(call latex,-g)

prepare: __force__
for i in $(LINKS); do ln -sf _build/$(MAIN).$$i .; done
rm -f _build/$(MAIN).pdf

scratch: purge all
scratch: clean all
@true

clean:
rm -rf _build/ $(LINKS:%=$(MAIN).%)

purge: clean
rm -f $(MAIN).pdf
latexmk -C $(MAIN)
rm -rf _build/
90 changes: 45 additions & 45 deletions refman/ambient-logic.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -281,67 +281,67 @@ \subsection{Introduction and Generalization}
equivalent to \rtactic{idtac}.
In its simplest form, the introduction tactical simply gives names
to assumptions. For example, if the current goal is
\ecinput{examps/parts/tactics/introduction/1-1.0.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/1-1.0.ec}
then running
\ecinput{examps/parts/tactics/introduction/1-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/1-1.ec}
produces
\ecinput{examps/parts/tactics/introduction/1-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/1-1.1.ec}
Alternatively, we can use the introduction pattern \ec{?}
to let \EasyCrypt choose the assumption names, using
\ec{H} as a base for formula assumptions and starting
from the identifier names given in universal quantifiers:
\ecinput{examps/parts/tactics/introduction/2-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/2-1.ec}
produces
\ecinput{examps/parts/tactics/introduction/2-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/2-1.1.ec}

To see how the \ec{->} rewriting pattern works, suppose
the current goal is
\ecinput{examps/parts/tactics/introduction/4-1.0.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/4-1.0.ec}
Then running
\ecinput{examps/parts/tactics/introduction/4-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/4-1.ec}
produces
\ecinput{examps/parts/tactics/introduction/4-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/4-1.1.ec}
Alternatively, one can introduce the assumption \ec{x = y},
and then use the \ec{->>} substitution pattern:
if the current goal is
\ecinput{examps/parts/tactics/introduction/8-1.0.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/8-1.0.ec}
then running
\ecinput{examps/parts/tactics/introduction/8-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/8-1.ec}
produces
\ecinput{examps/parts/tactics/introduction/8-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/8-1.1.ec}

To see how a view may be applied to a not-yet-introduced formula
assumption, suppose the current goal is
\ecinput{examps/parts/tactics/introduction/5-1.0.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/5-1.0.ec}
Then running
\ecinput{examps/parts/tactics/introduction/5-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/5-1.ec}
produces
\ecinput{examps/parts/tactics/introduction/5-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/5-1.1.ec}
And then running
\ecinput{examps/parts/tactics/introduction/5-2.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/5-2.ec}
on this goal produces
\ecinput{examps/parts/tactics/introduction/5-2.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/5-2.1.ec}

Finally, let's see examples of how a disjunction assumption
may be destructed, either using the \ec{case} tactic followed
by a case introduction pattern, or by making the
case introduction pattern do the destruction.
For the first case, if the current goal is
\ecinput{examps/parts/tactics/introduction/6-1.0.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/6-1.0.ec}
then running
\ecinput{examps/parts/tactics/introduction/6-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/6-1.ec}
produces the two goals
\ecinput{examps/parts/tactics/introduction/6-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/6-1.1.ec}
and
\ecinput{examps/parts/tactics/introduction/6-1.2.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/6-1.2.ec}
And for the second case, if the current goal is
\ecinput{examps/parts/tactics/introduction/7-1.0.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/7-1.0.ec}
then running
\ecinput{examps/parts/tactics/introduction/7-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/7-1.ec}
produces the two goals
\ecinput{examps/parts/tactics/introduction/7-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/7-1.1.ec}
and
\ecinput{examps/parts/tactics/introduction/7-1.2.ec}{}{}{}{}
\ecinput{examps/parts/tactics/introduction/7-1.2.ec}
Note how we used the clear pattern to discard the assumption
\ec{X}.
\end{tsyntax}
Expand All @@ -368,10 +368,10 @@ \subsection{Introduction and Generalization}
generalizing the former.

For example, if the current goal is
\ecinput{examps/parts/tactics/generalize/2-1.0.ec}{}{}{}{} then
running \ecinput{examps/parts/tactics/generalize/2-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/generalize/2-1.0.ec} then
running \ecinput{examps/parts/tactics/generalize/2-1.ec}
produces
\ecinput{examps/parts/tactics/generalize/2-1.1.ec}{}{}{}{} In
\ecinput{examps/parts/tactics/generalize/2-1.1.ec} In
this example, one can't generalize \ec{x} without also
generalizing \ec{eq_xy}.

Expand All @@ -381,14 +381,14 @@ \subsection{Introduction and Generalization}
universally quantified identifier of the approprate type.

For example, if the current goal is
\ecinput{examps/parts/tactics/generalize/1-1.0.ec}{}{}{}{} then
running \ecinput{examps/parts/tactics/generalize/1-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/generalize/1-1.0.ec} then
running \ecinput{examps/parts/tactics/generalize/1-1.ec}
produces
\ecinput{examps/parts/tactics/generalize/1-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/generalize/1-1.1.ec}
Alternatively, running
\ecinput{examps/parts/tactics/generalize/3-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/generalize/3-1.ec}
produces
\ecinput{examps/parts/tactics/generalize/3-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/generalize/3-1.1.ec}
\end{itemize}
\end{tsyntax}
\end{tactic}
Expand Down Expand Up @@ -444,10 +444,10 @@ \subsection{Tacticals}
\ec{($\tau_1$; $\;\tau_2$); $\;\tau_3$}.

For example, if the current goal is
\ecinput{examps/parts/tactics/sequence-tactical/1-1.0.ec}{}{}{}{} then
running \ecinput{examps/parts/tactics/sequence-tactical/1-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/sequence-tactical/1-1.0.ec} then
running \ecinput{examps/parts/tactics/sequence-tactical/1-1.ec}
produces the goals
\ecinput{examps/parts/tactics/sequence-tactical/1-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/sequence-tactical/1-1.1.ec}
\end{tsyntax}
\end{tactic}

Expand All @@ -457,8 +457,8 @@ \subsection{Tacticals}
Then apply $\tau'_i$ to $G_i$, for all $i$.

For example, if the current goal is
\ecinput{examps/parts/tactics/sequence-branching-tactical/1-1.0.ec}{}{}{}{} then
running \ecinput{examps/parts/tactics/sequence-branching-tactical/1-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/sequence-branching-tactical/1-1.0.ec} then
running \ecinput{examps/parts/tactics/sequence-branching-tactical/1-1.ec}
solves the goal.
\end{tsyntax}
\end{tactic}
Expand Down Expand Up @@ -489,12 +489,12 @@ \subsection{Tacticals}
\end{tsyntax}

For example, if the current goal is
\ecinput{examps/parts/tactics/do-tactical/1-1.0.ec}{}{}{}{} then
running \ecinput{examps/parts/tactics/do-tactical/1-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/do-tactical/1-1.0.ec} then
running \ecinput{examps/parts/tactics/do-tactical/1-1.ec}
produces the goals
\ecinput{examps/parts/tactics/do-tactical/1-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/do-tactical/1-1.1.ec}
and
\ecinput{examps/parts/tactics/do-tactical/1-1.2.ec}{}{}{}{}
\ecinput{examps/parts/tactics/do-tactical/1-1.2.ec}

\paragraph{Variants.}\strut

Expand Down Expand Up @@ -534,12 +534,12 @@ \subsection{Tacticals}

\bigskip
For example, if the current goal is
\ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.0.ec}{}{}{}{} then
running \ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.0.ec} then
running \ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.ec}
produces the goals
\ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.1.ec}{}{}{}{}
\ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.1.ec}
and
\ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.2.ec}{}{}{}{}
\ecinput{examps/parts/tactics/sequence-reordering-tactical/1-1.2.ec}
\end{tsyntax}
\end{tactic}

Expand Down
55 changes: 38 additions & 17 deletions refman/specifications.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -881,8 +881,7 @@ \subsection{Modules}
which have different name spaces.
Listing~\ref{list:simpmod} contains the definition of a simple module,
\ec{M}, which exemplifies much of the module language.
\ecinput{examps/specifications-examp1.ec}{Simple
Module}{}{list:simpmod}
\ecinput[caption={Simple Module},label=list:simpmod]{examps/specifications-examp1.ec}
\ec{M} has one \emph{global variable}---\ec{x}---which is used by the
\emph{procedures} of \ec{M}---\ec{init}, \ec{incr}, \ec{get} and
\ec{main}. Global variables must be declared before the procedures
Expand Down Expand Up @@ -923,9 +922,13 @@ \subsection{Modules}
\EasyCrypt tries to infer the return types of procedures and the
types of parameters and local variables. E.g., our example module
could be written \ecinput{examps/specifications-examp1a.ec}{Simple
Module with Type Inference}{3-25}{SimpModInfer} As we've seen, each
declaration or statement of a procedure is terminated with a
could be written
%
\ecinput
[linerange=3-25,caption={Simple Module with Type Inference},label={SimpModInfer}]
{examps/specifications-examp1a.ec}
%
As we've seen, each declaration or statement of a procedure is terminated with a
semicolon. One may combine multiple local variable declarations, as
in:
\begin{easycrypt}{}{}
Expand Down Expand Up @@ -961,8 +964,11 @@ \subsection{Modules}
The two remaining kinds of statements are illustrated in
Listing~\ref{list:condwhileexamp}: \emph{conditionals} and \emph{while
loops}.
\ecinput{examps/specifications-examp2.ec}{Conditionals
and While Loops} {}{list:condwhileexamp}
%
\ecinput
[caption={Conditionals and While Loops},label=list:condwhileexamp]
{examps/specifications-examp2.ec}
%
\ec{N} has a single procedure,
\ec{loop}, which begins by initializing a local variable \ec{y} to
\ec{0}. It then enters a while loop, which continues executing until
Expand Down Expand Up @@ -995,9 +1001,12 @@ \subsection{Modules}
As illustrated in Listing~\ref{list:usingothermoduleexamp}, modules may
access the global variables, and call the procedures, of previously
declared modules.
\ecinput{examps/specifications-examp3.ec}{One
Module Using Another Module} {}{list:usingothermoduleexamp} Procedure
\ec{g} of \ec{N} both accesses the global variable \ec{x} of module
%
\ecinput
[caption={One Module Using Another Module},label=list:usingothermoduleexamp]
{examps/specifications-examp3.ec}
%
Procedure \ec{g} of \ec{N} both accesses the global variable \ec{x} of module
\ec{M} (\ec{M.x}), and calls \ec{M}'s procedure, \ec{f} (\ec{M.f}).
The parameter list of \ec{g} could equivalently be written:
\begin{easycrypt}{}{}
Expand Down Expand Up @@ -1050,7 +1059,10 @@ \subsection{Module Types}
\EasyCrypt's \emph{module types} specify the types of a set of
procedures. E.g., consider the module type \ec{OR} :
\ecinput{examps/specifications-examp4.ec}{} {3-7}{} \ec{OR} describes
%
\ecinput[linerange=3-7]{examps/specifications-examp4.ec}
%
\ec{OR} describes
minimum expectations for a ``guessing oracle''---that it provide at
least procedures with the specified types. The order of the
procedures in a module type is irrelevant. In a procedure's type, one
Expand All @@ -1068,8 +1080,13 @@ \subsection{Module Types}
should have. Modules types have a different name space than modules.
Listing~\ref{list:guessormodule} contains an example guessing oracle
implementation. \ecinput{examps/specifications-examp4.ec}{Guessing
Oracle Module} {9-30}{list:guessormodule} Its \ec{init} procedure stores
implementation.
%
\ecinput
[linerange=9-30,caption={Guessing Oracle Module},label=list:guessormodule]
{examps/specifications-examp4.ec}
%
Its \ec{init} procedure stores
the supplied secret in the global variable \ec{sec}, initializes the
allowed number of guesses in the global variable \ec{tris}, and
initializes the \ec{guessed} global variable to record that the secret
Expand All @@ -1083,8 +1100,11 @@ \subsection{Module Types}
module type \ec{OR}, and we can ask \EasyCrypt to check this by
supplying that module type when declaring \ec{Or}, as in
Listing~\ref{list:guessormodulecheck}.
\ecinput{examps/specifications-examp5.ec}{Guessing Oracle Module with
Module Type Check}{9-30}{list:guessormodulecheck}
%
\ecinput
[linerange=9-30,caption={Guessing Oracle Module with Module Type Check},label=list:guessormodulecheck]
{examps/specifications-examp5.ec}
%
Supplying a module type \emph{doesn't} change the result of a module
declaration. E.g., if we had omitted \ec{guessed} from the module type
\ec{OR}, the module \ec{Or} would still have had the procedure
Expand Down Expand Up @@ -1162,8 +1182,9 @@ \subsection{Module Types}
tactics).
The full Guessing Game example is contained in Listing~\ref{list:fullguessing}.
\ecinput{examps/specifications-examp5.ec}{Full
Guessing Game Example} {}{list:fullguessing}
\ecinput
[caption={Full Guessing Game Example},label=list:fullguessing]
{examps/specifications-examp5.ec}
\ec{SimpAdv} is a simple implementation of an adversary.
The inclusion of the constraint \ec{SimpAdv : ADV} in \ec{SimpAdv}'s declaration
\begin{easycrypt}{}{}
Expand Down
6 changes: 4 additions & 2 deletions refman/started.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,8 +79,10 @@ \section{Running \EasyCrypt}
Chapter~\ref{chap:advanced}.

A sample \EasyCrypt script is shown in Listing~\ref{list:startedexamp}.
\ecinput[xleftmargin=.09\textwidth,xrightmargin=.09\textwidth]{examps/started-examp-1.ec}{Sample \EasyCrypt
Script}{}{list:startedexamp}
%
\ecinput
[caption={Sample \EasyCrypt Script},label=list:startedexamp,xleftmargin=.09\textwidth,xrightmargin=.09\textwidth]
{examps/started-examp-1.ec}
%%
As can be inferred from the example, comments begin and end with
\ec{(*} and \ec{*)}, respectively; they may be nested. Each sentence
Expand Down
Loading

0 comments on commit b1e5f06

Please sign in to comment.