Merge branch 'tech-whitepaper'

This commit is contained in:
Mike Hearn 2016-11-28 14:23:00 +00:00
commit f840f8b58c
10 changed files with 118 additions and 47 deletions

View File

@ -346,3 +346,21 @@ publisher = {USENIX Association},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@misc{TheDAOHack,
author = {David Siegel},
howpublished = {\url{http://www.coindesk.com/understanding-dao-hack-journalists/}},
year = {2016}
}
@misc{BitcoinEnergy,
author = {Christopher Malmo},
howpublished = {\url{http://motherboard.vice.com/read/bitcoin-is-unsustainable}},
year = {2015}
}
@misc{Swanson,
author = {Tim Swanson},
howpublished = {\url{http://tabbforum.com/opinions/settlement-risks-involving-public-blockchains}},
year = {2016}
}

View File

@ -24,11 +24,6 @@
\begin{document}
\maketitle
%\epigraphfontsize{\small\itshape}
%\renewcommand{\abstractname}{An introduction}
%\textit{Confidential: Pre-Publication Final Draft For R3 Distributed Ledger Group Steering Committee}
\begin{abstract}

View File

@ -11,7 +11,8 @@
breaklines,%
autogobble,%
frame=lines,%
framesep=2\fboxsep%
framesep=2\fboxsep,%
fontsize=\footnotesize%
}
\usepackage{color}
\usepackage{epigraph}
@ -183,7 +184,7 @@ Oracles and notaries are covered in later sections.
\subsection{Identity and the permissioning service}
Unlike Bitcoin and Ethereum, Corda is designed for semi-private networks in which admission requires obtaining an
identity signed by a root authority. This assumption is pervasive - the flow API provides messaging in terms of identities,
identity signed by a root authority. This assumption is pervasive -- the flow API provides messaging in terms of identities,
with routing and delivery to underlying nodes being handled automatically. There is no global broadcast at any point.
This `identity' does not have to be a legal or true identity. In the same way that an email address is a globally
@ -216,7 +217,7 @@ provide. On receiving a connection, nodes check that the connecting node is in t
The network map abstracts the underlying IP addresses of the nodes from more useful business concepts like identities
and services. Each participant on the network, called a \emph{party}, publishes one or more IP addresses in the
network map. Equivalent domain names may be helpful for debugging but are not required. User interfaces and APIs
always work in terms of identities - there is thus no equivalent to Bitcoin's notion of an address (hashed public key),
always work in terms of identities -- there is thus no equivalent to Bitcoin's notion of an address (hashed public key),
and user-facing applications rely on auto-completion and search rather than QRcodes to identify a logical recipient.
It is possible to subscribe to network map changes and registering with the map is the first thing a node does at
@ -235,8 +236,10 @@ either reliably stored the message or processed it completely. Connections betwe
needed: there is no assumption of constant connectivity. An ideal network would be entirely flat with high quality
connectivity between all nodes, but Corda recognises that this is not always compatible with common network
setups and thus the message routing component of a node can be separated from the rest and run outside the firewall.
In this way nodes that do not have duplex connectivity can still take part in the network as first class citizens.
Additionally a single node may have multiple advertised IP addresses.
Being outside the firewall or in the firewall's `de-militarised zone' (DMZ) is required to ensure that nodes can
connect to anyone on the network, and be connected to in turn. In this way a node can be split into multiple
sub-services that do not have duplex connectivity yet can still take part in the network as first class citizens.
Additionally, a single node may have multiple advertised IP addresses.
The reference implementation provides this functionality using the Apache Artemis message broker, through which it
obtains journalling, load balancing, flow control, high availability clustering, streaming of messages too large to fit
@ -277,14 +280,14 @@ this can become quite involved. The implementation of Bitcoin payment channels i
As another example, the core Bitcoin protocol only allows you to append transactions to the ledger. Transmitting other
information that might be useful such as a text message, refund address, identity information and so on is not supported
and must be handled in some other way - typically by wrapping the raw ledger transaction bytes in a larger message that
and must be handled in some other way -- typically by wrapping the raw ledger transaction bytes in a larger message that
adds the desired metadata and giving responsibility for broadcasting the embedded transaction to the recipient, as in
Bitcoin's BIP 70\cite{BIP70}.
In Corda transaction data is not globally broadcast. Instead it is transmitted to the relevant parties only when they
need to see it. Moreover even quite simple use cases - like sending cash - may involve a multi-step negotiation between
need to see it. Moreover even quite simple use cases -- like sending cash -- may involve a multi-step negotiation between
counterparties and the involvement of a third party such as a notary. Additional information that isn't put into the
ledger is considered essential, as opposed to nice-to-have. Thus unlike traditional blockchain systems in which the primary
ledger is considered essential, as opposed to nice-to-have. Thus unlike traditional block chain systems in which the primary
form of communication is global broadcast, in Corda \emph{all} communication takes the form of small multi-party sub-protocols
called flows.
@ -331,6 +334,12 @@ a payment is not considered acceptable.
Flows are named using reverse DNS notation and several are defined by the base protocol. Note that the framework is
not required to implement the wire protocols, it is just a development aid.
% TODO: Revisit this diagram once it matches the text more closely.
%\begin{figure}[H]
%\includegraphics[scale=0.16, center]{trading-flow}
%\caption{A diagram showing the two party trading flow with notarisation}
%\end{figure}
\subsection{Data visibility and dependency resolution}
When a transaction is presented to a node as part of a flow it may need to be checked. Simply sending you
@ -352,9 +361,9 @@ involve many round-trips and thus take some time to fully complete. How quickly
is thus difficult to characterise: it depends heavily on usage and distance between nodes. Whilst nodes could
pre-push transactions in anticipation of them being fetched anyway, such optimisations are left for future work.
A more important consequence is that in the absence of additional privacy measures it is difficult to reason
about who may get to see transaction data. We can say it's definitely better than a system that uses global
broadcast, but how much better is hard to characterise. This uncertainty is mitigated by several factors.
Whilst this system is simpler than creating rigid data partitions and clearly provides better privacy than global
broadcast, in the absence of additional privacy measures it is nonetheless still difficult to reason about who
may get to see transaction data. This uncertainty is mitigated by several factors.
\paragraph{Small-subgraph transactions.}Some uses of the ledger do not involve widely circulated asset states.
For example, two institutions that wish to keep their view of a particular deal synchronised but who are making
@ -378,6 +387,11 @@ be an issue.
\subsection{Transaction structure}
States are the atomic unit of information in Corda. They are never altered: they are either current (`unspent') or
consumed (`spent') and hence no longer valid. Transactions consume zero or more states (inputs) and create zero or more
new states (outputs). Because states cannot exist outside of the transactions that created them, any state whether consumed
or not can be identified by the identifier of the creating transaction and the index of the state in the outputs list.
Transactions consist of the following components:
\begin{labeling}{Input references}
@ -415,6 +429,28 @@ the transaction will not be valid unless every key listed in every command has a
structures are themselves opaque. In this way algorithmic agility is retained: new signature algorithms can be deployed
without adjusting the code of the smart contracts themselves.
\begin{figure}[H]
\includegraphics[width=\textwidth]{cash}
\caption{An example of a cash issuance transaction}
\end{figure}
\paragraph{Example.}In the diagram above, we see an example of a cash issuance transaction. The transaction (shown lower
left) contains zero inputs and one output, a newly issued cash state. The cash state (shown expanded top right) contains
several important pieces of information: 1) details about the cash that has been issued -- amount, currency, issuer,
owner and so forth, 2) the contract code whose verify() function will be responsible for verifying this issuance
transaction and also any transaction which seeks to consume this state in the future, 3) a hash of a document which may
contain overarching legal prose to ground the behaviour of this state and its contract code in a governing legal
context.
The transaction also contains a command, which specifies that the intent of this transaction is to issue cash and the
command specifies a public key. The cash state's verify function is responsible for checking that the public key(s)
specified on the command(s) are those of the parties whose signatures would be required to make this transaction valid.
In this case, it means that the verify() function must check that the command has specified a key corresponding to the
identity of the issuer of the cash state. The Corda framework is responsible for checking that the transaction has been
signed by all keys listed by all commands in the transaction. In this way, a verify() function only needs to ensure that
all parties who need to sign the transaction are specified in Commands, with the framework responsible for ensuring that
the transaction has been signed by all parties listed in all commands.
\subsection{Composite keys}\label{sec:composite-keys}
The term ``public key'' in the description above actually refers to a \emph{composite key}. Composite keys are trees in
@ -424,6 +460,11 @@ determined by walking the tree bottom-up, summing the weights of the keys that h
against the threshold. By using weights and thresholds a variety of conditions can be encoded, including boolean
formulas with AND and OR.
\begin{figure}[H]
\includegraphics[width=\textwidth]{composite-keys}
\caption{Examples of composite keys}
\end{figure}
Composite keys are useful in multiple scenarios. For example, assets can be placed under the control of a 2-of-2
composite key where one leaf key is owned by a user, and the other by an independent risk analysis system. The
risk analysis system refuses to sign if the transaction seems suspicious, like if too much value has been
@ -461,7 +502,7 @@ way to Bitcoin's \texttt{nLockTime} transaction field, which specifies a \emph{h
Timestamps are checked and enforced by notary services. As the participants in a notary service will themselves
not have precisely aligned clocks, whether a transaction is considered valid or not at the moment it is submitted
to a notary may be unpredictable if submission occurs right on a boundary of the given window. However, from the
perspective of all other observers the notaries signature is decisive: if the signature is present, the transaction
perspective of all other observers the notary's signature is decisive: if the signature is present, the transaction
is assumed to have occurred within that time.
\paragraph{Reference clocks.}In order to allow for relatively tight time windows to be used when transactions are fully
@ -521,7 +562,7 @@ states place constraints on the data they're willing to accept. Attachments \emp
there must be a constraints mechanism to prevent that from happening. This is rooted at the contract constraints
encoded in the states themselves: a state can not only name a class that implements the \texttt{Contract}
interface but also place constraints on the zip/jar file that provides it. That constraint can in turn be used to
ensure that the contract checks the authenticity of the data - either by checking the hash of the data directly,
ensure that the contract checks the authenticity of the data -- either by checking the hash of the data directly,
or by requiring the data to be signed by some trusted third party.
% TODO: The code doesn't match this description yet.
@ -530,7 +571,7 @@ or by requiring the data to be signed by some trusted third party.
Decentralised ledger systems often differ in their underlying political ideology as well as their technical
choices. The Ethereum project originally promised ``unstoppable apps'' which would implement ``code as law''. After
a prominent smart contract was hacked, an argument took place over whether what had occurred could be described
a prominent smart contract was hacked\cite{TheDAOHack}, an argument took place over whether what had occurred could be described
as a hack at all given the lack of any non-code specification of what the program was meant to do. The disagreement
eventually led to a split in the community.
@ -636,12 +677,22 @@ in a transaction (in a state or command). We take a different approach in which
and data the oracle doesn't need to see is ``torn off'' before the transaction is sent. This is done by structuring
the transaction as a Merkle hash tree so that the hash used for the signing operation is the root. By presenting a
counterparty with the data elements that are needed along with the Merkle branches linking them to the root hash,
that counterparty can sign the entire transaction whilst only being able to see some of it. Additionally, if the
as seen in the diagrams below, that counterparty can sign the entire transaction whilst only being able to see some of it. Additionally, if the
counterparty needs to be convinced that some third party has already signed the transaction, that is also
straightforward. Typically an oracle will be presented with the Merkle branches for the command or state that
contains the data, and the timestamp field, and nothing else. The resulting signature contains flag bits indicating which
parts of the structure were presented for signing to avoid a single signature covering more than expected.
\begin{figure}[H]
\includegraphics[width=\textwidth]{tearoffs1}
\caption{How the transaction's identifier hash is calculated}
\end{figure}
\begin{figure}[H]
\includegraphics[width=\textwidth]{tearoffs2}
\caption{Construction of a Merkle branch}
\end{figure}
% TODO: The flag bits are unused in the current reference implementation.
There are a couple of reasons to take this more indirect approach. One is to keep a single signature checking
@ -663,7 +714,7 @@ share the signature itself (because it covers a one-time-use structure by defini
Each state in a transaction specifies a contract (boolean function) that is invoked with the entire transaction as input. All contracts must accept
in order for the transaction to be considered valid. Sometimes we would like to compose the behaviours of multiple
different contracts. Consider the notion of a ``time lock'' - a restriction on a state that prevents it being
different contracts. Consider the notion of a ``time lock'' -- a restriction on a state that prevents it being
modified (i.e. sold) until a certain time. This is a general piece of logic that could apply to many kinds of
assets. Whilst such logic could be implemented in a library and then called from every contract that might want
to benefit from it, that requires all contract authors to think ahead and include the functionality. It would be
@ -741,8 +792,8 @@ kilograms of bananas, units of a stock and so on.
When cash is represented on a digital ledger an additional complication can arise: for national ``fiat'' currencies
the ledger merely records an entity that has a liability which may be redeemed for some other form (physical currency,
a wire transfer via some other ledger system, etc). This means that two ledger entries of \pounds1000 may \emph{not}
be entirely fungible because all the entries really represent is a claim on an issuer, which - if it is not a central
bank - may go bankrupt. Even assuming defaults never happen, the data representing where an asset may be redeemed
be entirely fungible because all the entries really represent is a claim on an issuer, which -- if it is not a central
bank -- may go bankrupt. Even assuming defaults never happen, the data representing where an asset may be redeemed
must be tracked through the chain of custody, so `exiting' the asset from the ledger and thus claiming physical
ownership can be done.
@ -751,7 +802,7 @@ quantity of some token. This type does not support fractional quantities so when
currencies the quantity must be measured in pennies, with sub-penny amount requiring the use of some other type.
The token can be represented by any type. A common token type to use is \texttt{Issued<T>}, which defines a token
issued by some party. It encapsulates what the asset is, who issued it, and an opaque reference field that is not
parsed by the platform - it is intended to help the issuer keep track of e.g. an account number, the location where
parsed by the platform -- it is intended to help the issuer keep track of e.g. an account number, the location where
the asset can be found in storage, etc.
\subsection{Obligations}
@ -784,6 +835,11 @@ can be rewritten. If a group of trading institutions wish to implement a checked
can use an encumbrance (see \cref{sec:encumbrances}) to prevent an obligation being changed during certain hours,
as determined by the clocks of the notaries (see \cref{sec:timestamps}).
\begin{figure}[H]
\includegraphics[width=\textwidth]{state-class-hierarchy}
\caption{Class hierarchy diagram showing the relationships between different state types}
\end{figure}
\subsection{Market infrastructure}
Trade is the lifeblood of the economy. A distributed ledger needs to provide a vibrant platform on which trading may
@ -795,7 +851,7 @@ from a central meeting point.
The Corda data model allows for integration of the ledger with existing markets and exchanges. A sell order for
an asset that exists on-ledger can have a \emph{partially signed transaction} attached to it. A partial
signature is a signature that allows the signed data to be changed in controlled ways after signing. Partial signatures
are directly equivalent to Bitcoin's \texttt{SIGHASH} flags and work in the same way - signatures contain metadata
are directly equivalent to Bitcoin's \texttt{SIGHASH} flags and work in the same way -- signatures contain metadata
describing which parts of the transaction are covered. Normally all of a transaction would be covered, but using this
metadata it is possible to create a signature that only covers some inputs and outputs, whilst allowing more to be
added later.
@ -822,7 +878,7 @@ future distributed ledger services contemplated by CCPs and CSDs.
\section{Notaries and consensus}\label{sec:notaries}
Corda does not organise time into blocks. This is sometimes considered strange, given that it can be described as a
blockchain system or `blockchain inspired'. Instead a Corda network has one or more notary services which provide
block chain system or `block chain inspired'. Instead a Corda network has one or more notary services which provide
transaction ordering and timestamping services, thus abstracting the role miners play in other systems into a pluggable
component.
@ -850,7 +906,7 @@ a reward of newly issued bitcoins, an unrecognised block represents a loss and a
a profit.
Bitcoin uses proof-of-work because it has a design goal of allowing an unlimited number of identityless parties to join
and leave the network at will, whilst simultaneously making it hard to execute sybil attacks (attacks in which one party
and leave the network at will, whilst simultaneously making it hard to execute Sybil attacks (attacks in which one party
creates multiple identities to gain undue influence over the network). This is an appropriate design to use for a peer to
peer network formed of volunteers who can't/won't commit to any long term relationships up front, and in which identity
verification is not done. Using proof-of-work then leads naturally to a requirement to quantise the timeline into chunks,
@ -867,14 +923,14 @@ its multiple unfortunate downsides:
\begin{itemize}
\item Energy consumption is excessively high for such a simple task, being comparable at the time of writing to the
consumption of an entire town. At a time when humanity needs to use less energy rather than more this is ecologically
undesirable.
electricity consumption of an entire city\cite{BitcoinEnergy}. At a time when humanity needs to use less energy
rather than more this is ecologically undesirable.
\item High energy consumption forces concentration of mining power in regions with cheap or free electricity. This results
in unpredictable geopolitical complexities that many users would rather do without.
\item Identityless participants mean all transactions must be broadcast to all network nodes, as there's no reliable
way to know who the miners are. This worsens privacy.
\item The algorithm does not provide finality, only a probabilistic approximation, which is a poor fit for existing
business and legal assumptions.
business and legal assumptions.\cite{Swanson}
\item It is theoretically possible for large numbers of miners or even all miners to drop out simultaneously without
any protocol commitments being violated.
\end{itemize}
@ -1002,7 +1058,7 @@ and thus does not know who is involved with the operation (assuming source IP ad
\section{The vault}\label{sec:vault}
In any blockchain based system most nodes have a wallet, or as we call it, a vault.
In any block chain based system most nodes have a wallet, or as we call it, a vault.
The vault contains data extracted from the ledger that is considered \emph{relevant} to the node's owner, stored in a form
that can be easily queried and worked with. It also contains private key material that is needed to sign transactions
@ -1123,19 +1179,21 @@ interprets them.
Domain specific languages for the expression of financial contracts are a popular area of research. A seminal work
is `Composing contracts' by Peyton-Jones, Seward and Eber [PJSE2000\cite{PeytonJones:2000:CCA:357766.351267}] in which
financial contracts are modelled with a small library of Haskell combinators. These models can then be used for
valuation of the underlying deals. Blockchain systems use the term `contract' in a slightly different sense to
valuation of the underlying deals. Block chain systems use the term `contract' in a slightly different sense to
how PJSE do but the underlying concepts can be adapted to our context as well. The platform provides an
experimental \emph{universal contract} that builds on the language extension features of the Kotlin programming
language. To avoid linguistic confusion it refers to the combined code/data bundle as an `arrangement' rather
than a contract. A European FX option expressed in this language looks like this:
than a contract. A European FX call option expressed in this language looks like this:
\newpage
\begin{kotlincode}
val european_fx_option = arrange {
actions {
acmeCorp.may {
"exercise".anytime {
acmeCorp may {
"exercise" anytime {
actions {
(acmeCorp or highStreetBank).may {
(acmeCorp or highStreetBank) may {
"execute".givenThat(after("2017-09-01")) {
highStreetBank.owes(acmeCorp, 1.M, EUR)
acmeCorp.owes(highStreetBank, 1200.K, USD)
@ -1144,7 +1202,7 @@ than a contract. A European FX option expressed in this language looks like this
}
}
}
highStreetBank.may {
highStreetBank may {
"expire".givenThat(after("2017-09-01")) {
zero
}
@ -1186,7 +1244,7 @@ smart contract logic may be appreciated by the users.
\subsection{Background}
A common feature of digital financial systems and blockchain-type systems in particular is the use of secure client-side
A common feature of digital financial systems and block chain-type systems in particular is the use of secure client-side
hardware to hold private keys and perform signing operations with them. Combined with a zero tolerance approach to
transaction rollbacks, this is one of the ways they reduce overheads: by attempting to ensure that transaction
authorisation is robust and secure, and thus that signatures are reliable.
@ -1220,7 +1278,7 @@ node not having any ability to sign for transactions itself:
\item If the node is hacked by a malicious intruder or bad insider they cannot steal assets, modify agreements,
or do anything else that requires human approval, because they don't have access to the signing keys. There is no single
point of failure from a key management perspective.
\item It's more clear who signed off on a particular action - the signatures prove which devices were used to sign off
\item It's more clear who signed off on a particular action -- the signatures prove which devices were used to sign off
on an action. There can't be any back doors or administrator tools which can create transactions on behalf of someone else.
\item Devices that integrate fingerprint readers and other biometric authentication could further increase trust by
making it harder for employees to share/swap devices. A smartphone or tablet could be also used as a transaction authenticator.
@ -1230,7 +1288,7 @@ making it harder for employees to share/swap devices. A smartphone or tablet cou
The biggest problem facing anyone wanting to integrate smart signing devices into a distributed ledger system is how the
device processes transactions. For Bitcoin it's straightforward for devices to process transactions directly because
their format is very small and simple (in theory - in practice a fixable quirk of the Bitcoin protocol actually
their format is very small and simple (in theory -- in practice a fixable quirk of the Bitcoin protocol actually
significantly complicates how these devices must work). Thus turning a Bitcoin transaction into a human meaningful
confirmation screen is quite easy:
@ -1365,7 +1423,7 @@ human consumption at all.
Once a group is created other nodes can be invited to join it by using an invitation flow. Membership can be either
read only or read/write. To add a node as read-only, the certificate i.e. pubkey alone is sent. To add a node as
read/write the cert and private key are sent. A future elaboration on the design may support giving each member a
read/write the certificate and private key are sent. A future elaboration on the design may support giving each member a
separate private key which would allow tracing who added transactions to a group, but this is left for future work.
In either case the node records in its local database which other nodes it has invited to the group once they accept
the invitation.
@ -1392,7 +1450,7 @@ any nodes that have recently sent us this transaction and then kicks off a \text
with each of them. The other side of this flow checks if the transaction is already known, if not requests it, checks
that it is indeed signed by the group in question, resolves it and then assuming success, sends it to the vault. In this
way a transaction added by any member of the group propagates up and down the membership tree until all the members have
seen it. Propagation is idempotent - if the vault has already seen a transaction before then it isn't processed again.
seen it. Propagation is idempotent -- if the vault has already seen a transaction before then it isn't processed again.
The structure we have so far has some advantages and one big disadvantage. The advantages are:
@ -1506,8 +1564,8 @@ opcode-at-a-time accounting turns out to be insufficient.
A further complexity comes from the need to constrain memory usage. The sandbox imposes a quota on bytes \emph{allocated}
rather than bytes \emph{retained} in order to simplify the implementation. This strategy is unnecessarily harsh on smart
contracts that churn large quantities of garbage yet have relatively small peak heap sizes and, again, it may be that
in practice a more sophisticated strategy that integrates with the GC is required in order to set quotas to a usefully
generic level.
in practice a more sophisticated strategy that integrates with the garbage collector is required in order to set
quotas to a usefully generic level.
Control over \texttt{Object.hashCode()} takes the form of new JNI calls that allow the JVM's thread local random number
generator to be reseeded before execution begins. The seed is derived from the hash of the transaction being verified.
@ -1517,7 +1575,7 @@ reach. In particular this means that the `shadow JDK' is also instrumented and s
\section{Scalability}
Scalability of blockchains and blockchain inspired systems has been a constant topic of discussion since Nakamoto
Scalability of block chains and block chain inspired systems has been a constant topic of discussion since Nakamoto
first proposed the technology in 2008. We make a variety of choices and tradeoffs that affect and
ensure scalability. As most of the initial intended use cases do not involve very high levels of traffic, the
reference implementation is not heavily optimised. However, the architecture allows for much greater levels of
@ -1585,7 +1643,7 @@ any NoSQL database (such as Cassandra), at the cost of a more complex backup str
Due to partial visibility nodes check transaction graphs `just in time' rather than as a steady stream of
announcements by other participants. This complicates the question of how to measure the scalability of a Corda
node. Other blockchain systems quote performance as a constant rate of transactions per unit time.
node. Other block chain systems quote performance as a constant rate of transactions per unit time.
However, our `unit time' is not evenly distributed: being able to check 1000 transactions/sec is not
necessarily good enough if on presentation of a valuable asset you need to check a transation graph that consists
of many more transactions and the user is expecting the transaction to show up instantly. Future versions of

Binary file not shown.

After

Width:  |  Height:  |  Size: 35 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 119 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 89 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 76 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 214 KiB

View File

@ -158,7 +158,7 @@ class ActionBuilder(val actors: Set<Party>) {
}
}
fun String.anytime(init: ContractBuilder.() -> Unit): Action {
infix fun String.anytime(init: ContractBuilder.() -> Unit): Action {
val b = ContractBuilder()
b.init()
val a = Action(this, const(true), actors, b.final())