Skip to content

Commit

Permalink
[move-prover][tacas] Getting camera ready.
Browse files Browse the repository at this point in the history 
Only addressed spelling errors spotted by reviewers as well as updated the benchmark and linked to Meng's repo with the artifact evaluation which explains the benchmark methodology. There are many interesting questions from the reviewers but we do not have space to address them IMO.

Closes: diem#12
  • Loading branch information
@wrwg @bors-libra
wrwg authored and bors-libra committed Jan 14, 2022
1 parent 98ed299 commit ccc101c
Show file tree
Hide file tree
Showing 8 changed files with 51 additions and 41 deletions.
30 changes: 16 additions & 14 deletions language/move-prover/doc/paper21/analysis.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,11 @@
on one of our more challenging modules, the |DiemAccount| module, which is the
biggest module in the Diem framework. This module implements basic functionality
to create and maintain multiple types of accounts on the blockchain, as well as
manage their coin balances. It was called |LibraAccount| in release 1.0 of
\MVP. The table below lists the number of lines, functions, invariants,
conditions (requires, ensures, and aborts-if), as well as the verification
times:
manage their coin balances. It was called |LibraAccount| in release 1.0 of \MVP,
and is called |DiemAccount| today. The comparison requires various patches as
described in~\cite{MVP_ARTIFACT}. The table below lists the consolidated numbers
of lines, functions, invariants, conditions (requires, ensures, and aborts-if),
as well as the verification times:

