\section{\label{case}Guidelines for Formal Methods Adoption}
This section presents guidelines that the cryptocurrency community can consider for the adoption of FM. It starts with a brief and broad presentation of FM.

\subsection{Formal methods in a nutshell}
As we have said, FM is a class of software development techniques based on mathematics and formal logic that can be applied to different  development activities and phases\footnote{FM can be applied to hardware systems, too.}. The main goal of FM is to improve the confidence on the correctness of a program. Program correctness is usually defined as follows: \emph{a program is correct if it verifies its specification}. The word `verifies' can be replaced by `satisfies', `refines', `respects', etc. In any case, the fundamental idea is that you have a program, $P$, and its specification, $S$, and a FM provides you a way to ensure, with different levels of confidence, that $P$ behaves as $S$ states.

In FM the specification or model, $S$ plays a central role:
\begin{itemize}
\item $S$ should be written from the requirements, not from the program; ideally $S$ should be written before $P$ is developed.
\item $S$ is a formal description; that is, in a sense, $S$ is a mathematical model or formula.
\item $S$ represents a family of programs: from $S$ you can get a number of different programs; $S$ does not fix a particular implementation.
\item $S$ should be simpler and shorter than $P$ but, fundamentally, it should be more evidently correct than $P$. That is, when you read $S$ you should feel you are reading something that obviously describes what you want.
\item $S$ should abstract away as many implementation details as possible. Implementing a program entails giving enough details as to a  computer can execute it. A huge number of these details are nonexistent in the requirements. For example, at the requirements level one simply says ``if the customer is a new one, then add it to the data base'', while a C implementation might use a singly-linked list to store customers and so checking if the customer exists and adding it requires pointer arithmetic. In this case, pointer arithmetic is an implementation detail that should not be visible in $S$.
\item $S$ is usually a functional specification but it can also be a security specification (or whatever other non-functional requirement). Then, FM can be used to verify that $P$ correctly does what it is supposed to do and that it does that securely.
\end{itemize}

Then, the application of FM starts by writing a formal specification of your software. It does not mean you must write a complete specification; it can be the specification of a portion of your program (usually the most complex or the most critical). It has been proved countless times that the mere fact of writing $S$ clarifies ideas, pops up unseen problems, etc. Is this a waste of time and resources, or an added cost? No, it is not. These unseen problems will flow into code and sooner or later they will produce unwanted behaviors. Actually, writing $S$ can save you time and money.

Depending on the particular FM you are using, once you have $S$ you can keep applying formal techniques such as:
\begin{enumerate}
\item $S$ can be checked for different levels of soundness.
\item $S$ can be used as a prototype.
\item $S$ can be used to generate test cases.
\item $S$ can be handled to the development team (i.e $P$ is implemented from $S$).
\item $S$ can be used to formally generate a correct-by-construction $P$.
\end{enumerate}

All these activities improve the confidence on the correctness (either functional or security) of your software; only the last one can guarantee correctness but it is the most demanding in terms of time, effort and technical proficiency. Depending on the context, many of these techniques can be automated to some extent, and some times they can be fully automated. The first activity can uncover errors in $S$ thus removing them before they make into $P$. The difference between 4 and 5 is that in 4 developers just read $S$ and write $P$ while in 5 developers \emph{formally prove} that $P$ implements $S$.

There are a number of FM and formal techniques. There are old, enduring, established, assessed, supported FM and there are new, experimental ones. None of them is a silver bullet: if it is very expressive, then it will  be harder to automate, and vice versa; if its models are abstract, then program correctness will be harder to be formally proved; if its models are less abstract, then their complexity can be similar to that of the implementation. In general, each FM was thought and designed to be applied to a class of systems or for a particular verification activity. For example, there are FM to specify and analyze information systems; others more suitable for concurrency; there are very expressive FM aimed at full formal verification; and others aimed at automated verification of limited classes of programs.

In any case, the determining factor of a FM is its specification language. The specification language somewhat fixes what can be expressed, what formal techniques are possible and which can be automated to some valuable extent. The specification language determines the form of your models or specifications. Each specification language is based on some well-known mathematical or logic theory; they always have a formal semantics. There are specification languages based on set theory, type theory, relation algebra, process algebra, transition systems, first-order logic, category theory, higher-order logic, temporal logic, etc. Some specification languages resemble high-level programming languages, most look like math+logic. Nevertheless, specification languages are to high-level programming languages what the latter are to machine code. That is, you can implement a formal specification in any given programming language.

\subsection{Components of cryptocurrency software}
A cryptocurrency software may encompass the following: cryptographic primitives, cryptographic protocols, consensus protocols, a blockchain, a virtual machine, a scripting language, a contract-oriented programming language, a wallet a number of smart contracts. Orthogonal to those the system runs on top of one or more operating systems and the TCP/IP stack, and it has been programmed in one or more programming languages with their corresponding compilers or interpreters. Yet orthogonal to all that you have complex functional and security requirements. And finally, a cryptocurrency software is usually a distributed system.

Any error on any of those components can potentially produce a failure or a vulnerability. That is, an error on any of those components can potentially affect the functional correctness of the system or its security.

Guaranteeing that a cryptocurrency software will never fail and will never be hacked (at least by using any known attack technique) entails proving that all those components are functional and security correct, which in turn requires a formal specification of each component and the interactions between them---which, in particular, includes giving a formal semantics to all the programming languages involved. If you program your blockchain on Rust and the Rust compiler has some error, then your system is potentially vulnerable; if you are using a proven cryptographic primitive whose implementation happens to hide an obscure error, then your system is potentially vulnerable.

Certifying the functional and security correctness of such a system is, currently, a challenging task even for seasoned FM experts. Fortunately, in many cases each component can be independently certified and, furthermore, many verification tasks (cf. items 1-4 above) can be carried on before attempting a formal correctness proof. Indeed, so far, the FM community has formally verified (some times parts of) some of the components of a cryptocurrency software such as, cryptographic primitives \cite{DBLP:journals/iacr/ProtzenkoPFHPBB19}, compilers \cite{DBLP:journals/cacm/Leroy09}, communication protocols \cite{DBLP:conf/nsdi/MusuvathiE04}, cryptographic protocols \cite{DBLP:conf/csfw/BartheHBGH10}, secure operating systems \cite{DBLP:journals/tocs/KleinAEMSKH14}. However, as far as we know, a formal proof of the scale and scope necessary for a full-fledged cryptocurrency software has never been attempted.

\subsection{Cryptocurrency software as critical systems}
If society will eventually depend on a cryptocurrency software its correctness proof should be attempted. Indeed, if a cryptocurrency software ever plays an important role in the society it will be that of a critical system. That is, of a system whose failure would cause irreparable loses---as a failure in the software controlling a nuclear power reactor. If the error or the attack causes the unwanted transfer of cryptomoney, the victims will not be able to recover it due to the virtual nature of cryptocurrencies and because many of these systems enforce strong privacy and anonymity protections.

On the other hand, critical software has been the main target of FM since their inception. For example, the railway industry has been applying FM for its critical systems for quite a long time \cite{DBLP:conf/sbmf/LecomteDPM17}; computer security has been one of the traditional application domains of FM for almost 50 years \cite{Bell:LaPadula,GoguenM82,DBLP:journals/tocs/KleinAEMSKH14,Barthe2017,DBLP:journals/cuza/BetarteCLR16,DBLP:conf/ccs/BartheBCLP14}; several other industrial sectors such as nuclear, defense, health care, etc. apply FM to some of their critical software projects where, in average, 80\% report no increase in development time, +90\% report no added costs, and 88\% report on improved quality \cite{DBLP:books/daglib/p/FitzgeraldBLW13}.

Developers of cryptocurrency software should not be scared about using mathematics as a tool to describe software. In fact, Nakamoto uses math in his seminal paper on Bitcoin \cite{bitcoin} and Wood uses it to describe the EVM \cite{wood2014ethereum}. However, these descriptions would not be understood as FM because they are not based on standardized notations nor on clear mathematical theories. On the other hand, recently, the FM community has started to pay attention to cryptocurrency software. Idelberger et al. \cite{DBLP:conf/ruleml/IdelbergerGRS16} propose to use defeasible logic frameworks such as Formal Contract Logic for the description of smart contracts. Bhargavan et al. \cite{DBLP:conf/ccs/BhargavanDFGGKK16} compile \textsc{Solidity} programs into a verification-oriented functional language where they can verify source code. Luu et al. \cite{DBLP:conf/ccs/LuuCOSH16} use the \textsc{Oyente} tool to find and detected vulnerabilities in smart contracts. Hirai \cite{DBLP:conf/fc/Hirai17} use \textsc{Lem} to formally specify the EVM; Grishchenko, Maffei and Schneidewind \cite{DBLP:conf/post/GrishchenkoMS18} also formalize the EVM but in \textsf{F*}; and Hildenbrandt et al. do the same but with the reachability logic system known as $\mathbb{K}$. P\^irlea and Sergey \cite{Pirlea:2018:MBC:3176245.3167086} present a Coq \cite{coq-manual,coqart} formalization of a blockchain consensus protocol where some properties are formally verified.
Finally, in \cite{DBLP:journals/corr/abs-1907-01688} Betarte et al. present and briefly discuss (formally) properties and outline the basis of a model-driven verification approach to address the certification of the correctness of a particular implementation of the MimbleWimble cryptocurrency protocol.

\subsection{A gradual adoption process}
Hence, the cryptocurrency community should consider the adoption of FM for the developtment of its critical software components. However, the adoption of FM is not only a technical challenge but, more importantly, it requires a sort of cultural shift. In effect, the introduction of FM into the development process requires new personnel or a thorough training of existing staff; the introduction of new tools, techniques and processes; and, in some cases, a redesign of the development cycle---e.g., you cannot change source code without first (re)proving a theorem. Note that the works cited above are carried out by experts on FM. If the cryptocurrency community wants to use FM then it either has to establish strong, mid-term collaboration projects with academic groups or start an adoption program.

Due to the nature and dynamics of the cryptocurency ecosystem we think that developers should slowly introduce FM into the development of cryptocurrency software. FM should become a new asset of the community rather than an outsourced service. The following are some guidelines that can be considered:
\begin{enumerate}
\item Do not attempt a full formal correctness proof from the beginning.
\item Start with abstract specification languages (e.g. set theory) based on first-order logic.
\item Learn to formally specify.
\item Put the verification of code aside for later, focus on writing good models.
\item Abstract away cryptography, assume it is correct, focus on functional specifications.
\item Add \emph{lightweight} or \emph{automated} verification techniques such as simulation \cite{DBLP:journals/scp/HallerstedeLP13}, prototyping \cite{CristiaRossiSETS14}, model-based testing \cite{Utting00}, model-checking \cite{DBLP:books/daglib/0007403} and automated proofs \cite{DBLP:books/daglib/0007471,DBLP:series/faia/2009-185}.
\item Assess what you have learned, correct the course and move on.
\end{enumerate}

In point 5 we suggest that cryptography should be abstracted away in this first adoption stage. This might be generalized to security properties.
The formal verification of security properties is still a challenging issue (see Appendix \ref{security}). Formal verification of some cryptographic primitives has only been achieved very recently \cite{DBLP:journals/iacr/ProtzenkoPFHPBB19}. Furthermore, formally proving non-trivial security properties of code might be an overwhelming task in terms of the effort required, especially compared with proving functional correctness. In addition, many implementation details are orthogonal to the security properties to be established. This implies that slight changes in the implementation technology might have devastating consequences as concerns the security of the implementation.

Therefore, in this paper we show excerpts of a set-based formal model of two components of a cryptocurrency software: a consensus protocol (Sect. \ref{protocol}) and the Ethereum Virtual Machine (EVM, Sec. \ref{evm}), where cryptography and security are abstracted away. Besides, we show how these models can be easily, although partially, analyzed by either lightweight or automated verification techniques (Sect. \ref{verification}).

\section{Final remarks}
\label{sec:conclusion}
Cryptocurrency software should be considered critical: its failures and vulnerabilities would cause irreparable loses. Formal methods have proved to be successful in delivering bug-free software for a range of critical systems. Hence, our first conclusion is that the cryptocurrency community should pay attention to formal methods. However, integrating formal methods into the development process of highly innovative domains cannot be done all at once. Then, our second conclusion is that the cryptocurrency community should \emph{gradually} adopt formal methods.

Specifically, we propose to start the adoption process by using formal specification languages based on set theory and first-order logic. Most developers have been exposed to the mathematics underlying these languages, so adoption could be made minimizing the learning curve. Set-based specifications accurately and concisely describe cryptocurrency software. In order to support this claim we formally specified representative parts of two key components of cryptocurrency software. Once a set-based specification has been written, several verification techniques are enabled. In particular we have shown how prototypes can be easily generated and simulations can be run on them; then, we have applied a model-based testing method to generate test cases from a set-based specification; and finally, we have automatically discharged some proof obligations.

However, these techniques do not allow the formal verification of the implementation. To this end more powerful languages and techniques (e.g. the Coq proof assistant \cite{coq-manual,coqart}) can and should be adopted in future stages. This should be done once the use of formal methods is well understood by the community.

Hopefully, the contents of this paper will convince key players of the cryptocurrency community to assess the application of formal methods more thoroughly.

\section{\label{create} \textit{Create1}}
$Create1$ is defined as follows:
\begin{zed}
Create1 \defs CreateCallsCC \land ContractCreation
\end{zed}
where $ContractCreation$ (not shown) specifies a contract creation operation which entails computing the so-called \emph{mutated state}, executing the initialization code and computing the final state. The specification of these operations needs a few pages of formal code. However we show the definition of $CreateCallsCC$ which

\begin{schema}{CreateCallsCC}
\Xi WorldState; \Delta MachineState; \Xi CallStack \\
s?,o?,a?:ADDR; g?,p?,v?:ETH; i?:PROG; e?:\nat \\
\where
cs \neq \langle \rangle \\
cs~1~pc = create \\
s~1 \leq (acc~(ees~1).Ia).bal \\
(ees~1).Ie < 1024 \\
s? = (ees~1).Ia \\
o? = (ees~1).Io \\
g? = g - g \div 64 \\
p? = (ees~1).Ip \\
v? = s~1 \\
i? = toprog((s(2) \upto s(2) + s(3) - 1) \dres m) \\
e? = (ees~1).Ie + 1 \\
s' = \langle newAddr((ees~1).Ia,(acc~(ees~1).Ia).nonce) \rangle
     \cat tail(tail(tail~s)) \\
i' = M(i,s~2,s~3) \\
out' = \langle \rangle \\
step' = ccbegins \\
m' = m \\
g' = g
\end{schema}

The following function transforms an array of memory cells into a program; it is left underspecified.

\begin{axdef}
toprog: (MADDR \pfun BYTE) \fun PROG
\end{axdef}

\section{\label{evm}Formal Specification of the EVM}
The same notation and methodology can be used to formally specify the EVM. In this case we depart from the Yellow Paper \cite{wood2014ethereum}. The state of the EVM is given by three records:
\[
EVMState \defs [World; Machine; CallStack]
\]
where, for example $World$ and $Machine$ are defined as follows:
\[
World \defs [acc,accCC:Addr \pfun Acc; newaddr:Addr; step:STEP] \\
Machine \defs [
g:ETH;
pc: \nat;
m: A \pfun B;
i:\nat;
s: \seq W;
out: P]
\]
where in turn, for instance, $acc$ represents the Ethereum accounts as a partial function from the set of addresses onto the set of records $Acc \defs [nonce:\nat; bal:ETH; code: PROG]$, which stores the main information of the accounts; $step$ records the current transaction execution step; $m$ represents the state of the memory and $g$ the available gas---where $A$, $B$, $W$, etc. are given sets like $Addr$.

We have two types of transactions:
\[
TT \defs \{contractCreation, messageCall\}
\]
A transaction can be modeled as a record with several fields (some are omited):
\[
Transaction \defs
[Tn,Tg:\nat;
Tp,Tv: ETH;
Ti: P;
Td: \seq B;
snd:Addr]
\]
where, for instance, $Tn$ is the nonce, $Tg$ is the gas limit, $Tp$ is the gas price and $Ti$ is the initialization program for the account.

Now we can model how transactions are executed. According to the YP, a transaction is executed in four steps:
\emph{(a)} the checkpoint state ($\boldsymbol{\sigma}_0$, in YP's notation); \emph{(b)} the post-execution provisional state ($\boldsymbol{\sigma}_P$); \emph{(c)} the pre-final state ($\boldsymbol{\sigma}^*$); and \emph{(d)} the final state ($\boldsymbol{\sigma}'$) is reached after deleting all accounts
that either appear in the self-destruct list or are touched
and empty. The specification of the processing step called checkpoint state ($\boldsymbol{\sigma}_0$) is independent of the transaction type and is defined as follows:
\[
CheckpointState(s:World; t?:Transaction; s':World) \defs \\
\t1 TransactionValidity(s,t?) \\
\t1 \land UpdateSender(s.acc~t?.sender, (acc~t?.sender).bal, t?.Tp, t?.Tg,a')\\
\t1 \land s.step = initial \\
\t1 \land s'.acc = s.acc \oplus \{(t?.sender,a')\} \\
\t1 \land s'.step = ccbegins
\]
where $TransactionValidity$ (not shown) is a complex predicate stating the conditions for a transaction to be valid and $UpdateSender$ is defined as follows:
\[
UpdateSender(s:Acc;b,p:ETH;g:\nat;s':Acc) \defs \\
\t1 s'.bal = b - g*p
\land s'.nonce = s.nonce + 1
\land s'.code = s.code
\]

Hence, $CheckpointState$ checks whether the requested transaction is valid and in that case it (only) updates the sender account by debiting the result of multiplying the gas price and the gas limit as given in the transaction and by adding one to the number of transactions ($s.nonce$).

The transition from $\boldsymbol{\sigma}_0$ to $\boldsymbol{\sigma}_P$ requires the execution of the program associated to the account (or the initialization program if it is a contract creation). Then, at this point we should specify how the EVM executes (bytecode) programs.
To this end, we first need to formalize each and every EVM bytecode instruction. Most instructions can be modeled as a transition between two $MachineState$. We will do that only for a simplified version of the instruction called \verb+create+. According to the YP \verb+create+ ``Creates a new account with associated code''. We have identified two cases so we have:
\begin{zed}
Create \defs Create1 \lor Create2
\end{zed}
where $Create1$ is not shown due to space restrictions. $Create2$ formalizes a situation where the account is actually not created due to some boundary condition:
\[
Create2(q:Machine; w:World; a?:Addr; n?:\nat; q':Machine) \defs \\
\t1 q.s~1 > (w.acc~a?).bal \lor n? \geq 1024 \\
\t1 \land q'.s = \langle 0 \rangle \cat tail(tail(tail~q.s)) \\
\t1 \land q'.i = M(q.i,q.s~2,q.s~3) \\
\t1 \land q'.m = q.m \land q'.g = q.g
\]
where $M$ updates the amount of used memory ($q.i$) by using the second and third positions of the machine stack ($q.s$). Note that $Create2$ modifies the machine state but it needs to access the world state. It also receives the address of the account which owns the code
that is executing ($a?$) and the number of $Creates$ being executed at present ($n?$). The account is not created because either the balance of the caller is too low to fulfill the value transfer or there are too many active $Create$ calls ($n? \geq 1024$). In this case the first three positions in the stack are removed and a 0 is stacked on top of that.

\paragraph{Lesson learned.} The YP describes the semantics of the EVM mixing informal text with  formulas written in some ad-hoc mathematical notation. In the process of writing this specification we found many obscure (probably inconsistent) issues in the math used in the YP. Established formal specification languages have gone a long process of standardization and analysis; their fundamentals have been studied for decades (maybe centuries) by some of the founding fathers of modern mathematics and Computer Science. Even the math used in the YP cannot be compared to well established FM. Besides, most FM are supported by tools implementing a variety of verification techniques. Using math in the YP is a good step forward but the invested effort would be at least partially wasted.

\section{Introduction}
\label{sec:intro}

Given that cryptocurrency software deals with virtual money, software errors can produce irreparable loses. Furthermore, they are a valuable target of highly skilled attackers. Therefore, if a cryptocurrency software has an exploitable vulnerability chances are that attackers will eventually use it to steal money. In fact, some attacks have already been mounted against cryptocurrency software causing irreparable loses of money and credibility (e.g. \cite{dao}).

Note that cryptocurrency software face a more complex problem than traditional banking systems. If your homebanking account is hacked your money can be (potentially) wired transferred to one or more \emph{bank accounts} anywhere on Earth. But these accounts have registered owners who can be duly prosecuted, although some times you will not get your money back. If the same happens in the cryptocurrency world you will not have a registered owner and so prosecution will be harder, if possible.

Hence, software errors in the cryptocurrency world are potentially more costly than the same class of errors in traditional banking systems. Therefore, the quality of cryptocurrency software should be, at least, one ``level'' higher than that of banking software. Although banking software is not (always) ``loose web code'', it certainly is not ``code for a nuclear power reactor''.

For these reasons the cryptocurrency community is seeking for approaches, methods, techniques and development practices that can reduce the chances of the presence of either errors or vulnerabilities\footnote{Actually, the presence of certain errors lead to the existence of vulnerabilities.}. The traditional banking system has less incentives to pursue high levels of software quality and thus to seek better development practices.

One such approach is the application of Formal Methods (FM) to software construction. FM are development methods based on mathematics and logic. They have been around in academia for at least 50 years. There have been undergraduate courses around the globe teaching FM for decades. A number of scientific journals and international conferences are devoted to the study, progess and application of FM. FM is the working field of hundreds of researchers across the planet. The FM community has produced breakthrough results on fundamental aspects of Computer Science and some of its most prominent actors have earned international prizes such as the Turing Award. Leading companies such as Microsoft and Amazon hire  software engineers or researchers on FM to produce or apply FM.

When FM are fully applied they produce ``code for a nuclear power reactor''. That is, due application of FM can produce bug-free, zero-defect, correct-by-construction, guaranteed, certified software. There are a number of critical or mission critical software systems that were developed with FM.

However, the software industry seldom use FM. There are several reasons for which industry is reluctant to use FM among which we can cite: a pervasive underrating of software quality (usually in favor of innovation or as the consequence of free distribution\footnote{That is: Why should I produce bug-free software if I am not sure anyone will use it? Why are you asking me for a warranty if I am giving you this program for free?}); either the perception or the fact that FM severely increase costs and extend schedules; at times the sheer fact that managers do not have a clue about the existence of FM; and the difficulties of finding the right technical staff.

In this paper we present the case for the application of FM to cryptocurrency software. In Sect. \ref{case} we present some guidelines for the adoption of FM in cryptocurrency software projects. We argue that set-based formal modeling (or specification), simulation, prototyping and automated proof can be applied before considering more powerful approaches such as code formal verification. Hence, in Sect. \ref{protocol} we show excerpts of a set-based formal specification of a consensus protocol and in Sect. \ref{evm} of the Ethereum Virtual Machine (EVM). In Sect. \ref{verification} we show that prototypes can be generated from these formal models and simulations can be run on them. Then, we show that test cases can be generated from the same models and how automated proof can be used to evaluate the correctness of these models.

\section{\label{protocol}Formal Specification of a Consensus Protocol}
There are several FM based on set theory and first-order logic (e.g. Z \cite{Spivey00}, VDM \cite{Jones:1990:SSD:94062}, B \cite{Abrial00}). These notations are designed to write large, complex specifications; and there is a number of tools to work with them such as editors, typecheckers, theorem provers, animators, etc. However, in this paper we will use the plain and simple language of mathematics extended with a couple of conventions, to avoid explaining the peculiarities of a particular notation. This will be enough as to show the `look-and-feel' of such specifications.