{
\setlength{\tabcolsep}{6pt}
Expand All @@ -39,8 +40,8 @@
\hline
Module & Lines & Functions & Invariants & Conditions & Timing \\
\hline
LibraAccount & 1975 & 72 & 10 & 113 & \textbf{9.131s} \\
DiemAccount & 2554 & 64 & 32 & 171 & \textbf{6.290s} \\
LibraAccount & 1975 & 72 & 10 & 113 & \textbf{9.899s} \\
DiemAccount & 2554 & 64 & 32 & 171 & \textbf{7.340s} \\
\hline
\end{tabular*}
\vspace{2ex}
Expand All @@ -51,15 +52,16 @@
added. Moreover, in the original |LibraAccount|, some of the most complex
functions had to be disabled for verification because the old version of \MVP
would time out on them. In contrast, in |DiemAccount| and with the new version,
all functions are verified. Verification time has been improved by roughly 30\%,
in the presence of three times more global invariants, and 50\% more function
conditions.
all functions are verified. Verification time has been improved by roughly 20\%,
\emph{in the presence of three times more global invariants, and 50\% more function
conditions}.

We were able to observe similar improvements for the remaining of the 40 modules
of the Diem framework. All of the roughly half-dozen timeouts in verification in
the framework resolved after introduction of the transformations described in
this paper. Also, specifications which were introduced after the new
transformations did not introduce new timeouts.
of the Diem framework. All of the roughly half-dozen timeouts resolved after
introduction of the transformations described in this paper.

%%Also, specifications which were introduced after the new
%%transformations did not introduce new timeouts.

%% A further improvement is that
%% often, in cases where specification and program disagree, a timeout occurred
Expand Down Expand Up @@ -188,7 +190,7 @@
\Paragraph{Future Work}

\MVP is conceived as a tool for achieving higher assurance systems, not as a bug
hunting tool. Having at least temporarily achieved satsifactory performance and
hunting tool. Having at least temporarily achieved satisfactory performance and
reliability, we are turning our attention to the question of the goal of higher
assurance, which raises several issues. If we're striving for high assurance,
it would be great to be able to measure progress towards that goal. Since
Expand Down
9 changes: 9 additions & 0 deletions language/move-prover/doc/paper21/biblio.bib
View file
Original file line number Diff line number Diff line change
Expand Up @@ -998,3 +998,12 @@ @misc{StateConstraintsPatent
title = {Efficient checking of state-dependent constraints},
year = {U.S. Patent 20050198621A1, 2004}
}

@misc{MVP_ARTIFACT,
author = {{Meng Xu}},
title = {{Artifact for Paper ``Fast and Reliable Formal Verification of Smart Contracts with the Move Prover''}},

url = {https://github.com/meng-xu-cs/mvp-artifact},
bdsk-url-1 = {https://github.com/meng-xu-cs/mvp-artifact},
year = 2020,
}
6 changes: 3 additions & 3 deletions language/move-prover/doc/paper21/design.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -287,7 +287,7 @@
address and the requirement certain state changes are only permitted
for certain accounts by the access control scheme.

Most softare formal verification tools prove that functions preserve
Most software verification tools prove that functions preserve
invariants by assuming the invariant at the entry to each function and
proving them at the exit. In a module or class, it is only necessary
to prove that invariants are preserved by public functions, since
Expand Down Expand Up @@ -412,7 +412,7 @@

Global invariant injection is optimized by knowledge of the prover, obtained by
static analysis, about accessed and modified memory. Let |accessed(f)| be the
memory accessed by a function, and |modified(f)| the memory be modified. Let
memory accessed by a function, and |modified(f)| be the memory modified. Let
|accessed(I)| by an invariant (including transitively by all functions it
calls).

Expand Down Expand Up @@ -463,7 +463,7 @@
however, does not apply for this function, because there is no overlap with
|S<u64>|. In contrast, |g| is generic in type |R|, which could be instantiated
to |u64|. So, |I1|, which applies to |S<u64>| needs to be injected
in addition to |I1|.
in addition to |I2|.
%% relevant for the specific case of |S<u64>|.

The general solution depends on type unification. Given the accessed memory of
Expand Down
2 changes: 1 addition & 1 deletion language/move-prover/doc/paper21/intro.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
well-defined, isolated environment, and 3) their computations are typically
sequential, deterministic, and have minimal interactions with the environment
(e.g., no explicit I/O operations). At the same time, formal verification is
more appealing to the advocates for smart contracts becaues of the large
more appealing to the advocates for smart contracts because of the large
financial and regulatory risks that smart contracts may entail if misbehaved, as
evidenced by large losses that have occurred
already~\cite{CONTRACT_VERIFICATION,hacks-on-smart-contracts,hacks-on-compound}.
Expand Down
34 changes: 17 additions & 17 deletions language/move-prover/doc/paper21/llncs.cls
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
% LLNCS DOCUMENT CLASS -- version 2.20 (10-Mar-2018)
% LLNCS DOCUMENT CLASS -- version 2.21 (12-Jan-2022)
% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
%
%%
Expand All @@ -19,7 +19,7 @@
%% Right brace \} Tilde \~}
%%
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
\ProvidesClass{llncs}[2018/03/10 v2.20
\ProvidesClass{llncs}[2022/01/12 v2.21
^^J LaTeX document class for Lecture Notes in Computer Science]
% Options
\let\if@envcntreset\iffalse
Expand Down Expand Up @@ -122,7 +122,7 @@
\def\ackname{Remerciements.}%
\def\andname{et}%
\def\lastandname{ et}%
\def\appendixname{Appendice}
\def\appendixname{Appendice}%
\def\chaptername{Chapitre}%
\def\claimname{Pr\'etention}%
\def\conjecturename{Hypoth\`ese}%
Expand All @@ -132,13 +132,13 @@
\def\examplename{Exemple}%
\def\exercisename{Exercice}%
\def\figurename{Fig.}%
\def\keywordname{{\bf Mots-cl\'e:}}
\def\indexname{Index}
\def\keywordname{{\bf Mots-cl\'e:}}%
\def\indexname{Index}%
\def\lemmaname{Lemme}%
\def\contriblistname{Liste des contributeurs}
\def\contriblistname{Liste des contributeurs}%
\def\listfigurename{Liste des figures}%
\def\listtablename{Liste des tables}%
\def\mailname{{\it Correspondence to\/}:}
\def\mailname{{\it Correspondence to\/}:}%
\def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
\def\notename{Remarque}%
\def\partname{Partie}%
Expand All @@ -148,9 +148,9 @@
%\def\propositionname{Proposition}%
\def\questionname{Question}%
\def\remarkname{Remarque}%
\def\seename{voir}
\def\seename{voir}%
\def\solutionname{Solution}%
\def\subclassname{{\it Subject Classifications\/}:}
\def\subclassname{{\it Subject Classifications\/}:}%
\def\tablename{Tableau}%
\def\theoremname{Th\'eor\`eme}%
}
Expand All @@ -171,13 +171,13 @@
\def\examplename{Beispiel}%
\def\exercisename{\"Ubung}%
\def\figurename{Abb.}%
\def\keywordname{{\bf Schl\"usselw\"orter:}}
\def\indexname{Index}
\def\keywordname{{\bf Schl\"usselw\"orter:}}%
\def\indexname{Index}%
%\def\lemmaname{Lemma}%
\def\contriblistname{Mitarbeiter}
\def\contriblistname{Mitarbeiter}%
\def\listfigurename{Abbildungsverzeichnis}%
\def\listtablename{Tabellenverzeichnis}%
\def\mailname{{\it Correspondence to\/}:}
\def\mailname{{\it Correspondence to\/}:}%
\def\noteaddname{Nachtrag}%
\def\notename{Anmerkung}%
\def\partname{Teil}%
Expand All @@ -187,9 +187,9 @@
%\def\propositionname{Proposition}%
\def\questionname{Frage}%
\def\remarkname{Anmerkung}%
\def\seename{siehe}
\def\seename{siehe}%
\def\solutionname{L\"osung}%
\def\subclassname{{\it Subject Classifications\/}:}
\def\subclassname{{\it Subject Classifications\/}:}%
\def\tablename{Tabelle}%
%\def\theoremname{Theorem}%
}
Expand Down Expand Up @@ -890,8 +890,8 @@ to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}%
\@ifpackageloaded{hyperref}{%
\def\doi#1{\href{https://doi.org/#1}{https://doi.org/#1}}}{
\def\doi#1{https://doi.org/#1}}
\def\doi#1{\href{https://doi.org/\detokenize{#1}}{\url{https://doi.org/\detokenize{#1}}}}}{
\def\doi#1{https://doi.org/\detokenize{#1}}}
}
\def\homedir{\~{ }}

Expand Down
Binary file modified language/move-prover/doc/paper21/main.pdf
View file
Binary file not shown.
7 changes: 3 additions & 4 deletions language/move-prover/doc/paper21/main.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,11 @@


\author{
David Dill\inst{1} \and Wolfgang Grieskamp\inst{1} \and \\ Junkil
Park\inst{1} \and Shaz Qadeer\inst{1} \and Meng Xu\inst{1}
\and Emma Zhong\inst{1}
David Dill \and Wolfgang Grieskamp \and \\ Junkil
Park \and Shaz Qadeer \and Meng Xu \and Emma Zhong
}

\institute{Novi Research, Facebook}
\institute{Novi Research, Meta Platforms}
\authorrunning{D. Dill, W. Grieskamp et. al.}

\title{Fast and Reliable Formal Verification of Smart Contracts with the Move Prover}
Expand Down
4 changes: 2 additions & 2 deletions language/move-prover/doc/paper21/prelude.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@
\def\UrlBreaks{\do\/\do-}
\usepackage{caption}

\newcommand{\Section}[1]{\vspace{-0ex}\section{#1}}
\newcommand{\SubSection}[1]{\vspace{-0ex}\subsection{#1}}
\newcommand{\Section}[1]{\vspace{-0.5ex}\section{#1}}
\newcommand{\SubSection}[1]{\vspace{-1.0ex}\subsection{#1}}
\newcommand{\Paragraph}[1]{\vspace{-1.0ex}\subsubsection{#1}} % lncs

\newcommand{\TODO}[2]{%
Expand Down

0 comments on commit ccc101c

Please sign in to comment.