The following are some snippets of a model of a consensus protocol based on the work by P\^irlea and Sergey \cite{Pirlea:2018:MBC:3176245.3167086}.

A consensus protocol deals with addresses, hashes, proof objects, etc. In an abstract model of the protocol the internal structure of these entities is irrelevant. In particular, hashes and proof objects are strongly related to cryptography which is a feature we think should be abstracted away at this point. Then, we have the set of all possible addresses ($Addr$) that can be used. If $a \in Addr$ then $a$ is an address of the protocol. We do not know what $a$'s structure is, how it was generated, whether it is 128 bits or 256 bits long, etc. The idea is that we do not need to know those things now, because they are implementation details which will not alter the fundamental behavior of the protocol. In this sense we also have the set of hashes ($Hash$), the set of proofs objects ($Proof$) and the set of transactions ($Tx$). The only condition required for these sets is that they come equipped with equality and be pairwise disjoint.
\[
[[Addr,Hash,Proof,Tx]]
\]
The block data structure (cf. blockchain) is a record with three fields: $prev$, (usually) points to the parent block; $txs$, stores the sequence of transactions stored in the block; and $pf$ is a proof object required to validate the block. Then we define $Block$ as the set of all such records:
\[
Block \defs [prev:Hash; txs: \seq Tx; pf:Proof]
\]
The local state space of a participating network node is given by three state variables: $as$, are the addresses of the peers this node is aware of; $bf$, is a block forest (not shown) which records the minted and received blocks; and $tp$, is a set of received transactions which eventually will be included in minted blocks.
\[
LocState \defs [as:\power Addr; bf: Hash \pfun Block; tp: \power Tx]
\]
The protocol configuration is represented by two state variables: $Delta$, which establishes a mapping between network addresses and the corresponding node (local) states (in \cite{Pirlea:2018:MBC:3176245.3167086} this variable is referred to as the \emph{global state}); and $P$, a set of packets (which represent the messages exchanged by nodes).
\[
Conf \defs [Delta:Addr \pfun LocState; P:\power Packet]
\]
Packets are just tuples of two addresses (origin and destination) and a message.
\begin{zed}
Packet == Addr \cross Addr \cross Msg
\end{zed}
The model has twelve state transitions divided into two groups: \emph{local} and \emph{global}. Local transitions are those executed by network nodes, while global transitions promote local transitions to the network level. In turn, the local transitions are grouped into \emph{receiving} and \emph{internal} transitions. Receiving transitions model the nodes receiving messages from other nodes and, possibly, sending out new messages; internal transitions model the execution of instructions run by each node when some local condition is met. Here, we show only the local, receiving transition named $RcvAddr$.
\[
RcvAddr(s:LocState; p?:Packet; ps!:\power Packet; s':LocState) \defs \\
\t1 p?.2 = this \\
\t1 \land \exists asm:\power Addr @ \\
   \t2 p?.3 = AddrMsg~asm \\
   \t2 \land s'.as = s.as \cup asm \\
   \t2 \land s'.bf = s.bf \land s'.tp = s.tp \\
   \t2 \land ps! = \{a:asm \setminus as @ (p?.2,a,ConnectMsg)\} \\
   \t4{}\cup \{a:as @ (p?.2,a,AddrMsg~p'.as)\}
\]
As can be seen, $RcvAddr$ transitions from the local state $s$ into a new local state $s'$, receives a packet ($p?$), and sends out a set of packets ($ps!$). The node checks whether or not the packet's destination address coincides with its own address. In that case, the node adds the received addresses to its local state and sends out a set of packets that are either of the form $(p?.2,a,ConnectMsg)$ or $(p?.2,a,AddrMsg~p'.as)$. The former are packets generated from the received addresses and sent to the new peers the node now knows, while the latter are messages telling its already known peers that it has learned of new peers.

Observe that the expression after the $\defs$ symbol in $RcvAddr$ is a predicate. That is, for example, the equal symbol in $s'.as = s.as \cup asm$ represents logical equality and not (imperative) assignment; $\land$ means logical conjunction and thus $p \land q$ is equal to $q \land p$; $\cup$ is set union; and so forth.

Hopefully, this simple example lets the reader see that abstract specifications tend to be much simpler, concise and evidently correct than code. Furthermore, much of what is said in an abstract specification is what seasoned programmers think while designing good code. Then, formal specification languages give programmers an efficient technique by means of which they can write down their best ideas and be able to communicate them easily and unambiguously. In most cases using formal specifications in this way provides costs savings rather than the opposite.

\section{\label{security}Subtleties and Traps with Security Properties}
Security properties have proved to be unexpectedly complex to grasp and formalize. One of the fundamental reasons for this is that security properties are not safety properties (w.r.t. the Alper-Schneider framework \cite{DBLP:journals/ipl/AlpernS85}). Most of the verification methods, results and tools developed for almost half a century by the Software Engineering community have been aimed at safety properties. Then, most of them fall short when dealing with security properties. Only very recently some of these methods and tools have been adapted for the problem of security properties.

For instance, safety properties enjoy, what is some times called, the \emph{refinement property}. This means that, if $S$ is the description of a system verifying safety property $F$ and $S'$ is a more deterministic refinement of $S$, then $S'$ (automatically) verifies $F$. However, in general, security properties do not enjoy the refinement property. This means that even if you have proved that $S$ verifies security property $F$ and that $S'$ is a refinement of $S$, then you cannot assert that $S'$ verifies $F$. The problem is that there are implementation decisions that in spite of generating a more deterministic system, they might introduce security issues. A typical example is the specification of the values stored in the memory cells delivered by the operating system to a process. At a certain level of abstraction these values might be underspecified which implies that, potentially, any value can be stored. Assume you can prove that this is secure. Afterwards, programmers decide to deliver the cells with the values left by the last process that used that buffer. Although this is an implementation of the first specification it is blatantly insecure.

On the other hand, reasoning about implementations provides the ultimate guarantee that
deployed mechanisms behave as expected. However, due to the issues mentioned above, formally proving non-trivial security properties of code might be an overwhelming task in terms
of the effort required, especially compared w.r.t. proving functional correctness (i.e. a safety property). In addition,
many implementation details are orthogonal to the security properties
to be established. This implies that slight changes in the implementation technology might have devastating consequences as concerns the security of the implementation. Therefore, complementary approaches are needed when non-trivial security properties are at stake:
\begin{enumerate}
\item Verification is performed on idealized models that abstract away the specifics of any particular implementation, and yet provide a realistic setting in which to explore the security issues that pertain to the realm of those (critical) mechanisms.
\item Additionally, verification is performed on more concrete models where low level mechanisms (such as pointer arithmetic) are specified.
\item Finally, the low level model is proved to be a correct implementation of the idealized model.
\end{enumerate}

A particular class of the idealized models mentioned above are those called \emph{security models}. These models have played an important role in the design and evaluation of high assurance security systems. Their importance was already pointed out in the Anderson report~\cite{1296905}. The
paradigmatic Bell-LaPadula model~\cite{Bell:LaPadula}, conceived in 1973, constituted the first big effort on providing a formal setting in which to study and reason on confidentiality properties of data in time-sharing mainframe systems.

\section{\label{verification}Some Verification Techniques for Set-Based Models}
In this section we show the application of three verification techniques that can be used when set-based formal specifications are available. In the first one we show how a set-based specification can be turned into a set-based prototype, that is an inefficient program that nonetheless is correct-by-construction and so it can be used to analyze complex situations (Sect. \ref{prototypes}). Next, we show how the same set-based model can be used to generate test cases that can be used to test the implementation (Sect. \ref{mbt}). Finally, we automatically prove that the same models enjoy some properties (Sect. \ref{proofs}).

\subsection{\label{prototypes}Set-based prototypes and simulations}

Set-based specifications such as those presented in sections \ref{protocol} and \ref{evm}, can be easily turned into set-based prototype programs. In effect, a set-based model can be encoded in the programming language provided by the $\{log\}$\xspace (`setlog') tool \cite{Cristia2019,setlog}. $\{log\}$\xspace is a programming language, a satisfiability solver and an automated theorem prover where sets are first-class entities. $\{log\}$\xspace provides the usual Boolean connectives and most of the set and relational operators available in set theory including binary relations. Hence, it is quite natural to encode a set-based specification as a $\{log\}$\xspace program. Given that $\{log\}$\xspace is based on Prolog its programs resemble Prolog programs.

The $\{log\}$\xspace encoding of $RcvAddr$ presented in Sect. \ref{protocol} is the following:
\begin{verbatim}
rcvAddr(S,P,Ps,S_) :-
  S = {[as,As] / Rest} &
  P = [_,this, addrMsg(Asm)] &
  un(As,Asm,As_) &
  diff(Asm,As,D) &
  PsD = ris(A in D,[],true,[this,A,connectMsg]) &
  PsAs = ris(A in As,[],true,[this,A,addrMsg(As_)]) &
  un(PsD,PsAs,Ps) &
  S_ = {[as,As_] / Rest}.
\end{verbatim}

\verb+rcvAddr+ is a $\{log\}$\xspace clause respecting the interface of $RcvAddr$. In this case, however, instead of using set membership to somewhat ``type'' the parameters we rest on unification. As in Prolog, $\{log\}$\xspace programs are based on unification with the addition of set unification. Variables must start with an uppercase letter. We take advantage of set theory to encode other data structures such as records. A record is a set of ordered pairs where the first component names the field and the second is the variable holding the values. Hence, a statement such as \verb+S = {[as,As] / Rest}+ (set) unifies the first parameter with a set term singling out the record field needed in this case (\verb+As+) and the rest of the record (\verb+Rest+). The same is done with packet \verb+P+ where \verb+_+ means any value as first component and \verb+addrMsg(Asm)+ gets the set of addresses received in the packet without introducing an existential quantifier. The set comprehensions used in the specification are implemented with $\{log\}$\xspace's so-called Restricted Intentional Sets (RIS) \cite{DBLP:conf/cade/CristiaR17}. A RIS is interpreted as a set comprehension where the control variable ranges over a finite set (\verb+D+ and \verb+As+). Finally, \verb+diff(A,B,C)+ is interpreted as $C = A \setminus B$ and \verb+un(A,B,C)+ as $C = A \cup B$.

A clause such as \verb+rcvAddr+ can be seen both as a $\{log\}$\xspace formula and as a $\{log\}$\xspace program. It is a formula in the sense that \verb+&+ is logical conjunction and so the order of statements in \verb+rcvAddr+ is irrelevant due to commutativity. It is a program simply because we can use the $\{log\}$\xspace interpreter to compute outputs from inputs. However, given that $\{log\}$\xspace programs are meant to be prototypes we talk of \emph{simulations} or \emph{animations} rather than executions.

Then, given that \verb+S+ and \verb+P+ are meant to be inputs while \verb+Ps+ and \verb+S_+ are outputs, we can run a simulation from an initial $LocState$ and input packet $p?$ such as:
\begin{verbatim}
S = {[as,{}] / _}
P = [_,this,addrMsg({a1,a2})]
\end{verbatim}
Now, for instance, we can call \verb+rcvAddr+ twice chaining before and after states as follows:
\begin{verbatim}
S = {[as,{}] / _} &
P = [_,this,addrMsg({a1,a2})] &
rcvAddr(S,P,Ps1,S1) &
rcvAddr(S1,[_,this,addrMsg({a1,a3})],Ps2,S2).
\end{verbatim}
in which case $\{log\}$\xspace returns:
\begin{verbatim}
Ps1 = ris(A in {a1,a2/_N2},[],true,[this,A,connectMsg],true),
S1  = {[as,{a1,a2}]/R},
Ps2 = {[this,a3,connectMsg],[this,a1,addrMsg({a2,a1,a3})],
      [this,a2,addrMsg({a2,a1,a3})] /
      ris(A in _N1,[],true,[this,A,connectMsg],true)},
S2  = {[as,{a2,a1,a3}]/R}
Constraint: subset(_N2,{a1,a2}), subset(_N1,{a1,a3}),
            a1 nin _N1, a2 nin _N1
\end{verbatim}
That is, $\{log\}$\xspace binds values for all the free variables in a way that the formula is satisfied (if it is satisfiable at all). In this way we can trace the execution of the protocol w.r.t. states and outputs by starting from a given state (e.g. \verb+S+) and input values (e.g. \verb+[_,this,addrMsg({a1,a2})]+), and chaining states throughout the execution of the state transitions included in the simulation (e.g. \verb+S1+ and \verb+S2+).

\subsection{\label{mbt}Model-based testing}
Model-based testing (MBT) is a testing methodology where test cases are drawn from models or program specifications \cite{Utting00}. That is, instead of letting testers to think what test cases are necessary to test a program, a MBT method gives a disciplined, systematic and quantifiable algorithm for test case generation. There are a number of MBT methods depending on the FM and the type of systems under consideration \cite{Hierons02-largo}. Most MBT methods are supported by (semi)automatic tools thus turning program testing into a more efficient process.

In particular, the Test Template Framework (TTF) can be applied to set-based specifications \cite{Stocks2}. Then, this means that, by writing a set-based specification you can get, almost for free, a prototype and test cases to test the implementation.

We will apply a reduced version of the TTF to the $CheckpointState$ specification given in Sect. \ref{evm}---see elsewhere in the literature for more examples and applications to critical software \cite{DBLP:conf/sew/CristiaAFPM11,DBLP:journals/stvr/CristiaAFPM14}. Note that in $CheckpointState$ we have the following post-condition:
\begin{equation}\label{eq:oplus}
s'.acc = s.acc \oplus \{(t?.sender,a')\}
\end{equation}
where $\oplus$ is a relational operator stating that if $t?.sender \in \dom s.acc$ then its relational image must be updated with $a'$, otherwise the pair $(t?.sender,a')$ must be added to $s.acc$. Besides, recall that $acc$ is a partial function, i.e. a binary relation where all first components are different from each other. Such data structures and operators are seldom available in high-level programming languages. Hence, an efficient implementation of a predicate like \eqref{eq:oplus} will yield a non-trivial piece of code that deserves to be thoroughly tested, specially when it belongs to a critical system.

The TTF defines so-called \emph{standard partitions} for each set theoretic operator. The standard partition for $R \oplus G$ is the following:
\begin{center}
\begin{tabular}{ll}
$R = \emptyset, G = \emptyset$ & $R \neq \emptyset, G \neq \emptyset, \dom G \subset \dom R$ \\[1mm]
$R = \emptyset, G \neq \emptyset$ & $R \neq \emptyset, G \neq \emptyset, \dom R \cap \dom G = \emptyset$ \\[1mm]
$R \neq \emptyset, G = \emptyset$ & $R \neq \emptyset, G \neq \emptyset, \dom R \subset \dom G$ \\[1mm]
$R \neq \emptyset, G \neq \emptyset,$ & $R \neq \emptyset, G \neq \emptyset, \dom R \cap \dom G \neq \emptyset,$ \\
$\quad \dom R = \dom G \phantom{a}$ & $\quad \lnot(\dom G \subseteq \dom R), \lnot(\dom R \subseteq \dom G)$
\end{tabular}
\end{center}
This means that an expression of the form $R \oplus G$ should be tested with eight test cases as follows: $R$ and $G$ equal to the empty set; $R$ equal to the empty set and $G$ not equal to the empty set and vice versa; $R$ and $G$ different from the empty set but having the same domain; and so forth. If for a particular expression some combination of $R$ and $G$ is unfeasible, then it is simply discarded.

Thus, when the standard partition for $\oplus$ is applied to \eqref{eq:oplus} in the context of $CheckpointState$ it yields, after some simplifications, only two test conditions:
\[
\dom s.acc = \{t?.sender\} \\
\{t?.sender\} \subset \dom s.acc
\]
That is, it make sense to test the implementation of \eqref{eq:oplus} in $CheckpointState$ when: the address of the transaction sender is the only account in the system and when it is not the only account in the system.
However, there is more to be tested in $CheckpointState$. For example, $TransactionValidity$ is a complex predicate where the TTF can be applied in several ways. Furthermore, the TTF dictates how the test conditions for some lines of code must be combined with the test conditions generated for the other lines of code.

In general, all the steps of the TTF can be (semi)automated by tools such as \textsc{Fastest} \cite{DBLP:journals/stvr/CristiaAFPM14} and other MBT methods for set-based specifications provide good tool support as well \cite{DBLP:journals/sttt/LeuschelB08}.

\subsection{\label{proofs}Automated proofs}
A program is correct if it verifies its specification. But if the specification is wrong, the program will be wrong and this will be undetectable. Therefore, effort must be made to ensure the specification is correct. The confidence on the correctness of the specification can be increased by proving that it enjoys many desired properties. In a full formal context, all these proofs should be mechanized, although a good first approximation are manual proofs and a second best are automated proofs, as in general full automation is impossible.

For set-based specifications $\{log\}$\xspace can be used as an automated theorem prover and as a counterexample generator---that is, if a proof fails we can know why that happened. In this case we see $\{log\}$\xspace code as formulas over the theory of finite sets (cf. Sect. \ref{prototypes}). In order to prove that a $\{log\}$\xspace formula is a theorem we actually need to prove that its negation is unsatisfiable. For example, concerning \verb+rcvAddr+, we might prove that \verb+PsD+ and \verb+PsAs+ are disjoint sets. In this case we can submit the following to $\{log\}$\xspace:
\begin{verbatim}
diff(Asm,As,D) &
PsD = ris(A in D,[],true,[this,A,connectMsg]) &
PsAs = ris(A in As,[],true,[this,A,addrMsg(As_)]) &
ndisj(PsD,PsAs).
\end{verbatim}
where \verb+ndisj(A,B)+ is interpreted as $A \cap B \neq \emptyset$. In this case $\{log\}$\xspace returns \verb+no+ which means that the formula is unsatisfiable and so \verb+PsD+ and \verb+PsAs+ are disjoint.

As another example, we may want to prove that $s.acc$ is still a partial function after executing $CheckpointState$. This is a so-called \emph{state invariant preservation theorem}. These theorems are of the following form:
\begin{equation}\label{eq:invtheo}
Inv \land Op \implies Inv'
\end{equation}
that is, if $Inv$ holds before executing $Op$, then $Inv$ also holds in the after state (i.e., $Inv'$ is true, where $Inv' \defs Inv[\forall v, v'/v]$). If we want to use $\{log\}$\xspace to discharge such a theorem we must check whether the negation of \eqref{eq:invtheo} is unsatisfiable. Then, in this case the formula to be submitted to $\{log\}$\xspace is:
\begin{verbatim}
  World = {[acc,Acc] / Rest} &
  pfun(Acc) &
  checkpointState(World,Trans,World_) &
  World_ = {[acc,Acc_] / Rest} &
  npfun(Acc_).
\end{verbatim}
where \verb+pfun(F)+ is interpreted as $F$ is a partial function and \verb+npfun+ as its negation. In this case $\{log\}$\xspace returns \verb+no+, which means that \verb+checkpointState+ preserves the invariant, as otherwise expected.


\section{Introduction}
The  most fundamental laws  of nature express the conservation of mass, momentum, energy, etc. The corresponding mathematical models, known as systems of conservation laws, were the object of extensive study from the classical period of mathematical physics, when Euler came up with equations for ideal fluid, to modern times (see \cite{J-75,RJ-83,S-99}).  Such systems revealed  a rich geometric structure
 (see for instance \cite{DN-83,T-85,S-94,AF-99}). This paper falls into the long-term trend of geometrization of mathematical physics.

In presence of 2-dimensional translation symmetry, systems of conservation laws reduce to a system of quasilinear partial differential equations (PDEs) in two independent variables
\begin{equation}
u^i_t=\frac{d}{dx}f^i(u)=v^i_j(u)  u^j_x, ~~~
v^i_j=\frac{\partial f^i}{\partial u^j},~~~i=1,...,n,
\label{CL}
\end{equation}
where $t$ is interpreted as the time and $x$ as the space variable. (In what follows, we sum by repeating indices.)

To the system of conservation laws (\ref{CL}), one associates a
 {\it congruence of lines} (see \cite{AF-96}), i.e. an $n$-parameter family of lines
\begin{equation}
Y^i=u^i\ Y^0+f^i(u)Y^{n+1}, ~~~ i=1,..., n
\label{congrn}
\end{equation}
in $(n+1)$-dimensional projective space $\mathbb P^{n+1}$ with homogeneous coordinates
$[Y^0:...:Y^{n+1}]$. This congruence is also viewed as an $n$-dimensional submanifold of Grassmannian $Gr(2,n+2)$.

The geometry behind this correspondence is the following. Any solution $u(x,t)$ to  (\ref{CL}), which is almost inevitably local for non-linear systems, defines a (germ of) surface $S$ in $(n+2)$-dimensional affine space $A^{n+2}$ with coordinates $(q^1,...,q^n,x,t)=(q,x,t)$, parametrized by $x,t$ via integrating the forms $dq^i:=u^i(x,t)dx+f^i(u(x,t))dt$ closed on the solutions. Taking the affine tangent space to this surface at a point $(q(x,t),x,t)\in S$, translating it to the origin, and projectivizing, we get the {\it Gauss map}
$$
G:S\to Gr(2,n+2).
$$
Now solutions to (\ref{CL}) are intrinsically interpreted as surfaces in $A^{n+2}$ whose Gauss map images lie in the Grassmannian submanifold (\ref{congrn}).

The correspondence allows one to translate   the basic concepts of the theory of systems
of conservation laws into geometrical language. In particular (see \cite{AF-96,AF-99}),
\begin{itemize}
\item rarefaction curves parametrize developable surfaces of the congruence;
\item shock curves describe ruled surfaces of the congruence, whose line generators meet a fixed congruence line;
\item reciprocal transformations manifest themselves as projective transformations of the congruence;
\item commuting systems correspond to congruences, whose focal submanifolds are related by a Peterson transformation;
\item linear degeneracy of a system means that the  developable surfaces of the congruence are conical and the codimension of the focal submanifold jumps up by one;
\item rarefaction curves are rectilinear (this property distinguishes systems of Temple class) if and only if the developable surfaces of the congruence are planar;
\item  a system possesses a Riemann invariant when the focal net of the corresponding focal submanifold is conjugate.
\end{itemize}

Phrased in this geometrical language, the classification of 2-component linearly degenerate systems and of systems of Temple class \cite{T-83} becomes an easy exercise in analytic geometry \cite{AF-96}.
The case of 3-component  systems  is
more involved. In presence of Riemann invariants, both linearly degenerate systems and systems of Temple class were described geometrically in \cite{AF-99}. The case of 3-component nondiagonalizable systems (i.e. not possessing a single Riemann invariant) revealed much stronger resistance. Three-component systems of Temple class were studied in  \cite{AF-99}:  the derived so-called structure equations and equations for characteristic speeds allowed to show that systems with the same structure equations are equivalent by reciprocal transformations; integrable and Hamiltonian systems were also identified . Integrability, linear degeneracy, and equivalence to some Hamiltonian system by reciprocal transformations were shown to be equivalent.

The congruence of a linearly degenerate 3-component system of Temple class turns out to be linear: the Pl\"ucker coordinates of congruence lines are related by linear equations. Thus, the classification and geometric description of linearly degenerate 3-component system of Temple class \cite{AF-01} extend to differential-geometric context the algebraic-geometrical classification of linear congruences, obtained by Castelnuovo in 19th century. Although a general classifications of linear congruences in $\mathbb P^5$ is not known, the integrable class of corresponding 4-component systems of conservation laws was described in detail in \cite{AF-05}. These systems are linearly degenerate; their rarefaction curves are rectilinear; their characteristic speeds form a harmonic quadruplet; the corresponding congruence is linear. Integrable systems with 3 or 4 components, corresponding to linear congruences, admit also the third-order nonlocal Hamiltonian formalism \cite{FPV-18}.
It is remarkable that linearly degenerate systems of Temple class exist for any number of component: along those having  linear congruences, there is a parametric family of so-called reducible systems (see \cite{AF-02}) whose congruences are not linear. Such systems are equivalent to completely exceptional equations of Monge-Amp\`ere type \cite{B-92}.

Projective theory of congruences is a rich and fascinating area of classical differential geometry. The above story certifies that its interrelations with mathematical physics are not restricted just to geometrical optics. As a one more example, we mention the interpretation of iterated Laplace transformation of congruences (see \cite{F-50}) as integrable chains for characteristic speeds \cite{AF-99}.

This paper is dedicated to systems (\ref{CL}) admitting at least two additional conservation laws, i.e.
differential one-forms $B(u)dx+A(u)dt$, $N(u)dx+M(u)dt$ closed on each solution of (\ref{CL}). We suppose that
 the $n+4$ one-forms $dx$, $dt$, $u^i(x,t)dx+f^i(u(x,t)dt, \ \ i=1,...,n,$  $B(u)dx+A(u)dt,$ $N(u)dx+M(u)dt$ are linearly independent over $\mathbb R$ (as 1-forms in $(n+2)$-dimensional space with coordinates $u,x,t$).
It is known that generic Hamiltonian systems have exactly two additional conservation laws, and nondiagonalizable systems with 3 or 4 components cannot admit more than two additional conservation laws.

We straightforwardly generalize  the above construction by assigning   to (\ref{CL}) an $n$-dimensional submanifold of Grassmannian $Gr(2,n+4)$:
\begin{equation}
\begin{array}{l}
Y^i=u^i Y^0+f^i(u)Y^{n+3},\ \ \ \ i=1,..., n,\\
\\
Y^{n+1}=B(u) Y^0+A(u)Y^{n+3},\\
\\
Y^{n+2}=N(u) Y^0+M(u)Y^{n+3}.
\end{array}
\label{congrn2}
\end{equation}
Now the lines in $\mathbb P^{n+3}$, corresponding to the points of this submanifold of the Grassmannian $Gr(2,n+4)$, do not sweep out the whole space but form a ruled $(n+1)$-dimensional hypersurface $\Sigma$ in $\mathbb{P}^{n+3}$.
In what follows, we call  $\Sigma$  the {\it ruled hypersurface of conservation law system}. The existence of two additional independent conservation laws is very restrictive and implies non-trivial geometric properties of the hypersurface $\Sigma$. For such systems we show:
\begin{itemize}
\item projective tangent spaces to $\Sigma$ are stable along its line generators;
\item the hypersurface $\Sigma^*$ dual to $\Sigma$ also corresponds do some system of conservation laws, which we call the  {\it dual} system;
\item  Hamiltonian systems of conservation laws are auto-dual;
\item  the ruled hypersurface $\Sigma$ of a Hamiltonian system sits in some quadric, there is a contact structure on  Fano variety
of this quadric, and the generators of $\Sigma$ form a Legendre submanifold;
\item 3-component nondiagonalizable systems of Temple class are dual to systems with constant characteristic speeds.
\end{itemize}
Five conservation laws of 3-component nondiagonalizable systems with constant characteristic speeds can be viewed as the {\it Abelian relations} of 3-webs of curves in the space of field variables $u$, the web being formed by the rarefaction curves. The web rank, i.e. the dimension of the vector space of Abelian relations, is at most 5 for such webs. There is an elegant geometric description of such webs via cubic hypersurfaces in $\mathbb P^4$     (\cite{BB-38,BW-34}). The established duality gives a complete geometric description of 3-component nondiagonalizable systems of Temple class. The construction of 3-component nondiagonalizable systems of Temple class via cubic hypersurfaces in $\mathbb P^4$ was presented in \cite{AF-99}, though it was not proved that this construction embraces all such systems.

We finish the introduction by an example encapsulating practically all the properties mentioned above.
Consider the  Hamiltonian system
$$
\frac{\partial}{\partial t}\left(\begin{array}{l} u_1\\ u_2\\ u_3 \end{array} \right)=\left(\begin{array}{ccc} -1 & 1 & 1\\ 1 & -1 & 1\\ 1 & 1 & -1 \end{array} \right)\frac{d}{dx}\left(\begin{array}{l} \partial_{u_1} H(u)\\  \partial_{u_2} H(u)\\  \partial_{u_3} H(u) \end{array} \right)
$$
with the Hamiltonian density $H(u)=\frac{1}{2}u_1u_2u_3$ and flat coordinates $u_1,u_2,u_3$.

It has 5 conservation laws
$$
\begin{array}{l}
\sigma_1=u_1dx+\frac{1}{2}[u_2u_3-u_1(u_2+u_3)]dt, \\
\\
\sigma_2=u_2dx+\frac{1}{2}[u_3u_1-u_2(u_3+u_1)]dt, \\
\\
\sigma_3=u_3dx+\frac{1}{2}[u_1u_2-u_3(u_1+u_2)]dt, \\
\\
\sigma_4 = b(u)dx+c(u)dt,\\
\\
\sigma_5 = c(u)dx+f(u)dt,\\
\end{array}
$$
where $b=-\frac{1}{2}\left(u_1u_2+u_2u_3+u_3u_1\right)$, $c= u_1u_2u_3$, and $f= b^2-ac$ with $a=u_1+u_2+u_3$.

This system is {\it reducible}, namely, with $\sigma_1+\sigma_2+\sigma_3=a(u)dx+b(u)dt$,  one can introduce a potential $u(x,t)$ (see \cite{MF-96}) by
$$
u_{xxx}=a, \ \ \ u_{xxt}=b, \ \ \ u_{xtt}=c,\ \ \ u_{ttt}=f,
$$
so that the system is equivalent to the associativity equation of 2D topological field theory
$$
u_{ttt}=u^2_{xxt}-u_{xxx}u_{xtt}.
$$

The characteristic speeds of the system are $\lambda_{\alpha}=-u_{\alpha}$, the rarefaction curves corresponding to $\lambda _1=-u_1$ are trajectories of the characteristic vector field $\xi_1=(u_1-u_2)\partial_{u_2}+(u_3-u_1)\partial_{u_3}$. The other two characteristic vector fields are obtained by cyclic permutations of indices. Thus, the system is {\it lineraly degenerate}, i.e. $\xi_{\alpha}(\lambda_{\alpha})=0$. Moreover, in the new field variables $a,b,c$, which are also densities of conservation laws, the rarefaction curves are rectilinear, thus the system is of {\it Temple class} (\cite{AF-96}).

Finally, the reciprocal transformation
$$
dX=\sigma_1-\sigma_3, \ \ \ \ dT=\sigma_2-\sigma_3
$$
brings our system to the one with constant characteristic speeds $\Lambda_1=\infty$, $\Lambda_2=0$, and $\Lambda_3=-1$. Now let us rewrite the system in the new independent variables $X,T$, choose a basis for the conservation laws, and compose two vectors $\vec I_1,\vec I_2$ with 5 components: the first with fluxes (coefficients of $dT$ of corresponding 1-forms) of the elements of the basis and the second with the densities (coefficients of $dX$).  Then the points  $P,Q,R\in \mathbb P^4$, where $P=-\xi_1(\vec I_2)$,
$Q=\xi_2(\vec I_1)$, and $R=\xi_3(\vec I_2)=-\xi_3(\vec I_1)$ parametrize one and the same cubic hypersurface  in $\mathbb P^4$, the three lines spanned by any pair of points  $P,Q,R$ lying on the cubic.

\section{Conservation laws and families of lines in projective space}

Interpretation of  solutions to (\ref{CL})  as surfaces in affine space whose Gauss map images lie in the Grassmannian sub-manifold (\ref{congrn})
 naturally leads to the idea of {\it reciprocal transformation}: instead of $x,t$ as parameters on the surface $S$ (see Introduction) one can choose suitable linear combinations of the affine coordinates $(q_1,...,q_n,x,t)$. Such reparametrizations induce non-local changes of independent variables:
\begin{equation}
\begin{array}{c}
dX=(\alpha _iu^i+\alpha) dx+(\alpha _if^i+\tilde{\alpha}) dt,\\
dT=(\beta _iu^i+\beta) dx+(\beta _if^i+\tilde{\beta} ) dt,
\end{array}
\label{Trec}
\end{equation}
(here $\alpha _i,\alpha,\tilde{\alpha},\beta _i,\beta,\tilde{\beta}$ are arbitrary constants) and the following substitution for the densities $U^i$ and fluxes $F^i$
$$
U^i=\frac{u^iM-f^iN}{BM-AN}, ~~ F^i=\frac{f^iB-u^iA}{BM-AN},
$$
of the transformed system
\begin{equation}
U^i_T=\frac{d}{dX} F^i(U) ,\ \ \,  i=1,...,n,
\label{CLn}
\end{equation}
where $B=\alpha _iu^i+\alpha$, $A=\alpha _if^i+\tilde{\alpha}$, $N=\beta _iu^i+\beta$, amd $M=\beta _if^i+\tilde{\beta}$.

Finally, there is no reason to restrict oneself to affine transformations changing only two of $n+2$ coordinates $(q^1,...,q^n,x,t)$. Thus, the affine transformations of $A^{n+2}$ induce projective transformations of the congruence (\ref{congrn}).

For systems admitting 2 additional conservation laws, we straightforwardly generalize this construction to surfaces  in  the affine space
$A^{n+4}$ with coordinates $(q^1,...,q^n,q^{n+1},q^{n+2},x,t)$, the quantities $q^{n+1},q^{n+2}$ being defined
by $dq^{n+1}=B(u)dx+A(u)dt$ and $dq^{n+2}=N(u)dx+M(u)dt$, and consider all the geometric objects  in $\mathbb P^{n+3}$ up to projective equivalence.

Observe that any $n$-tuple $f^1,...,f^n$ of functions define a system of conservation laws (\ref{CL}), while the existence of two additional independent conservation laws is very restrictive and implies non-trivial geometric properties of the hypersurface $\Sigma$. Following algebraic geometry, we say that $\Sigma$ is {\it nondegenerate} if it does not lie in any hyperplane.

\begin{theorem}\label{tangentstable}
A nondegenerate ruled hypersurface $\Sigma$ of codimension 2 in $\mathbb P^{n+3}$ corresponds via (\ref{congrn2}) to some system of $n$ conservation laws (\ref{CL}), admitting two additional independent conservation laws, if and only if the projective tangent spaces to $\Sigma$ are stable along the line generators (\ref{congrn2}).
\end{theorem}
{\it Proof:} Let $\Sigma$ correspond to a conservation law system.  Line generators of $\Sigma$ are spanned by points $p=[1,u^1:...:u^n:B:N:0]$ and $r=[0:f^1:...:f^n:A:M:1]$. Denoting   the derivations with respect to $u^i$ by subscript $i$, we get the tangent space at $p$ as the span of $p,r,p_i,$ $i=1,...,n$. For the additional conservation laws one has
\begin{equation}\label{AB}
A_i=B_kf^k_i,\ \ \ \ \   M_i=N_kf^k_i,\ \ \ i=1,...,n.
\end{equation}
hence $r_i=f^l_ip_l$. Thus, the projective tangent space at $r$, and therefore at any point of the generator, coincides with the tangent space at $p$.

Conversely, a ruled hypersurface $\Sigma$ of codimension 2 can be locally parametrized by (\ref{congrn2}). Then the stability of tangent spaces implies (\ref{AB}). Therefore $B(u)dx+A(u)dt$ and $N(u)dx+M(u)dt$ are indeed the additional conservation laws of system (\ref{CL}).
\hfill $\Box$\\

A richer geometry corresponds to the {\it strictly hyperbolic} conservation laws systems, for which the matrix $\nabla f=f^i_j=\partial _{u_j}f^i$ has $n$ distinct real eigenvalues $\lambda^{\alpha}$, called {\it characteristic speeds}:
\begin{equation}\label{char}
\nabla f\xi_{\alpha}=\lambda^{\alpha}\xi_{\alpha},
\end{equation}
 (no summation).
The integral curves of the {\it characteristic} vector fields  $\xi_{\alpha}=\xi_{\alpha}^i\partial _i$, called {\it rarefaction curves}, play distinguished role in the theory of hydrodynamic type systems. A generic solution to (\ref{CL}) parametrizes some surface in the space of field variables $u$. When this surface degenerates into a curve then this curve is necessarily tangent to one of $\xi_{\alpha}$.
For the congruence (\ref{congrn}), the rarefaction curves parametrize the {\it developable surfaces} of the congruence: the lines corresponding to points of the rarefaction curve are tangent to the cuspidal edge of the developable surface (see \cite{AF-96}). Applying this correspondence to various projections of the hypersurface  $\Sigma$ onto $n+1$-dimensional projective subspaces, one concludes that rarefaction curves still parametrize developable surfaces, which now lie on  $\Sigma$. Thus, each generator of  $\Sigma$ is tangent to $n$ submanifolds of  $\Sigma$, which we will call {\it focal}. These focal submanifolds are parametrized by $u$ as follows (see again see \cite{AF-96}):
\begin{equation}
\begin{array}{l}
Y^0=-\lambda^{\alpha}Y^{n+3}\\
\\
Y^i=(f^i(u)-\lambda^{\alpha} u^i)Y^{n+3},\ \ \ \ i=1,..., n,\\
\\
Y^{n+1}=(A(u)-\lambda^{\alpha}B(u))Y^{n+3},\\
\\
Y^{n+2}=(M(u)-\lambda^{\alpha}N(u))Y^{n+3}.
\end{array}
\label{focal}
\end{equation}

\section{Dual conservation laws}

Consider the hypersurface dual to $\Sigma$. Recall that the dual hypersurface $\Sigma ^*$ is the set of points $h$ in the dual space $\mathbb (\mathbb P^{n+3})^*$ such that each $h$ is a projective tangent hyperplane to $\Sigma$.
Note that $codim(\Sigma)=2$ and therefore for each $p\in \Sigma$, there is a pencil $L$ of projective  hyperplanes tangent to $\Sigma$ at $p$.
Thus, the dual hypersurface $\Sigma ^*$ is also ruled.
Theorem \ref{tangentstable} implies that  the pencils $L$ are stable along the line generators of $\Sigma$.
Consequently, the family of the line generators $L$ of the dual hypersurface $\Sigma ^*$ can be parametrized by $u$ and therefore the hypersurface $\Sigma ^*$ has the codimension at least 2.
Observe also that n+2 one-forms of the conservation laws are independent if and only if the hypersurface is not contained in a proper projective subspace of $\mathbb{P}^{n+3}$.
\begin{theorem}\label{dual}
Suppose that the ruled hypersurface $\Sigma$, corresponding via (\ref{congrn2}) to some system of $n$ conservation laws (\ref{CL}), admitting two additional independent conservation laws, enjoys the following properties:\\
1) it is not ruled by projective spaces of any dimension $r>1$,\\
2) its projective tangent spaces are not concurrent.\\
Then the dual hypersurface $\Sigma ^*$ is of codimension 2, it is not contained in a proper projective subspace of $\mathbb{P}^{n+3}$, and its projective tangent spaces are stable along the generators of $\Sigma ^*$.
\end{theorem}
{\it Proof:} By the biduality theorem, the dual to $\Sigma ^*$ is $\Sigma $. If $\Sigma ^*$ were of codimension larger than $2$ then $\Sigma $ would allow ruling in projective spaces of dimension at least 2 (see e.g. \cite{GKZ-94}). If  $\Sigma ^*$ were contained in a proper projective subspace of $\mathbb{P}^{n+3}$ then the tangent spaces of
$\Sigma $ were concurrent.
To prove the last claim, we introduce homogeneous coordinates $Z_i,\ i=0,...,n+3$ in the dual space so that the incidence is given by $Z_iY^i=0.$ Direct calculation gives the following ruling of $\Sigma ^*$:
\begin{equation}
\begin{array}{l}

Z_0=(u^iB_i(u)-B(u))Z_{n+1}+(u^iN_i(u)-N(u))Z_{n+2},\\
\\
Z_i=-B_i(u) Z_{n+1}-N_i(u)Z_{n+2},\ \ \ \ i=1,..., n,\\
\\
Z_{n+3}=(f^i(u)B_i(u)-A(u))Z_{n+1}+(f^i(u)N_i(u)-M(u))Z_{n+2}.\\
\end{array}
\label{congrn2D}
\end{equation}
The generators are spanned by
$\tilde{p}=[u^iB_i-B:-B_1:...:-B_n:1:0:f^iB_i-A]$ and $\tilde{r}=[u^iN_i-N:-N_1:...:-N_n:0:1:f^iN_i-N]$.

Observe that $\partial_k(u^iB_i-B)=u^iB_{ik}$ and by (\ref{AB}) holds  $\partial_k(f^iB_i-A)=f^iB_{ik}.$
Similarly, $\partial_k(u^iN_i-N)=u^iN_{ik}$ and  $\partial_k(f^iN_i-N)=f^iN_{ik}.$ Thus, under the  restrictions imposed, the hypersurface $\Sigma ^*$
  also comes from some conservation law system, for which either $B_i$ or $N_i$ play the role of field variables (densities). Hence the projective tangent space to  $\Sigma ^*$ along the line $\tilde{p}\tilde{r}$ is spanned by $\tilde{p},\tilde{r},\tilde{p_i},\ i=1,...,n$ and is stable.
 \hfill $\Box$

\begin{definition}
Two systems of conservation laws, admitting 2 additional conservation laws, are dual to each other if their ruled hypersurfaces are dual.
\end{definition}

\noindent{\bf Remark.}
Exploiting the geometric ideas manifested in Theorems \ref{tangentstable} and \ref{dual}, we easily construct  systems of conservation laws, which admit one additional conservation law,   via envelope of  an $n$-parameter family of hyperplanes in $\mathbb P^{n+2}$
$$
Z_0+u^iZ_i+B(u)Z_{n+1}+N(u)Z_{n+2}=0,\ \ \ i=1,...,n.
$$
The corresponding $n$-parameter family of lines is
$$
\begin{array}{l}
Z_0=(u^iB_i-B)Z_{n+1}+(u^iN_i-N)Z_{n+2},   \\
\\
 Z_i=-B_i Z_{n+1}-N_iZ_{n+2},\ \ \ \ i=1,..., n.\\
\end{array}
$$
The constructed systems are {\it Godunov's systems} for the case of 2 independent variables  \cite{Gi-61}.
\medskip

 For a strictly hyperbolic system of hydrodynamic type, one can introduce {\it characteristic  forms} $\omega^{\alpha}=l_i^{\alpha}du^i$, where $l^{\alpha}(u)=(l^{\alpha}_1(\vec{u}),...,l^{\alpha}_n(\vec{u}))$ are left eigenvectors of the matrix $\nabla f$. Then the system (\ref{CL}) (and, similarly, any strictly hyperbolic system of hydrodynamical type \cite{F-93}) can be expressed as $n$ exterior equations (no summation)
\begin{equation}\label{exterior}
\omega^{\alpha}\wedge (dx+\lambda^{\alpha}dt)=0.
\end{equation}

This form is particularly convenient for studying systems without Riemann invariants. The forms $\omega^{\alpha}$ constitute a basis for each cotangent space of dependent variables. Thus, differentials of functions $A,B,M,N$ of dependent variables can be decomposed as $dA=A_{\alpha}\omega^{\alpha}$ etc.
Then the equations (\ref{AB}) for conservation laws  become (no summation)
\begin{equation}\label{ABf}
A_{\alpha}=\lambda^{\alpha} B_{\alpha},\ \ \ \ \   M_{\alpha}=\lambda^{\alpha} N_{\alpha},\ \ \alpha=1,...,n.
\end{equation}
 If we normalize the characteristic forms and the characteristic vector fields to verify $\omega^{\alpha}(\xi_{\beta})=\delta^{\alpha}_{\beta}$ then $A_{\alpha}=\xi_{\alpha}(A)$.
In particular, we define coefficients $c^{\alpha}_{ij}$ and  $\lambda^{\alpha}_i$ by relations
 \begin{equation}\label{structureeq}
d\omega ^{\alpha}=c^{\alpha}_{ij}\omega ^i\wedge \omega ^j, \ \ \ \ d\lambda^{\alpha}=\lambda^{\alpha}_i\omega^i.
\end{equation}
and call the first ones  {\it structure equations}.

\begin{theorem}\label{structureD}
Characteristic vectors $\xi_{\alpha}$ of strictly hyperbolic system (\ref{CL}) are also characteristic vectors of the dual system. In particular, the structure equations of the dual system are the same.
\end{theorem}
 {\it Proof:} Suppose that $B_i$ are functionally independent densities of the the dual system defined by (\ref{congrn2D}).  Differentiating the first equation of (\ref{AB}) and comparing the mixed derivatives, one gets
 $$
 A_{ij}=B_{kj}f^k_i+B_kf^k_{ij}=A_{ji}=B_{ki}f^k_j+B_kf^k_{ij}.
 $$
Therefore $B_{kj}f^k_i=B_{ki}f^k_j$ and for each characteristic vector  $\xi_{\alpha}$ of (\ref{CL}) holds
$$
\xi^i_{\alpha}B_{ki}f^k_j=B_{kj}f^k_i\xi^i_{\alpha}=B_{kj}\lambda^{\alpha}\xi^k_{\alpha}.
$$
Note that $\xi^i_{\alpha}B_{ki}=\xi_{\alpha}(B_{k})$ are the components of $\xi_{\alpha}$ in coordinates $B_k$.
Then the above equality says that $\xi_{\alpha}(B_{k})$ are coordinates of a (left) eigenvector of $\nabla f$. Repeating the calculation for $N$ and taking into account the strict hyperbolicity of (\ref{CL}) we conclude the proof.  \hfill $\Box$\\
\section{Contact structure on Fano variety of quadric and Hamiltonian systems}

A Hamiltonian system of hydrodynamical type of first order (see \cite{DN-83} for details) can be written in the so-called flat coordinates as
\begin{equation}\label{hamiltonian}
u^i_t=\varepsilon^i\frac{d}{dx}\left(\frac{\partial h(u)}{\partial u^i}\right),\ \ \  i=1,...,n,
\end{equation}
(no summation) where $h(u)$ is  the Hamiltonian density and $\varepsilon^i=\pm 1$. For $n\ge 3$, a generic system (\ref{hamiltonian}) has no Riemann invariants and possesses exactly $n+2$ conservation laws \cite{T-85}:
\begin{equation}
\begin{array}{l}
u^idx+\varepsilon^i h_idt, \ \text{(no summation)}\\
\\
\frac{1}{2}|u|^2dx+(h_iu^i-h)dt,\\
\\
hdx+\frac{1}{2}|\nabla h|^2dt,
\end{array}
\end{equation}
where $h_i=\frac{\partial h}{\partial u^i}$, $\nabla h=(h_1,...,h_i)$, and $|v|=\varepsilon^i(v_i)^2$ is a pseudo-Riemannian metric.

The line generators of the ruled hypersurface $\Sigma$ are spanned by points
$$
p=[1:u^1:...:u^n:|u|^2/2:h:0]\ \mbox{and} \
r=[0:\varepsilon^1 h_1,...,\varepsilon^n h_n:h_iu^i-h:|\nabla h|^2/2:1].
$$
It is straightforward that these lines lie on the smooth quadric  $(X,X)=0$ defined by the following symmetric bilinear form
$$
(X,Y)=\varepsilon^1X_1Y_1+...+\varepsilon^nX_nY_n-X_0Y_{n+1}-X_{n+1}Y_0-X_{n+2}Y_{n+3}-X_{n+3}Y_{n+2}.
$$
The lines $pr$ parameterize an $n$-dimensional submanifold of $(2n+1)$-dimensional Fano variety $F_{1,n+2}$ of lines on this $(n+2)$-dimensional quadric  $Q$. The tangent space to $F_{1,n+2}$ at $l\in F_{1,n+2}$, where $l$ is the projectivization of a plane $\Lambda \subset \mathbb R^{n+4}$, can be represented as
$$
T_lF_{1,n+2}=\{\overline{\varphi}\in \mbox{Hom}(\Lambda, \mathbb R^{n+4}/ \Lambda): \overline{\varphi}(v)\in T_{[v]}Q/ \Lambda) \},
$$
 (see \cite{H-92},  p. 209). For a representative $\varphi\in \mbox{Hom}(\Lambda, \mathbb R^{n+4})$ of $\overline{\varphi}$ and $X,Y\in \Lambda$, the imposed restrictions read as
$$
(X,\varphi(X))=(Y,\varphi(Y))=(X,\varphi(Y))+(Y,\varphi(X))=0.
$$
Thus, the additional constraint
$$
(X,\varphi(Y))=0
$$
defines a distribution $\tau$ of codimension one on $TF_{1,n+2}$. The geometrical meaning of this constraint is transparent: any pair of points $[X],[Y]$ on a line generator of the quadric $Q$ determines a pencil of projective tangent hyperplanes to $Q$ along the generator, and    $\varphi$ sends any point $Z\in \Lambda$ to the codimension 2 plane of intersection of pencil hyperplanes.

For $\varepsilon^i=1,\ \ i=1,...,n$ and up to a linear change of variables $Y_0,Y_{n+1},Y_{n+2},Y_{n+3}$, the quadric $Q$ coincides with the {\it Lie quadric} in Lie sphere geometry, the distribution $\tau$ defining the contact structure on the Fano variety of Lie quadric (see \cite{C-08}). The introduced distribution is a straightforward generalization.
\begin{lemma}
The distribution $\tau$ provides $TF_{1,n+2}$ with a contact structure.
\end{lemma}
Observe that with the points $p,s$
$$
p=[1:u^1:...:u^n:|u|^2/2:h:0]\ \mbox{and} \
s=[0:\varepsilon^1 k_1,...,\varepsilon^n k_n:k_iu^i-h:|\nabla h|^2/2:1],
$$
and $(u,k,h)\in \mathbb R^{2n+1}$, the lines $ps$ parameterize a Zarisski open subset of $F_{1,n+2}$.

\begin{theorem}
A ruled hypersurface corresponds to a Hamiltonian system (\ref{hamiltonian}) if and only if its line generators form a Legendre submanifold of Fano variety $F_{1,n+2}$ of some smooth quadric in $\mathbb P^{n+3}$.
\end{theorem}
{\it Proof:} The claim follows from the calculation: $(s,dp)=k_idu^i-dh$. \hfill $\Box$\\ \smallskip

 For Hamiltonian systems, duality does not produce any new class of systems with 2 additional conservation laws.
\begin{theorem}\label{autodual}
Hamiltonian system of conservation laws (\ref{hamiltonian}) is auto-dual, points of $\Sigma^*$ being the polar hyperplanes of the corresponding points of $\Sigma$ with respect to the quadric fixed by (\ref{hamiltonian}).
\end{theorem}
{\it Proof:} Applying formulae  (\ref{congrn2D}) to $f^i=\varepsilon^i h_i$ (no summation), $A=h_iu^i-h$, $B=\frac{1}{2}|u|^2$, $M=\frac{1}{2}|\nabla h|^2$, $N=h$, and substituting $Z_{n+3}=Y_{n+2}$, $Z_{n+1}=Y_0$, $Z_{n+2}=Y_{n+3}$, $Z_0=Y_{n+1}$, $ Z_i=-\varepsilon^i Y_i$  (no summation), one arrives at (\ref{congrn2}).
\hfill $\Box$\\

\section{Maximal rank 3-webs of curves in space and conservation laws}\label{5}

Consider 3 foliation $\mathfrak{F}_1,\mathfrak{F}_2,\mathfrak{F}_3$ of space by curves. They form a  {\it 3-web} $\mathfrak{W}_3=\{\mathfrak{F}_1,\mathfrak{F}_2,\mathfrak{F}_3 \}$. A function  $I_k$ (defined, generically, only locally) is a {\it first integral} of the $k$th foliation $\mathfrak{F}_k$ of the web, if it is constant on the leaves of $\mathfrak{F}_k$. An Abelian relation of $\mathfrak{W}_3$ is  an identity relating the first integrals of the form
\begin{equation}\label{Abel}
dI_1+dI_2+dI_3\equiv0.
\end{equation}

For a given web, Abelian relations form a vector space, whose dimension ${\rm rk}(\mathfrak{W}_3)$ is called the web rank. It is known (see \cite{BB-38}) that a $3$-web of integral curves of  3 vector fields have the rank at most 5 if the 2-dimensional distributions spanned by vector field pairs are not integrable. There is the following elegant description of such 3-webs of maximal rank (see \cite{BB-38} p.313 or \cite{BW-34}) via  cubic hypersurfaces $M^3$ in projective space $\mathbb P^4.$ A generic 2-dimensional plane $\mathbb P^2\subset \mathbb P^4$ cuts $M^3$ along some cubic curve $C$.
 There is a 3-parameter family $F^3$ of planes for which the curve  $C$ splits into 3 lines $l_1,l_2,l_3$.  Each line $l_{\alpha}$ determines a one parameter family $F^1_{\alpha}\subset F^3$ of planes, all planes  of $F^1_{\alpha}$ containing  the line $l_{\alpha}$.  These 3 families $F^1_{\alpha},\ \ \alpha=1,2,3,$ are the foliations of some 3-web. This 3-web is of maximal rank and each maximal rank 3-web of curves in space is locally diffeomorphic to some web obtained by the above construction. Observe that the projective moduli space of cubic hypersurfaces $M^3\subset \mathbb P^4$ is of dimension 10, thus the 3-webs under study depend on 10 essential parameters.

 Now let us choose some local parameters  $u^1,u^2,u^3$ in the family $F^3$. Then at each point $u=(u^1,u^2,u^3)$ in the parameter space we can (also locally) define 3 vector fields $\xi_{\alpha}$, each tangent to the corresponding family $F^1_{\alpha}$.
  Integrating an Abelian relation (\ref{Abel}), one can choose the integration constants for $I_i$ to hold $I_1+I_2+I_3\equiv0$. We have $\xi_1(I_1)=0$, $\xi_2(I_2)=0$,  and $\xi_3(I_3)=-\xi_3(I_1)-\xi_3(I_2)=0$.
These three relations can be interpreted as equations (\ref{ABf}) for the conservation laws $I_1dt+I_2dx$ of the hydrodynamical type system (\ref{exterior}) with characteristic speeds $\lambda_1=\infty$, $\lambda_2=0$, and $\lambda_3=-1$ (if you feel uncomfortable with infinity, rotate the coordinate axis in $xt$-plane).
The system has 5-dimensional space of conservation laws.
\begin{lemma}\label{PQR}
 The ruled hypersurface of the above system of conservation laws is 4-dimensional.
\end{lemma}
 {\it Proof:} The proof appeals to the description of 3-webs of maximal rank in \cite{BB-38}. Namely, we choose some basis of Abelian relations $(I_1^i,I_2^i,I_3^i)$, $i=1,...,5$. Then  the 3 lines $l_1,l_2,l_3$  generically intersect in 3 points $P,Q,R\in \mathbb P^4$, where $P=\xi_1(\vec I_3)=-\xi_1(\vec I_2)$,
$Q=\xi_2(\vec I_1)=-\xi_2(\vec I_3)$, and $R=\xi_3(\vec I_2)=-\xi_3(\vec I_1)$. Rotating the axis in the $xt$-plane, we obtain a system of conservation laws with densities $I_1^i-I_2^i$. Then $\xi_1(\vec I_1- \vec I_2)=P$, $\xi_2(\vec I_1-\vec I_2)=Q$, $\xi_3(\vec I_1-\vec I_2)=-2R$ are linearly independent. Thus, the densities of some 3 conservation laws of the transformed system are functionally independent. Therefore the ruled hypersurface of the transformed system, as well as of the original one, is 4-dimensional.   \hfill $\Box$\\

The above Lemma implies that the  systems of conservation laws corresponding to maximal rank 3-webs are not degenerate. The characteristic speeds are not invariant under reciprocal transformations, though one can geometrically express  the property of being equivalent to a system with constant characteristic speeds   as follows.
\begin{theorem}
Strictly hyperbolic system of conservation laws is  equivalent by reciprocal transformation to one with constant characteristic speeds if and only if its focal manifolds lie in hyperplanes.
\end{theorem}
 {\it Proof:} The hyperplane equation is the first one in (\ref{focal}). \hfill $\Box$\\

 We can reformulate the result of Blaschke and Walberer \cite{BW-34} as follows:
\begin{theorem}
If the focal manifolds of strictly hyperbolic system of conservation laws with 2 additional conservation laws  lie in hyperplanes then
the system can be obtained from a maximal rank 3-web of curves in space as described above.
\end{theorem}

\section{Systems of Temple class}

Generic solutions to hyperbolic systems of hydrodynamic type develop shock waves (see \cite{L-79}). For a system of conservation laws (\ref{CL}),  the values of field variables $u_0$ before the shock wave, which is a curve in $xt$-plane, and their values $u$ across the shock wave are related by the {\it shock curve} (in $u$-space) with the vertex at $u_0$. To the shock curve with the vertex $u_0$, there corresponds a 2-dimensional ruled surface of the congruence (\ref{congrn}). The generators of this surface are the congruence lines $l(u)$ intersecting the "vertex" line $l(u_0)$ (see \cite{AF-96}.
\medskip

\noindent{\bf Remark.}
Note that conditions on the shock wave, being obtained by integrating the one-forms $u^idx+f^idt$ over an infinitesimal contour along the arc of the shock wave, distinguish the n-dimensional subspace of conservation laws, spanned by those with densities $u^i$. The choice of quantities preserved also in "integral" form, is dictated by the physics of the model in question. For systems with additional conservation laws,  these additional quantities are preserved only for smooth solutions.
\medskip

As shown by Lax \cite{L-57}, a shock curve with the vertex at a generic point $u_0$ splits into $n$ branches, the $\alpha$-th branch being
$C^2-$tangent of some rarefaction curve of the $\alpha$-th family passing through $u_0.$
There are also systems with shock curves coinciding  with their associated
rarefaction curves. For such systems, among smooth solutions with degenerate (i.e. one-dimensional) hodograph, there exit also weak, discontinuous solutions whose hodograph belongs to a smooth curve.    Systems with coinciding shock and rarefaction curves were characterized by Temple \cite{T-83} as follows.
\begin{theorem}\cite{T-83}
Rarefaction curves of the $\alpha$-th family coincide
with the associated  branches of the shock curve if and only if either\\
1) every rarefaction curve of the $\alpha$-th family is a straight line in the $u-$space, or\\
2) the characteristic velocity $\lambda ^{\alpha}$ is constant along rarefaction curves of the $\alpha$-th family:
 $$
 \xi_{\alpha}(\lambda ^{\alpha})=0
 $$
 (no summation).
\end{theorem}
Systems enjoying the second condition, are called {\it linearly degenerate}. Such systems possess properties unusual for nonlinear hyperbolic systems, namely, their smooth solutions do not develop shock waves \cite{R-67}.  Reciprocal transformations do not preserve the characteristic speeds, but respect linear degeneracy  \cite{F-89}.
Geometrically, the condition means that
developable surfaces of the congruence (\ref{congrn}) (see \cite{AF-96}), or of the hypersurface (\ref{congrn2}) respectively, are conical, and therefore the codimension of  focal submanifolds jumps up at least by one.

The first condition of Temple's Theorem also translates in the geometrical language quite naturally: the cuspidal edges of the developable surfaces are planar \cite{AF-96}.
This geometrical condition is respected not by all reciprocal transformations, but by ones corresponding to  linear combinations of "canonical" conservation laws $u^idx+f^idt$ (see also \cite{AF-96}).
In what follows, we call systems of conservation laws with rectilinear rarefaction curves {\it systems of Temple class}.

In this section, we will be concerned with {\it nondiagonalizable} 3-component systems of Temple class not admitting a single Riemann invariant, which amounts to $d\omega ^{\alpha} \wedge \omega ^{\alpha}\ne 0$ (no summation) for $\alpha =1,2,3$. It is well known that nondiagonalizable 3-component systems admit at most 5 conservation laws.
\begin{theorem}\label{5temple}
Nondiagonalizable 3-component systems of Temple class admit 5 conservation laws.
\end{theorem}
This Theorem can be proved on the basis of computations made in \cite{AF-99}: it was shown that the condition of having rectilinear rarefaction curves is very rigid, the imposed restriction almost  fixes (up to some constant) the coefficients $c^{\alpha}_{ij}$ and $\lambda^{\alpha}_i$ of equations (\ref{structureeq}).
In fact, these equations allow to compute the dimension of the space of conservation laws.
We can also get Theorem \ref{5temple} as a corollary of the proposed duality.
\begin{theorem}\label{DT3}
Nondiagonalizable 3-component systems of Temple class are dual to the systems  obtained from maximal rank 3-webs of curves in space.
\end{theorem}
 {\it Proof:} Let $(I_1^i,I_2^i,I_3^i)$, $i=1,...,5$ be a basis of Abelian relations. Then the ruled hypersurface of corresponding system is parametrized by $Y^i=I_1^iY^0+I_2^iY^6$, $i=1,...,5$. Denote $U=(1,I_1^1,...,I_1^5,0)$, $V=(0,I_2^1,...,I_2^5,1).$ With $P,Q,R$ introduced in the proof of Lemma \ref{PQR}, coordinates $Z_i$, $i=0,1,...,6$ in the dual space, and $\vec z=(Z_1,...,Z_5)$, we get the following equations for generators of the ruled hypersurface for the dual system:
$$
\begin{array}{l}
Z_0=-\vec I_1\cdot \vec z,\\
\\
Z_6=-\vec I_2\cdot \vec z,\\
\\
P\cdot \vec z=Q\cdot \vec z=R\cdot \vec z=0.
\end{array}
$$
Projecting this hypersurface to the projective subspace $Z_0=Z_6=0$, we get a line congruence in $\mathbb P^4$ whose   lines are dual to 2-dimensional planes spanned by 3 points $P,Q,R\in \mathbb P^4$. To the rarefaction curves, there correspond the developable surfaces, whose line generators are dual to the planes in one-parameter families denoted by $F^1_{\alpha}$ in section \ref{5}. The planes in the families pass through a pair of points $P,Q,R$, this pair being fixed by the rarefaction curve. This means that the developable surfaces of the congruence are planar and the dual system is of Temple class.
    \hfill $\Box$\\

Invoking the description of Blaschke and Walberer, we obtain (at least locally)  the rectilinear rarefaction curves of the system of Temple class as follows: consider the planes spanned by 3 points $P,Q,R$; take the dual objets, which are lines in $\mathbb P^4$,  and project these lines from a point to a subspace $\mathbb P^3$. The line images are rectilinear rarefaction curves.  This construction of systems of Temple class was proposed in \cite{AF-99}. Theorem \ref{DT3} implies that the construction gives {\it all} nondiagonalizable 3-component  systems of Temple class.

\section{Concluding remarks}

\subsection{Hydrodynamic surfaces} Formulae (\ref{congrn2D}) suggest that we can use the same field variables $u$ to parametrize the ruled hypersurfaces for both the original system and its dual. Due to Theorem \ref{autodual},  duality respects hydrodynamic surfaces of Hamiltonian systems. A general system with 2 additional conservation laws shares the rarefaction curves with its dual (see Theorem \ref{structureD}), thus respecting degenerate hodographs. For a non-Hamiltonian system, its hydrodynamic surfaces are not the ones for the dual system, as  can be shown by calculation for systems of Temple class with the help of equations (\ref{structureeq}).

\subsection{Intersection of classes of described examples}
We have described three sets of 3-component systems with 5 conservation laws: nondiagonalizable Hamiltonian, nondiagonalizable of Temple class, and the systems obtained from maximal rank 3-webs of curves in space. Up to reciprocal transformations, there is only one systems in the intersection of all three sets, namely, the one equivalent to the associativity equation. In fact, the reciprocal transformation orbit of this system is also the intersection of any pair of the described classes. For the 1st and 2nd, it follows from results of \cite{AF-99}: a nondiagonalizable system of Temple class is Hamiltonian if and only if it is linearly degenerate, and, up to reciprocal transformation, there is only one nondiagonalizable Hamiltonian system of Temple class. For the 2nd and 3d, the intesection consists of linearly degenerate systems and we are done by the same reason. Finally, the systems in the intersection of the 3d and the 1st sets are again linearly degenerate and the claim is equivalent to the main Theorem of \cite{F-95}.

\subsection{Reducible systems, linear congruences, nonlocal Hamiltonian}
Linearly degenerate 3-component systems of Temple class can be realized as {\it reducible} systems (see \cite{A-98,AF-02}). The corresponding congruences (\ref{congrn}) turned out to be linear (see \cite{AF-01}). The congruence of the following 4-component system
$$
u^1_t=u^2_x,\ \ \  u^2_t=u^3_x,\ \ \ \ u^3_t=u^4_x,\ \ \ \ u^4_t=\frac{d}{dx}[(u^2)^2-u^1u^3]
$$
is linear, the system is reducible, but it does not admit any additional conservation laws. Moreover, this system possesses nonlocal Hamiltonian structure of third order \cite{FPV-18}. Thus, the known classes of 3-component systems with 2 additional conservation laws are not straightforwardly generalizable.

\subsection{Correlations and dual congruences in $\mathbb P^3$}
Two-component systems of conservation laws have infinitely many additional conservation laws, but duality for such systems can be defined directly from the congruence (\ref{congrn}). Since the object dual to a line in $\mathbb P^3$ is again a line, any congruence has the dual one. If a developable surface of a congruence is conical, the corresponding developable surface of the dual congruence is planar. This kind of duality for 2-component systems, which is different from the one proposed in this paper, was described in \cite{AF-96} via {\it correlations} of $\mathbb P^3$.

\section*{Acknowledgements}
The author thanks E.V. Ferapontov for useful discussions.
This research was supported by FAPESP grant \#2018/20009-6.