diff --git a/specification-v3.html b/specification-v3.html new file mode 100644 index 0000000..6acc96f --- /dev/null +++ b/specification-v3.html @@ -0,0 +1,6566 @@ + + + + + + + + + + + + + + + + + +
+
Marlowe Specification
Version 3
Pablo Lamela Seijas Alexander Nemish David Smith
Simon Thompson Hernán Rajchert Brian Bush
December 31, 1979
+
Contents
1 Marlowe 2
1.1 Introduction ............................ 2
1.2 The Marlowe Model ........................ 3
1.2.1 Data types ......................... 3
1.2.2 Quiescent ......................... 3
1.2.3 Participants, accounts and state ............. 3
1.2.4 Core and Extended .................... 4
1.3 Specification generation and nomenclature ........... 4
1.4 Blockchain agnostic ....................... 4
2 Marlowe Core 6
2.1 Types ............................... 6
2.1.1 Participants, roles and addresses ............ 6
2.1.2 Multi-Asset token ..................... 7
2.1.3 Accounts ......................... 7
2.1.4 Choices .......................... 8
2.1.5 Values and Observations ................. 8
2.1.6 Actions and inputs .................... 9
2.1.7 Contracts ......................... 10
2.1.8 State and Environment ................. 12
2.2 Semantics ............................. 12
2.2.1 Compute Transaction ................... 13
2.2.2 Fix Interval ........................ 14
2.2.3 Apply All Inputs ..................... 14
2.2.4 Reduce Contract Until Quiescent ............ 15
2.2.5 Reduction Loop ...................... 16
2.2.6 Reduce Contract Step .................. 16
2.2.7 Apply Input ........................ 18
2.2.8 Apply Cases ........................ 19
2.2.9 Utilities .......................... 20
2.2.10 Evaluate Value ...................... 21
1
+
2.2.11 Evaluate Observation ................... 24
3 Marlowe Guarantees 26
3.1 Money Preservation ........................ 26
3.2 Contracts Always Close ...................... 27
3.3 Positive Accounts ......................... 27
3.4 Quiescent Result ......................... 28
3.5 Reducing a Contract until Quiescence Is Idempotent ..... 28
3.6 Split Transactions Into Single Input Does Not Affect the Result 28
3.6.1 Termination Proof .................... 29
3.6.2 All Contracts Have a Maximum Time .......... 29
3.6.3 Contract Does Not Hold Funds After it Closes ..... 29
3.6.4 Transaction Bound .................... 29
A Contract examples 30
A.1 Simple Swap ............................ 30
A.1.1 Contract definition .................... 30
A.1.2 Example execution .................... 32
A.1.3 Contract guarantees ................... 33
B ByteString 35
B.1 Ordering .............................. 36
C Code exports 38
D Marlowe Core JSON 41
D.1 Party ................................ 41
D.2 Token ............................... 42
D.3 Payee ............................... 42
D.4 ChoicesId ............................. 43
D.5 Bound ............................... 44
D.6 Values ............................... 44
D.7 Observation ............................ 49
D.8 Action ............................... 53
D.9 Case ................................ 55
D.10 Contract .............................. 56
D.11 Input ................................ 61
D.12 Transaction ............................ 63
D.13 Payment .............................. 64
D.14 State ................................ 65
D.15 TransactionWarning ........................ 67
2
+
D.16 IntervalError ........................... 71
D.17 TransactionError ......................... 72
D.18 TransactionOutput ........................ 74
D.19 Full Contract Example ...................... 77
D.20 Parse utils ............................. 79
3
+
Chapter 1
Marlowe
1.1 Introduction
Marlowe is a special purpose or domain-specific language (DSL) that is de-
signed to be usable by someone who is expert in the field of financial con-
tracts, somewhat lessening the need for programming skills.
Marlowe is modelled on special-purpose financial contract languages popu-
larised in the last decade or so by academics and enterprises such as LexiFi
1, which provides contract software in the financial sector. In developing
Marlowe, we have adapted these languages to work on any blockchain §1.4.
Where we differ from non-blockchain approaches is in how we make sure
that the contract is followed. In the smart contracts world there is a saying
“Code is law”, which implies that the assets deposited in a contract will
follow its logic, without the ability of a human to change the rules. This
applies for both the intended and not intended behaviour (in the form of
bugs or exploits).
To reduce the probability of not intended behaviour, the Marlowe DSL is
designed with simplicity in mind. Without loops, recursion, or other features
that general purposes smart-contract languages (E.g: Plutus, Solidity) have,
it is easier to make certain claims. Each Marlowe contract can be reasoned
with a static analizer to avoid common pitfalls such as trying to Pay more
money than the available. And the executable semantics that dictates the
logic of all Marlowe contracts is formalized with the proof-assistant Isabelle.
Chapter §1provides an overview of the Marlowe language. Chapter §2defines
the Core language and semantics in detail. Chapter §3presents proofs that
1https://www.lexifi.com/
4
+
guarantee that Marlowe contracts possess properties desirable for financial
agreements.
1.2 The Marlowe Model
Marlowe Contracts describe a series of steps, typically by describing the first
step, together with another (sub-)contract that describes what to do next.
For example, the contract Pay a p t v c says “make a payment of vnumber
of tokens tto the party pfrom the account a, and then follow the contract
c”. We call cthe continuation of the contract. All paths of the contract are
made explicit this way, and each Contract term is executed at most once.
1.2.1 Data types
The Values and Observations §2.1.5 only works with integers and booleans
respectively. There are no custom data types, records, tuples, nor string ma-
nipulation. There are also no floating point numbers, so in order to represent
currencies it is recommended to work with cents. Dates are only used in the
context of Timeouts and they are absolute, but it is likely we’ll add relative
times in a future version.
1.2.2 Quiescent
The blockchain can’t force a participant to make a transaction. To avoid
having a participant blocking the execution of a contract, whenever an Input
is expected, there is a Timeout with a contingency continuation. For each
step, we can know in advance how long it can last, and we can extend this to
know the maximum duration and the amount of transactions of a contract.
1.2.3 Participants, accounts and state
Once we define a contract, we can see how many participants it will have.
The number of participants is fixed for the duration of the contract, but there
are mechanisms to trade participation §2.1.1.
Each participant has an internal account that allows the contract to define
default owner for assets §2.1.3. Whenever a Party deposits an asset in the
contract, they need to decide the default owner of that asset. Payments can
be made to transfer the default owner or to take the asset out of the contract.
5
+
If the contract is closed, the default owner can redeem the assets available in
their internal accounts.
The accounts, choices, and variables stored in the State §2.1.8 are global to
that contract.
1.2.4 Core and Extended
The set of types and functions that conform the semantics executed in the
blockchain is called Marlowe Core, and it’s formalized in chapter §2. To
improve usability, there is another set of types and functions that compile to
core, and it is called Marlowe Extended.
In the first version of the extended language, the only modification to the
DSL is the addition of template parameters. These allows an initial form
of contract reutilization, allowing to instantiate the same contract with dif-
ferent Values and Timeouts. For the moment, the extended language is not
formalized in this specification but it will be added in the future
1.3 Specification generation and nomenclature
The Marlowe specification is formalized using the proof assistant Isabelle2.
The code is written in a literate programming style and this document is
generated from the proofs. This improves code documentation and lowers
the probability of stale information.
As a drawback, the code/doc organization is more rigid. Isabelle require us to
define code in a bottom-up approach, having to define first the dependencies
and later the most complex structures.
The notation is closer to a Mathematical formula than a functional program-
ming language. There are some configurations in the SpecificationLatexSugar
theory file that makes the output be closer to code.
1.4 Blockchain agnostic
Marlowe is currently implemented on the Cardano Blockchain, but it is de-
signed to be Blockchain agnostic.
2https://isabelle.in.tum.de/
6
+
Programs written in languages like Java and Python can be run on differ-
ent architectures, like amd64 or arm64, because they have interpreters and
runtimes for them. In the same way, the Marlowe interpreter could be im-
plemented to run on other blockchains, like Ethereum, Solana for example.
We make the following assumptions on the underlying Blockchain that allow
Marlowe Semantics to serve as a common abstraction:
In order to define the different Tokens that are used as currency in the
participants accounts §2.1.3, deposits, and payments, we need to be able to
express a TokenName and CurrencySymbol.
type-synonym TokenName =ByteString
type-synonym CurrencySymbol =ByteString
To define a fixed participant in the contract §2.1.1 and to make payouts to
them, we need to express an Address.
type-synonym Address =ByteString
In the context of this specification, these ByteString types are opaque, and we
don’t enforce a particular encoding or format, only that they can be sorted
§B.
The Timeouts that prevent us from waiting forever for external Inputs are
represented by the number of milliseconds from the Unix Epoch 3.
type-synonym POSIXTime =int
type-synonym Timeout =POSIXTime
The TimeInterval that defines the validity of a transaction is a tuple of
exclusive start and end time.
type-synonym TimeInterval =POSIXTime ×POSIXTime
3January 1st, 1970 at 00:00:00 UTC
7
+
Chapter 2
Marlowe Core
2.1 Types
This section introduces the data types of Marlowe Core, which are composed
by the Marlowe DSL and also the types required to compute a Transaction.
Because of the literate programming nature of Isabelle §1.3, the types are
defined bottom-up. To follow just the DSL, a reader can start by looking at
aContract definition §2.1.7.
2.1.1 Participants, roles and addresses
We should separate the notions of participant, role, and address in a Marlowe
contract. A participant (or Party) in the contract can be represented by
either a fixed Address or a Role.
type-synonym RoleName =ByteString
datatype Party =
Address Address
|Role RoleName
An address party is defined by a Blockhain specific Address §1.4 and it cannot
be traded (it is fixed for the lifetime of a contract).
ARole, on the other hand, allows the participation of the contract to be
dynamic. Any user that can prove to have permission to act as RoleName
is able to carry out the actions assigned §2.1.6, and redeem the payments
issued to that role. The roles could be implemented as tokens1that can be
1In the Cardano implementation roles are represented by native tokens and they are
8
+
traded. By minting multiple tokens for a particular role, several people can
be given permission to act on behalf of that role simultaneously, this allows
for more complex use cases.
2.1.2 Multi-Asset token
Inspired by Cardano’s Multi-Asset tokens 2, Marlowe also supports to trans-
act with different assets. A Token consists of a CurrencySymbol that repre-
sents the monetary policy of the Token and a TokenName which allows to
have multiple tokens with the same monetary policy.
datatype Token =Token CurrencySymbol TokenName
The Marlowe semantics treats both types as opaque ByteString.
2.1.3 Accounts
The Marlowe model allows for a contract to store assets. All participants of
the contract implicitly own an account identified with an AccountId.
type-synonym AccountId =Party
All assets stored in the contract must be in an internal account for one of
the parties; this way, when the contract is closed, all remaining assets can
be redeemed by their respective owners. These accounts are local: they only
exist (and are accessible) within the contract.
type-synonym Accounts = ((AccountId ×Token)×int)list
During its execution, the contract can invite parties to deposit assets into an
internal account through the construct “When [Deposit accountId party token
value]timeout continuation" . The contract can transfer assets internally
(between accounts) or externally (from an account to a party) by using the
term "Pay accountId payee token value continuation”, where Payee is:
datatype Payee =Account AccountId
|Party Party
APay always takes money from an internal AccountId, and the Payee defines
if we transfer internally (Account p) or externally (Party p)
distributed to addresses at the time a contract is deployed to the blockchain
2https://docs.cardano.org/native-tokens/learn
9
+
2.1.4 Choices
Choices – of integers – are identified by ChoiceId which is defined with a
canonical name and the Party who had made the choice:
type-synonym ChoiceName =ByteString
datatype ChoiceId =ChoiceId ChoiceName Party
Choices are Bounded. As an argument for the Choice action §2.1.6, we pass
a list of Bounds that limit the integer that we can choose. The Bound data
type is a tuple of integers that represents an inclusive lower and upper
bound.
datatype Bound =Bound int int
2.1.5 Values and Observations
We can store a Value in the Marlowe State §2.1.8 using the Let construct
§2.1.7, and we use a ValueId to referrence it
datatype ValueId =ValueId ByteString
Values and Observations are language terms that interact with most of the
other constructs. Value evaluates to an integer and Observation evaluates to
a boolean using evalValue §2.2.10 and evalObservation §2.2.11 respectively.
They are defined in a mutually recursive way as follows:
datatype Value =AvailableMoney AccountId Token
|Constant int
|NegValue Value
|AddValue Value Value
|SubValue Value Value
|MulValue Value Value
|DivValue Value Value
|ChoiceValue ChoiceId
|TimeIntervalStart
|TimeIntervalEnd
|UseValue ValueId
|Cond Observation Value Value
and Observation =AndObs Observation Observation
|OrObs Observation Observation
|NotObs Observation
|ChoseSomething ChoiceId
|ValueGE Value Value
|ValueGT Value Value
10
+
|ValueLT Value Value
|ValueLE Value Value
|ValueEQ Value Value
|TrueObs
|FalseObs
Three of the Value terms look up information in the Marlowe state: Avail-
ableMoney p t reports the amount of token tin the internal account of party
p;ChoiceValue i reports the most recent value chosen for choice i, or zero if
no such choice has been made; and UseValue i reports the most recent value
of the variable i, or zero if that variable has not yet been set to a value.
Constant v evaluates to the integer v, while NegValue x,AddValue x y,Sub-
Value x y,MulValue x y, and DivValue x y provide the common arithmetic
operations −x,x+y,x−y,x∗y, and x/y, where division always rounds
(truncates) its result towards zero.
Cond b x y represents a condition expression that evaluates to xif bis true
and to yotherwise.
The last Values, TimeIntervalStart and TimeIntervalEnd, evaluate respec-
tively to the start or end of the validity interval for the Marlowe transaction.
For the observations, the ChoseSomething i term reports whether a choice i
has been made thus far in the contract.
The terms TrueObs and FalseObs provide the logical constants true and false.
The logical operators ¬x,x∧y, and x∨yare represented by the terms
NotObs x,AndObs x y, and OrObs x y, respectively.
Value comparisons x<y,x≤y,x>y,x≥y, and x=yare represented
by ValueLT x y,ValueLE x y,ValueGT x y,ValueGE x y, and ValueEQ x y.
2.1.6 Actions and inputs
Actions and Inputs are closely related. An Action can be added in a list of
Cases §2.1.7 as a way to declare the possible external Inputs a Party can
include in a Transaction at a certain time.
The different types of actions are:
datatype Action =Deposit AccountId Party Token Value
|Choice ChoiceId Bound list
|Notify Observation
11
+
ADeposit a p t v makes a deposit of #v Tokenstfrom Party p into account
a.
A choice Choice i bs is made for a particular choice identified by the ChoiceId
§2.1.4 iwith a list of inclusive bounds bs on the values that are acceptable.
For example, [Bound 0 0 ,Bound 3 5 ]offers the choice of one of 0, 3, 4 and
5.
A notification can be triggered by anyone as long as the Observation evaluates
to true. If multiple Notify are present in the Case list, the first one with a
true observation is matched.
For each Action, there is a corresponding Input that can be included inside
aTransaction
type-synonym ChosenNum =int
datatype Input =IDeposit AccountId Party Token int
|IChoice ChoiceId ChosenNum
|INotify
The differences between them are:
•Deposit uses a Value while IDeposit has the int it was evaluated to
with evalValue §2.2.10.
•Choice defines a list of valid Bounds while IChoice has the actual Cho-
senNum.
•Notify has an Observation while INotify does not have arguments, the
Observation must evaluate to true inside the Transaction
2.1.7 Contracts
Marlowe is a continuation-based language, this means that a Contract can
either be a Close or another construct that recursively has a Contract. Even-
tually, all contracts end up with a Close construct.
Case and Contract are defined in a mutually recursive way as follows:
datatype Case =Case Action Contract
and Contract =Close
|Pay AccountId Payee Token Value Contract
|If Observation Contract Contract
12
+
|When Case list Timeout Contract
|Let ValueId Value Contract
|Assert Observation Contract
Close is the simplest contract, when we evaluate it, the execution is completed
and we generate Payments §?? for the assets in the internal accounts to their
default owners 3.
The contract Payaptvc, generates a Payment from the internal account a
to a payee §2.1.3 pof #v Tokens and then continues to contract c. Warnings
will be generated if the value vis not positive, or if there is not enough in the
account to make the payment in full. In the latter case, a partial payment
(of the available amount) is made
The contract If obs x y allows branching. We continue to branch xif the
Observation obs evaluates to true, or to branch yotherwise.
When is the most complex constructor for contracts, with the form When cs
t c. The list cs contains zero or more pairs of Actions and Contract continu-
ations. When we do a computeTransaction §2.2.1, we follow the continuation
associated to the first Action that matches the Input. If no action is matched
it returns a ApplyAllNoMatchError. If a valid Transaction is computed with
aTimeInterval with a start time bigger than the Timeout t, the contingency
continuation cis evaluated. The explicit timeout mechanism is what allows
Marlowe to avoid waiting forever for external inputs.
ALet contract Let i v c allows a contract to record a value using an identifier
i. In this case, the expression vis evaluated, and the result is stored with
the name i. The contract then continues as c. As well as allowing us to
use abbreviations, this mechanism also means that we can capture and save
volatile values that might be changing with time, e.g. the current price of oil,
or the current time, at a particular point in the execution of the contract, to
be used later on in contract execution.
An assertion contract Assert b c does not have any effect on the state of
the contract, it immediately continues as c, but it issues a warning if the
observation bevaluates to false. It can be used to ensure that a property
holds in a given point of the contract, since static analysis will fail if any
execution causes a warning. The Assert term might be removed from future
on-chain versions of Marlowe.
3Even if the payments are generated one at a time (per account and per Token), the
cardano implementation generates a single transaction
13
+
2.1.8 State and Environment
The internal state of a Marlowe contract consists of the current balances in
each party’s account, a record of the most recent value of each type of choice,
a record of the most recent value of each variable, and the lower bound for the
current time that is used to refine time intervals and ensure TimeIntervalStart
never decreases. The data for accounts, choices, and bound values are stored
as association lists.
record State =accounts :: Accounts
choices :: (ChoiceId ×ChosenNum)list
boundValues :: (ValueId ×int)list
minTime :: POSIXTime
The execution environment of a Marlowe contract simply consists of the
(inclusive) time interval within which the transaction is occurring.
record Environment =timeInterval :: TimeInterval
— TODO: see if we want to add data types of Semantic here (Transaction, etc)
or if we want to move this types to Semantic
datatype IntervalError =InvalidInterval TimeInterval
|IntervalInPastError POSIXTime TimeInterval
datatype IntervalResult =IntervalTrimmed Environment State
|IntervalError IntervalError
2.2 Semantics
Marlowe’s behavior is defined via the operational semantics (or executable
semantics) of the Isabelle implementation of its computeTransaction func-
tion. That function calls several auxiliary functions to apply inputs and find
a quiescent state of the contract. These, in turn, call evaluators for Value
and Observation.
14
+
2.2.1 Compute Transaction
The entry point into Marlowe semantics is the function computeTransaction
that applies input to a prior state to transition to a posterior state, perhaps
reporting warnings or throwing an error, all in the context of an environment
for the transaction.
computeTransaction :: Transaction ⇒State ⇒Contract ⇒TransactionOut-
put
FIXME: Print record: Transaction
datatype TransactionOutput =
TransactionOutput
TransactionOutputRecord
|TransactionError TransactionError
FIXME: Print record: TransactionOutputRecord
This function adjusts the time interval for the transaction using fixInter-
val and then applies all of the transaction inputs to the contract using ap-
plyAllInputs. It reports relevant warnings and throws relevant errors.
computeTransaction ::
Transaction_ext () -> State_ext () -> Contract -> TransactionOutput;
computeTransaction tx state contract =
let {
inps = inputs tx;
} in (case fixInterval (interval tx) state of {
IntervalTrimmed env fixSta ->
(case applyAllInputs env fixSta contract inps of {
ApplyAllSuccess reduced warnings payments newState cont
->
(if not reduced &&
(not (equal_Contract contract Close) ||
null (accounts state))
then TransactionError TEUselessTransaction
else TransactionOutput
(TransactionOutputRecord_ext warnings payments
newState
cont ()));
ApplyAllNoMatchError -> TransactionError TEApplyNoMatchError;
ApplyAllAmbiguousTimeIntervalError ->
15
+
TransactionError TEAmbiguousTimeIntervalError;
});
IntervalError errora -> TransactionError (TEIntervalError errora);
});
2.2.2 Fix Interval
The fixInterval functions combines the minimum-time constraint of State
with the time interval of Environment to yield a “trimmed” validity interval
and a minimum time for the new state that will result from applying the
transaction. It throws an error if the interval is nonsensical or in the past.
FIXME: print type synonym: IntervalResult
fixInterval :: (Int, Int) -> State_ext () -> IntervalResult;
fixInterval (low, high) state =
let {
curMinTime = minTime state;
newLow = max low curMinTime;
curInterval = (newLow, high);
env = Environment_ext curInterval ();
newState = minTime_update (\ _ -> newLow) state;
} in (if less_int high low then IntervalError (InvalidInterval (low,
high))
else (if less_int high curMinTime
then IntervalError (IntervalInPastError curMinTime (low,
high))
else IntervalTrimmed env newState));
2.2.3 Apply All Inputs
The applyAllInputs function iteratively progresses the contract and applies
the transaction inputs to the state, checking for errors along the way and con-
tinuing until all the inputs are consumed and the contract reaches a quiescent
state.
applyAllInputs ::
Environment_ext () -> State_ext () -> Contract -> [Input] -> ApplyAllResult;
applyAllInputs env state contract inputs =
applyAllLoop False env state contract inputs [] [];
16
+
applyAllLoop ::
Bool ->
Environment_ext () ->
State_ext () ->
Contract ->
[Input] -> [TransactionWarning] -> [Payment] -> ApplyAllResult;
applyAllLoop contractChanged env state contract inputs warnings payments
=
(case reduceContractUntilQuiescent env state contract of {
ContractQuiescent reduced reduceWarns pays curState cont ->
(case inputs of {
[] -> ApplyAllSuccess (contractChanged || reduced)
(warnings ++ convertReduceWarnings reduceWarns)
(payments ++ pays) curState cont;
input : rest ->
(case applyInput env curState input cont of {
Applied applyWarn newState conta ->
applyAllLoop True env newState conta rest
(warnings ++
convertReduceWarnings reduceWarns ++
convertApplyWarning applyWarn)
(payments ++ pays);
ApplyNoMatchError -> ApplyAllNoMatchError;
});
});
RRAmbiguousTimeIntervalError -> ApplyAllAmbiguousTimeIntervalError;
});
2.2.4 Reduce Contract Until Quiescent
The reduceContractUntilQuiescent executes as many non-input steps of the
contract as is possible. Marlowe semantics do not allow partial execution of
a series of non-input steps.
reduceContractUntilQuiescent ::
Environment_ext () -> State_ext () -> Contract -> ReduceResult;
reduceContractUntilQuiescent env state contract =
reductionLoop False env state contract [] [];
17
+
2.2.5 Reduction Loop
The reductionLoop function attempts to apply the next, non-input step to
the contract. It emits warnings along the way and it will through an error if
it encounters an ambiguous time interval.
reductionLoop ::
Bool ->
Environment_ext () ->
State_ext () -> Contract -> [ReduceWarning] -> [Payment] -> ReduceResult;
reductionLoop reduced env state contract warnings payments =
(case reduceContractStep env state contract of {
Reduced warning effect newState ncontract ->
let {
newWarnings =
(if equal_ReduceWarning warning ReduceNoWarning then warnings
else warning : warnings);
a = (case effect of {
ReduceNoPayment -> payments;
ReduceWithPayment payment -> payment : payments;
});
} in reductionLoop True env newState ncontract newWarnings a;
NotReduced ->
ContractQuiescent reduced (reverse warnings) (reverse payments)
state
contract;
AmbiguousTimeIntervalReductionError -> RRAmbiguousTimeIntervalError;
});
2.2.6 Reduce Contract Step
The reduceContractStep function handles the progression of the Contract
in the absence of inputs: it performs the relevant action (payments, state-
change, etc.), reports warnings, and throws errors if needed. It stops reducing
the contract at the point when the contract requires external input.
Note that this function should report an implicit payment of zero (due to
lack of funds) as a partial payment of zero, not as a non-positive payment.
An explicit payment of zero (due to the contract actually specifying a zero
payment) should be reported as a non-positive payment.
18
+
reduceContractStep ::
Environment_ext () -> State_ext () -> Contract -> ReduceStepResult;
reduceContractStep uu state Close =
(case refundOne (accounts state) of {
Nothing -> NotReduced;
Just ((party, (token, money)), newAccount) ->
let {
newState = accounts_update (\ _ -> newAccount) state;
} in Reduced ReduceNoWarning
(ReduceWithPayment (Payment party (Party party) token money))
newState Close;
});
reduceContractStep env state (Pay accId payee token val cont) =
let {
moneyToPay = evalValue env state val;
} in (if less_eq_int moneyToPay Zero_int
then let {
warning = ReduceNonPositivePay accId payee token moneyToPay;
} in Reduced warning ReduceNoPayment state cont
else let {
balance = moneyInAccount accId token (accounts state);
paidMoney = min balance moneyToPay;
newBalance = minus_int balance paidMoney;
newAccs =
updateMoneyInAccount accId token newBalance (accounts
state);
warning =
(if less_int paidMoney moneyToPay
then ReducePartialPay accId payee token paidMoney
moneyToPay
else ReduceNoWarning);
} in (case giveMoney accId payee token paidMoney newAccs
of {
(payment, finalAccs) ->
Reduced warning payment
(accounts_update (\ _ -> finalAccs) state) cont;
}));
reduceContractStep env state (If obs cont1 cont2) =
let {
a = (if evalObservation env state obs then cont1 else cont2);
} in Reduced ReduceNoWarning ReduceNoPayment state a;
reduceContractStep env state (When uv timeout cont) =
(case timeInterval env of {
19
+
(startTime, endTime) ->
(if less_int endTime timeout then NotReduced
else (if less_eq_int timeout startTime
then Reduced ReduceNoWarning ReduceNoPayment state cont
else AmbiguousTimeIntervalReductionError));
});
reduceContractStep env state (Let valId val cont) =
let {
evaluatedValue = evalValue env state val;
boundVals = boundValues state;
newState =
boundValues_update (\ _ -> insert valId evaluatedValue boundVals)
state;
warn = (case lookup valId boundVals of {
Nothing -> ReduceNoWarning;
Just oldVal -> ReduceShadowing valId oldVal evaluatedValue;
});
} in Reduced warn ReduceNoPayment newState cont;
reduceContractStep env state (Assert obs cont) =
let {
warning =
(if evalObservation env state obs then ReduceNoWarning
else ReduceAssertionFailed);
} in Reduced warning ReduceNoPayment state cont;
2.2.7 Apply Input
The applyInput function attempts to apply the next input to each Case in
the When, in sequence.
applyInput ::
Environment_ext () -> State_ext () -> Input -> Contract -> ApplyResult;
applyInput env state input (When cases t cont) =
applyCases env state input cases;
applyInput env state input Close = ApplyNoMatchError;
applyInput env state input (Pay v va vb vc vd) = ApplyNoMatchError;
applyInput env state input (If v va vb) = ApplyNoMatchError;
applyInput env state input (Let v va vb) = ApplyNoMatchError;
applyInput env state input (Assert v va) = ApplyNoMatchError;
20
+
2.2.8 Apply Cases
The applyCases function attempts to match an Input to an Action, compute
the new contract state, emit warnings, throw errors if needed, and determine
the appropriate continuation of the contract.
applyCases ::
Environment_ext () -> State_ext () -> Input -> [Case] -> ApplyResult;
applyCases env state (IDeposit accId1 party1 tok1 amount)
(Case (Deposit accId2 party2 tok2 val) cont : rest) =
(if equal_Party accId1 accId2 &&
equal_Party party1 party2 &&
equal_Token tok1 tok2 && equal_int amount (evalValue env state
val)
then let {
warning =
(if less_int Zero_int amount then ApplyNoWarning
else ApplyNonPositiveDeposit party1 accId2 tok2 amount);
newState =
accounts_update
(\ _ -> addMoneyToAccount accId1 tok1 amount (accounts
state))
state;
} in Applied warning newState cont
else applyCases env state (IDeposit accId1 party1 tok1 amount) rest);
applyCases env state (IChoice choId1 choice)
(Case (Choice choId2 bounds) cont : rest) =
(if equal_ChoiceId choId1 choId2 && inBounds choice bounds
then let {
newState =
choices_update (\ _ -> insert choId1 choice (choices state))
state;
} in Applied ApplyNoWarning newState cont
else applyCases env state (IChoice choId1 choice) rest);
applyCases env state INotify (Case (Notify obs) cont : rest) =
(if evalObservation env state obs then Applied ApplyNoWarning state
cont
else applyCases env state INotify rest);
applyCases env state (IDeposit accId1 party1 tok1 amount)
(Case (Choice vb vc) va : rest) =
applyCases env state (IDeposit accId1 party1 tok1 amount) rest;
applyCases env state (IDeposit accId1 party1 tok1 amount)
(Case (Notify vb) va : rest) =
21
+
applyCases env state (IDeposit accId1 party1 tok1 amount) rest;
applyCases env state (IChoice choId1 choice)
(Case (Deposit vb vc vd ve) va : rest) =
applyCases env state (IChoice choId1 choice) rest;
applyCases env state (IChoice choId1 choice) (Case (Notify vb) va : rest)
=
applyCases env state (IChoice choId1 choice) rest;
applyCases env state INotify (Case (Deposit vb vc vd ve) va : rest) =
applyCases env state INotify rest;
applyCases env state INotify (Case (Choice vb vc) va : rest) =
applyCases env state INotify rest;
applyCases env state acc [] = ApplyNoMatchError;
2.2.9 Utilities
The moneyInAccount,updateMoneyInAccount, and addMoneyToAccount func-
tions read, write, and increment the funds in a particular account of the State,
respectively. The giveMoney function transfer funds internally between ac-
counts. The refundOne function finds the first account with funds in it.
moneyInAccount :: Party -> Token -> [((Party, Token), Int)] -> Int;
moneyInAccount accId token accountsV =
findWithDefault Zero_int (accId, token) accountsV;
updateMoneyInAccount ::
Party -> Token -> Int -> [((Party, Token), Int)] -> [((Party, Token),
Int)];
updateMoneyInAccount accId token money accountsV =
(if less_eq_int money Zero_int then delete (accId, token) accountsV
else insert (accId, token) money accountsV);
addMoneyToAccount ::
Party -> Token -> Int -> [((Party, Token), Int)] -> [((Party, Token),
Int)];
addMoneyToAccount accId token money accountsV =
let {
balance = moneyInAccount accId token accountsV;
newBalance = plus_int balance money;
} in (if less_eq_int money Zero_int then accountsV
else updateMoneyInAccount accId token newBalance accountsV);
22
+
giveMoney ::
Party ->
Payee ->
Token ->
Int ->
[((Party, Token), Int)] -> (ReduceEffect, [((Party, Token),
Int)]);
giveMoney accountId payee token money accountsV =
let {
a = (case payee of {
Account accId -> addMoneyToAccount accId token money accountsV;
Party _ -> accountsV;
});
} in (ReduceWithPayment (Payment accountId payee token money), a);
refundOne ::
[((Party, Token), Int)] ->
Maybe ((Party, (Token, Int)), [((Party, Token), Int)]);
refundOne (((accId, tok), money) : rest) =
(if less_int Zero_int money then Just ((accId, (tok, money)), rest)
else refundOne rest);
refundOne [] = Nothing;
2.2.10 Evaluate Value
Given the Environment and the current State, the evalValue function evalu-
ates a Value into a number
evalValue :: Environment ⇒State ⇒Value ⇒int
Available Money
For the AvailableMoney case, evalValue will give us the amount of Tokens
that a Party has in their internal account.
evalValue env state (AvailableMoney accId token) = findWithDefault 0 (accId,
token) (accounts state)
23
+
Constant
For the Constant case, evalValue will always evaluate to the same value
evalValue env state (Constant integer) = integer
Addition
For the AddValue case, evalValue will evaluate both sides and add them
together.
evalValue env state (AddValue lhs rhs) = evalValue env state lhs +evalValue
env state rhs
Addition is associative and commutative:
evalValue env sta (AddValue x (AddValue y z)) = evalValue env sta (AddValue
(AddValue x y)z)
evalValue env sta (AddValue x y) = evalValue env sta (AddValue y x)
Subtraction
For the SubValue case, evalValue will evaluate both sides and subtract the
second value from the first.
evalValue env state (SubValue lhs rhs) = evalValue env state lhs −evalValue
env state rhs
Negation
For every value xthere is the complement NegValue x so that
evalValue env sta (AddValue x (NegValue x)) = 0
Multiplication
For the MulValue case, evalValue will evaluate both sides and multiply them.
evalValue env state (MulValue lhs rhs) = evalValue env state lhs ∗evalValue
env state rhs
24
+
Division
Division is a special case because we only evaluate to natural numbers:
•If the denominator is 0, the result is also 0. Other languages uses NaN
or Infinity to represent this case
•The result will be rounded towards zero.
evalValue env state (DivValue lhs rhs) =
(let n=evalValue env state lhs;
d=evalValue env state rhs
in if d=0then 0else n quot d)
TODO: lemmas around division? maybe extend the following to proof eval-
Value and not just div
c6=0=⇒c∗a div (c∗b) = a div b
c6=0=⇒ |c∗a|div |c∗b|=|a|div |b|
COMMENT(BWB): I suggest that the lemmas be (i) exact multiples di-
vide with no remainder, (ii) the remainder equals the excess above an exact
multiple, and (iii) negation commutues with division.
Choice Value
For the ChoiceValue case, evalValue will look in its state if a Party has made
a choice for the ChoiceName. It will default to zero if it doesn’t find it.
evalValue env state (ChoiceValue choId) = findWithDefault 0 choId (choices
state)
Time Interval Start
All transactions are executed in the context of a valid time interval. For the
TimeIntervalStart case, evalValue will return the beginning of that interval.
evalValue env state TimeIntervalStart =fst (timeInterval env)
25
+
Time Interval End
All transactions are executed in the context of a valid time interval. For the
TimeIntervalEnd case, evalValue will return the end of that interval.
evalValue env state TimeIntervalEnd =snd (timeInterval env)
Use Value
For the TimeIntervalEnd case, evalValue will look in its state for a bound
ValueId. It will default to zero if it doesn’t find it.
evalValue env state (UseValue valId) = findWithDefault 0 valId (boundValues
state)
Conditional Value
For the Cond case, evalValue will first call evalObservation on the condition,
and it will evaluate the the true or false value depending on the result.
evalValue env state (Cond cond thn els) = (if evalObservation env state cond
then evalValue env state thn else evalValue env state els)
2.2.11 Evaluate Observation
Given the Environment and the current State, the evalObservation function
evaluates an Observation into a number
evalObservation :: Environment ⇒State ⇒Observation ⇒bool
True and False
The logical constants true and false are trivially evaluated.
evalObservation env state TrueObs =True
evalObservation env state FalseObs =False
Not, And, Or
The standard logical operators ¬,∧, and ∨are evaluated in a straightforward
manner.
26
+
evalObservation env state (NotObs subObs) = (¬evalObservation env state
subObs)
evalObservation env state (AndObs lhs rhs) = (evalObservation env state lhs
∧evalObservation env state rhs)
evalObservation env state (OrObs lhs rhs)=(evalObservation env state lhs
∨evalObservation env state rhs)
Comparison of Values
Five functions are provided for the comparison (equality and ordering of
integer values) have traditional evaluations: =,<,≤,>, and ≥.
evalObservation env state (ValueEQ lhs rhs)=(evalValue env state lhs =
evalValue env state rhs)
evalObservation env state (ValueLT lhs rhs) = (evalValue env state lhs <
evalValue env state rhs)
evalObservation env state (ValueLE lhs rhs)=(evalValue env state lhs ≤
evalValue env state rhs)
evalObservation env state (ValueGT lhs rhs)=(evalValue env state rhs <
evalValue env state lhs)
evalObservation env state (ValueGE lhs rhs)=(evalValue env state rhs ≤
evalValue env state lhs)
Chose Something
The ChoseSometing i term evaluates to true if the a choice iwas previously
made in the history of the contract.
evalObservation env state (ChoseSomething choId) = member choId (choices
state)
27
+
Chapter 3
Marlowe Guarantees
We can also use proof assistants to demonstrate that the Marlowe semantics
presents certain desirable properties, such as that money is preserved and
anything unspent is returned to users by the end of the execution of any
contract.
Auxillary Functions
Many of the proofs in this chapter rely on function playTrace and play-
TraceAux that execute a sequence of transactions using the Marlowe seman-
tics defined in computeTransaction. They also rely on starting from a valid
and positive contract state, validAndPositive-state and a function maxTime-
Contract that extracts the latest timeout from the contract.
playTrace :: int ⇒Contract ⇒Transaction list ⇒TransactionOutput
playTraceAux :: TransactionOutputRecord ⇒Transaction list ⇒Transac-
tionOutput
validAndPositive-state :: State ⇒bool
maxTimeContract :: Contract ⇒int
3.1 Money Preservation
One of the dangers of using smart contracts is that a badly written one can
potentially lock its funds forever. By the end of the contract, all the money
paid to the contract must be distributed back, in some way, to a subset of
the participants of the contract. To ensure this is the case we proved two
properties: “Money Preservation” and “Contracts Always Close”.
28
+
Regarding money preservation, money is not created or destroyed by the
semantics. More specifically, the money that comes in plus the money in the
contract before the transaction must be equal to the money that comes out
plus the contract after the transaction, except in the case of an error.
moneyInTransactions tra =moneyInPlayTraceResult tra (playTrace sl con-
tract tra)
where moneyInTransactions and moneyInPlayTraceResult measure the funds
in the transactions applied to a contract versus the funds in the contract state
and the payments that it has made while executing.
3.2 Contracts Always Close
For every Marlowe Contract there is a time after which an empty transaction
can be issued that will close the contract and refund all the money in its
accounts.
FIXME: This theorem doesn’t actually prove the narrative. Are we missing
a theorem?
[[validAndPositive-state sta;accounts sta 6= [] ∨cont 6=Close]] =⇒ ∃ inp.
isClosedAndEmpty (computeTransaction inp sta cont)
3.3 Positive Accounts
There are some values for State that are allowed by its type but make no
sense, especially in the case of Isabelle semantics where we use lists instead
of maps:
1. The lists represent maps, so they should have no repeated keys.
2. We want two maps that are equal to be represented the same, so we
force keys to be in ascending order.
3. We only want to record those accounts that contain a positive amount.
We call a value for State valid if the first two properties are true. And we
say it has positive accounts if the third property is true.
FIXME: Address the review comment "Is this a note for us or the explanation
to the user of what playTraceAux-preserves-validAndPositive-state proves?".
29
+
[[validAndPositive-state (txOutState txIn); playTraceAux txIn transList =Trans-
actionOutput txOut]] =⇒validAndPositive-state (txOutState txOut)
3.4 Quiescent Result
A contract is quiescent if and only if the root construct is When, or if the
contract is Close and all accounts are empty. If an input State is valid and
accounts are positive, then the output will be quiescent, isQuiescent.
The following always produce quiescent contracts:
•reductionLoop §2.2.5
•reduceContractUntilQuiescent §2.2.4
•applyAllInputs §2.2.3
•computeTransaction §2.2.1
•playTrace §3
playTrace sl cont (h:t) = TransactionOutput traOut =⇒isQuiescent (txOutContract
traOut) (txOutState traOut)
3.5 Reducing a Contract until Quiescence Is
Idempotent
Once a contract is quiescent, further reduction will not change the contract
or state, and it will not produce any payments or warnings.
reduceContractUntilQuiescent env state contract =ContractQuiescent re-
ducedAfter wa pa nsta ncont =⇒reduceContractUntilQuiescent env nsta
ncont =ContractQuiescent False [] [] nsta ncont
3.6 Split Transactions Into Single Input Does
Not Affect the Result
Applying a list of inputs to a contract produces the same result as applying
each input singly.
playTraceAux acc tral =playTraceAux acc (traceListToSingleInput tral)
30
+
3.6.1 Termination Proof
Isabelle automatically proves termination for most function. However, this is
not the case for reductionLoop, but it is manually proved that the reduction
loop monotonically reduces the size of the contract (except for Close, which
reduces the number of accounts), this is sufficient to prove termination.
reduceContractStep env sta c =Reduced twa tef nsta nc =⇒evalBound nsta
nc <evalBound sta c
3.6.2 All Contracts Have a Maximum Time
If one sends an empty transaction with time equal to maxTimeContract, then
the contract will close.
validAndPositive-state sta
minTime sta ≤iniTime maxTimeContract cont ≤iniTime
iniTime ≤endTime accounts sta 6= [] ∨cont 6=Close
isClosedAndEmpty (computeTransaction (|interval = (iniTime,endTime),inputs = []|)sta cont)
3.6.3 Contract Does Not Hold Funds After it Closes
Funds are not held in a contract after it closes.
computeTransaction tra sta Close =TransactionOutput trec =⇒txOutWarn-
ings trec = []
3.6.4 Transaction Bound
There is a maximum number of transaction that can be accepted by a con-
tract.
playTrace sl c l =TransactionOutput txOut =⇒ |l| ≤ maxTransactionsIni-
tialState c
31
+
Appendix A
Contract examples
This appendix includes some example contracts embedded inside isabelle
with their corresponding guarantees:
A.1 Simple Swap
A simple swap contract consists on two parties exchanging some amount of
Tokens atomically. Each participant needs to deposit their tokens into the
contract by a certain depositDeadline. If they do, the contract makes the
swap and pays the participants, if one of the participant fails to make the
deposit, the funds held by the contract can be redeemed by the owner.
A.1.1 Contract definition
To reduce the number of parameters we bundle the information required by
each participant into a record.
record SwapParty =
— A participant of the contract,
party :: Party
— wants to swap an amount of Token
amount :: Value
currency :: Token
— before a deadline
depositDeadline :: Timeout
The following helper function allows participants to deposit their tokens into
the contract.
fun makeDeposit :: SwapParty ⇒Contract ⇒Contract where
32
+
makeDeposit sp continue =
— The contract waits for a deposit
When
[
Case
(Deposit
— into the internal account of the party
(party sp)
— from the party wallet
(party sp)
— Amount of tokens
(currency sp)
(amount sp)
)
— Once the deposit has been made, execute the continuation
continue
]
— If the tokens haven’t been deposited by the deadline, close the contract.
— This will return all current funds to their owners.
(depositDeadline sp)Close
The following helper function makes a Payment from one party to the other
fun makePayment :: SwapParty ⇒SwapParty ⇒Contract ⇒Contract where
makePayment src dest =
— The contract makes a Payment
Pay
— from the party internal account
(party src)
— to the destination wallet
(Party (party dest))
— of the number of tokens from the source
(currency src) (amount src)
The actual swap contract waits for both parties to make their deposits, then
makes the payout and closes.
fun swap :: SwapParty ⇒SwapParty ⇒Contract where
swap p1 p2 =makeDeposit p1
(makeDeposit p2
(makePayment p1 p2
(makePayment p2 p1 Close
)))
33
+
A.1.2 Example execution
Let’s define two participants that want to trade USD and ADA in the cardano
blockchain.
definition adaProvider =Role (BS 0 0
Ada Provider 0 0
)
definition dollarProvider =Role (BS 0 0
Dollar Provider 00
)
In cardano, the ADA symbol is represented by the empty string
definition adaToken =Token (BS 000 0
) (BS 00 0 0
)
definition dollarToken =Token (BS 00
85bb65 00
) (BS 00
dollar 0 0
)
The contract can be created as follow.
definition
swapExample =
swap
— Party A trades 10 lovelaces
— deposited before Monday, October 3, 2022 4:00:00 PM GMT
(|party =adaProvider
,amount =Constant 10
,currency =adaToken
,depositDeadline =1664812800000
|)
— Party B trades 20 cents
— deposited before Monday, October 3, 2022 5:00:00 PM GMT
(|party =dollarProvider
,amount =Constant 20
,currency =dollarToken
,depositDeadline =1664816400000
|)
Happy path
If both parties deposit before their deadline,
definition
happyPathTransactions =
[
— First party deposit
(|interval = (1664812600000 ,1664812700000 )
,inputs = [
34
+
IDeposit
adaProvider
adaProvider
adaToken
10
]
|)
— Second party deposit
,(|interval = (1664812900000 ,1664813100000 )
,inputs = [
IDeposit
dollarProvider
dollarProvider
dollarToken
20
]
|)
]
payments are made to swap the tokens
definition
happyPathPayments =
[Payment adaProvider (Party dollarProvider)adaToken 10
,Payment dollarProvider (Party adaProvider)dollarToken 20
]
and the contract is closed without emitting a warning
proposition
playTrace 0 swapExample happyPathTransactions =TransactionOutput txOut
=⇒
txOutContract txOut =Close
∧txOutPayments txOut =happyPathPayments
∧txOutWarnings txOut = []
A.1.3 Contract guarantees
Number of transactions
Counting the amount of When’s, it is easy to notice that there can be at
most two transactions
proposition maxTransactionsInitialState (swap a b) = 2
35
+
Expressed in a different way, if we use the lemma defined in §3.6.4 we can state
that, if the execution of the contract yields a succesful TransactionOutput,
then the number of transactions must be lower or equal than 2
lemma
playTrace
initialTime
(swap a b)
transactions =TransactionOutput txOut
=⇒length transactions ≤2
Maximum time
If the deadline of the second party is bigger than the first, then that deadline
is the maximum time of the contract.
proposition
sp1 =
(|party =p1
,amount =a1
,currency =t1
,depositDeadline =d1
|)
=⇒sp2 =
(|party =p2
,amount =a2
,currency =t2
,depositDeadline =d2
|)
=⇒d2 >d1
=⇒d1 >0
=⇒contract =swap sp1 sp2
=⇒maxTimeContract (contract) = d2
36
+
Appendix B
ByteString
Conceptually, a ByteString is defined as a list of 8-bit words.
datatype (plugins del:size)ByteString =ByteString (8 word)list
definition emptyByteString :: ByteString where
emptyByteString =ByteString []
fun singletonByteString :: 8 word ⇒ByteString where
singletonByteString w =ByteString [w]
fun consByteString :: 8 word ⇒ByteString ⇒ByteString where
consByteString w (ByteString t) = ByteString (w#t)
fun appendByteStrings :: ByteString ⇒ByteString ⇒ByteString where
appendByteStrings (ByteString a) (ByteString b) = ByteString (a@b)
fun innerListByteString :: ByteString ⇒8 word list where
innerListByteString (ByteString x) = x
lemma lazyConsByteString :consByteString w t =ByteString (w#innerList-
ByteString t)
by (metis consByteString.simps innerListByteString.elims)
lemma intToWordToUint :x≥0=⇒x<256 =⇒uint (word-of-int x :: 8 word)
= (x:: int)
apply (simp only:uint-word-of-int)
by auto
lemma appendByteStringsAssoc :appendByteStrings (appendByteStrings x y)z
37
+
=appendByteStrings x (appendByteStrings y z)
by (metis append.assoc appendByteStrings.simps innerListByteString.elims)
fun lengthByteString :: ByteString ⇒nat where
lengthByteString (ByteString x) = length x
fun takeByteString :: nat ⇒ByteString ⇒ByteString where
takeByteString n (ByteString x) = ByteString (take n x)
fun dropByteString :: nat ⇒ByteString ⇒ByteString where
dropByteString n (ByteString x) = ByteString (drop n x)
lemma appendTakeDropByteString :appendByteStrings (takeByteString n x) (dropByteString
n x) = x
by (metis appendByteStrings.simps append-take-drop-id dropByteString.simps
innerListByteString.cases takeByteString.simps)
The BS helper allows to create a ByteString out of a regular string.
fun BS :: string ⇒ByteString where
BS str =ByteString (map of-char str)
For example BS 0 0
abc 0 0 is evaluated to ByteString [97 ,98 ,99 ]
Size
instantiation ByteString :: size
begin
definition size-ByteString where
size-ByteString-overloaded-def :size-ByteString =lengthByteString
instance ..
end
B.1 Ordering
We define the (<)and (≤)functions that provide ordering.
instantiation ByteString :: ord
begin
fun less-eq-BS 0:: (8 word)list ⇒(8 word)list ⇒bool where
less-eq-BS 0Nil Nil =True |
38
+
less-eq-BS 0(Cons - -)Nil =False |
less-eq-BS 0Nil (Cons - -) = True |
less-eq-BS 0(Cons h1 t1 ) (Cons h2 t2 ) =
(if h2 <h1 then False
else (if h1 =h2 then less-eq-BS 0t1 t2 else True))
fun less-eq-BS :: ByteString ⇒ByteString ⇒bool where
less-eq-BS (ByteString xs) (ByteString ys) = less-eq-BS 0xs ys
definition a≤b=less-eq-BS a b
fun less-BS :: ByteString ⇒ByteString ⇒bool where
less-BS a b = (¬(less-eq-BS b a))
definition a<b=less-BS a b
end
And we also define some lemmas useful for total order.
lemma oneLessEqBS 0:¬less-eq-BS 0bs2 bs1 =⇒less-eq-BS 0bs1 bs2
lemma oneLessEqBS :¬less-eq-BS bs2 bs1 =⇒less-eq-BS bs1 bs2
lemma less-eq-BS-trans 0:less-eq-BS 0x y =⇒less-eq-BS 0y z =⇒less-eq-BS 0x z
lemma less-eq-BS-trans :less-eq-BS x y =⇒less-eq-BS y z =⇒less-eq-BS x z
lemma byteStringLessEqTwiceEq 0:less-eq-BS 0x y =⇒less-eq-BS 0y x =⇒x=
y
lemma byteStringLessEqTwiceEq :less-eq-BS x y =⇒less-eq-BS y x =⇒x=y
lemma lineaBS :less-eq-BS x y ∨less-eq-BS y x
39
+
Appendix C
Code exports
This theory contains the necessary code to export a version of the Marlowe
Semantics in Haskell.
We start by importing the theories we want to export and a translation the-
ory. The theory Code-Target-Numeral translates the default representation
of numbers (which is suitable for logic reasoning) into a more performant
representation.
theory CodeExports
imports
Core.Semantics
Examples.Swap
HOL−Library.Code-Target-Numeral
HOL.String
begin
We provide some Serialization options to use Haskell native String instead
of our logical represenation of ByteString
code-printing
— The first command tells the serializer to use Haskell
— native String instead of our logical ByteString
type-constructor ByteString
*(Haskell)String
— The next three commands tells the serializer to use the operators provided by
— the Ord instance instead of the ones that work with the logical representation
|constant less-eq-BS
*(Haskell)infix 4<=
|constant less-BS
40
+
*(Haskell)infix 4<
|constant HOL.equal :: ByteString ⇒ByteString ⇒bool
*(Haskell)infix 4==
— The next command tells the serializer to implode the logical Isabelle string
— into Haskell string. Because this is a textual rewrite, we need to force the
— generation of String.implode
|constant BS :: string ⇒ByteString
*(Haskell)Stringa.implode
With a code_identifier we hint what the name of the module should be.
code-identifier
code-module Swap *(Haskell)Examples.Swap
We export all the constants in one statement, because they don’t add up, if
you export two times, the second export will overwrite the first one.
export-code
— With the following exports, we declare that we want to have all the important
semantic functions. Ideally, just with this we would have everything we need, but
we need to force some exports.
evalValue
evalObservation
reductionLoop
reduceContractUntilQuiescent
applyAllInputs
playTrace
computeTransaction
— Export examples to be used as oracle specificaiton tests
swapExample
happyPathTransactions
happyPathPayments
— Force the export of string implode (works together with the BS code_printing
hint)
String.implode
— Force export of State record selectors
txOutContract
txOutWarnings
txOutPayments
txOutState
— Force export of Arith.Int constructor
41
+
int-of-integer
— Force export of TransactionOutput constructors
TransactionOutput
— Force export of TransactionWarning constructors
TransactionNonPositiveDeposit
— Force export of TransactionError constructors
TEAmbiguousTimeIntervalError
— Force export of Payment constructor
Payment
— Force the export of the transaction record
Transaction-ext
— Force the export of the transaction output record
TransactionOutputRecord-ext
— Force the export on some equality functions (sadly it does not force the Eq
instance)
equal-TransactionWarning-inst.equal-TransactionWarning
equal-Payment-inst.equal-Payment
equal-Value-inst.equal-Value
equal-Observation-inst.equal-Observation
equal-Action-inst.equal-Action
equal-Input-inst.equal-Input
equal-Transaction-ext-inst.equal-Transaction-ext
equal-State-ext-inst.equal-State-ext
equal-IntervalError-inst.equal-IntervalError
equal-TransactionError-inst.equal-TransactionError
equal-TransactionOutput-inst.equal-TransactionOutput
in Haskell (string-classes)
42
+
Appendix D
Marlowe Core JSON
The Json specification for Marlowe Core is defined in Literate Haskell us-
ing the Aeson library. In order to fully understand the specification, some
knowledge of Haskell and the library is recommended but not necessary.
For each Marlowe datatype we define a way to parse the JSON into a value
(FromJSON instances) and a way to serialize a value to JSON (ToJSON
instances).
D.1 Party
Parties are serialized as a simple object with an address or role_token key,
depending on the Party type.
instance ToJSON Party where
toJSON (Address address) =
object ["address" .=address ]
toJSON (Role name) =
object ["role_token" .=name ]
instance FromJSON Party where
parseJSON =withObject "Party" $
λv→asAddress v <|>asRole v
where
asAddress v =Address <$>v.:"address"
asRole v =Role <$>v.:"role_token"
for example, the following Party
addressExample :: Party
addressExample =Address "example address"
43
+
is serialized as {"address" :"example address"}, and
roleExample :: Party
roleExample =Role "example role"
is serialized as {"role_token" :"example role"}
D.2 Token
The Token type is serialized as an object with two properties, currency_sym-
bol and token_name
instance ToJSON Token where
toJSON (Token currSym tokName) = object
["currency_symbol" .=currSym
,"token_name" .=tokName
]
instance FromJSON Token where
parseJSON =withObject "Token"
(λv→
Token <$>(v.:"currency_symbol")
<∗>(v.:"token_name")
)
for example, the following Token
dolarToken :: Token
dolarToken =Token "85bb65" "dolar"
is serialized as {"currency_symbol" :"85bb65","token_name" :"dolar"}
D.3 Payee
Payees are serialized as a simple object with an account or party key, de-
pending on the Payee type.
instance ToJSON Payee where
toJSON (Account account) =
object ["account" .=account ]
toJSON (Party party) =
44
+
object ["party" .=party ]
instance FromJSON Payee where
parseJSON =withObject "Payee" $
λv→asAccount v <|>asParty v
where
asAccount v =Account <$>v.:"account"
asParty v =Party <$>v.:"party"
for example, the following Payee
internalPayeeExample :: Payee
internalPayeeExample =Account addressExample
is serialized as {"account" :{"address" :"example address"}}, and
externalPayeeExample :: Payee
externalPayeeExample =Party roleExample
is serialized as {"party" :{"role_token" :"example role"}}
D.4 ChoicesId
The ChoiceId type is serialized as an object with two properties, choice_name
and choice_owner
instance ToJSON ChoiceId where
toJSON (ChoiceId name party) = object
["choice_name" .=name
,"choice_owner" .=party
]
instance FromJSON ChoiceId where
parseJSON =withObject "ChoiceId"
(λv→
ChoiceId <$>(v.:"choice_name")
<∗>(v.:"choice_owner")
)
for example, the following ChoiceId
choiceIdExample :: ChoiceId
choiceIdExample =ChoiceId "ada price" addressExample
is serialized as
45
+
{
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
}
D.5 Bound
The Bound type is serialized as an object with two properties, from and to
instance ToJSON Bound where
toJSON (Bound from to) = object
["from" .=from
,"to" .=to
]
instance FromJSON Bound where
parseJSON =withObject "Bound" (λv→
Bound <$>(getInteger "lower bound" =<< (v.:"from"))
<∗>(getInteger "higher bound" =<< (v.:"to"))
)
for example, the following Bound
exampleBound :: Bound
exampleBound =Bound 2 10
is serialized as {"from" : 2,"to" : 10}
D.6 Values
The ValueId type is serialized as a literal string.
instance ToJSON ValueId where
toJSON (ValueId x ) = toJSON x
instance FromJSON ValueId where
parseJSON =withText "ValueId" $return ◦ValueId ◦T.unpack
The Value serialization depends on the constructor. A Constant is serialized
as a number,TimeIntervalStart and TimeIntervalEnd are serialized as literal
46
+
strings, and the rest are serialized as a single object (with keys depending on
the constructor).
instance ToJSON Value where
toJSON (AvailableMoney accountId token) = object
["amount_of_token" .=token
,"in_account" .=accountId
]
toJSON (Constant (Int_of _integer x )) = toJSON x
toJSON (NegValue x ) = object
["negate" .=x]
toJSON (AddValue lhs rhs) = object
["add" .=lhs
,"and" .=rhs
]
toJSON (SubValue lhs rhs) = object
["value" .=lhs
,"minus" .=rhs
]
toJSON (MulValue lhs rhs) = object
["multiply" .=lhs
,"times" .=rhs
]
toJSON (DivValue lhs rhs) = object
["divide" .=lhs
,"by" .=rhs
]
toJSON (ChoiceValue choiceId ) = object
["value_of_choice" .=choiceId ]
toJSON TimeIntervalStart =JSON .String $T.pack "time_interval_start"
toJSON TimeIntervalEnd =JSON .String $T.pack "time_interval_end"
toJSON (UseValue valueId) = object
["use_value" .=valueId ]
toJSON (Cond obs tv ev ) = object
["if" .=obs
,"then" .=tv
,"else" .=ev
]
instance FromJSON Value where
parseJSON (JSON .Object v) =
(AvailableMoney <$>(v.:"in_account")
47
+
<∗>(v.:"amount_of_token"))
<|>(NegValue <$>(v.:"negate"))
<|>(AddValue <$>(v.:"add")
<∗>(v.:"and"))
<|>(SubValue <$>(v.:"value")
<∗>(v.:"minus"))
<|>(MulValue <$>(v.:"multiply")
<∗>(v.:"times"))
<|>(DivValue <$>(v.:"divide")<∗>(v.:"by"))
<|>(ChoiceValue <$>(v.:"value_of_choice"))
<|>(UseValue <$>(v.:"use_value"))
<|>(Cond <$>(v.:"if")
<∗>(v.:"then")
<∗>(v.:"else"))
parseJSON (JSON .String "time_interval_start") = return TimeIntervalStart
parseJSON (JSON .String "time_interval_end") = return TimeIntervalEnd
parseJSON (JSON .Number n) = Constant <$>getInteger "constant value" n
parseJSON =fail "Value must be either a string, object or an integer"
Some examples for each Values type
Constant
constantExample :: Value
constantExample =Constant 1
is serialized as 1
TimeIntervalStart
intervalStartExample :: Value
intervalStartExample =TimeIntervalStart
is serialized as "time_interval_start"
TimeIntervalEnd
intervalEndExample :: Value
intervalEndExample =TimeIntervalEnd
is serialized as "time_interval_end"
48
+
AddValue
addExample :: Value
addExample =AddValue (Constant 1) (Constant 2)
is serialized as {"add" : 1,"and" : 2}
SubValue
subExample :: Value
subExample =SubValue (Constant 4) (Constant 2)
is serialized as {"minus" : 2,"value" : 4}
MulValue
mulExample :: Value
mulExample =MulValue (Constant 3) (Constant 6)
is serialized as {"multiply" : 3,"times" : 6}
DivValue
divExample :: Value
divExample =DivValue (Constant 8) (Constant 4)
is serialized as {"by" : 4,"divide" : 8}
NegValue
negateExample :: Value
negateExample =NegValue (Constant 3)
is serialized as {"negate" : 3}
49
+
ChoiceValue
choiceValueExample :: Value
choiceValueExample =ChoiceValue choiceIdExample
is serialized as
{
"value_of_choice": {
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
}
}
UseValue
useValueExample :: Value
useValueExample =UseValue (ValueId "variable name")
is serialized as {"use_value" :"variable name"}
Cond
condExample :: Value
condExample =Cond TrueObs addExample mulExample
is serialized as
{
"else": {
"multiply": 3,
"times": 6
},
"if": true,
"then": {
"add": 1,
"and": 2
}
}
50
+
AvailableMoney
availableMoneyExample :: Value
availableMoneyExample =AvailableMoney addressExample dolarToken
is serialized as
{
"amount_of_token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
},
"in_account": {
"address": "example address"
}
}
D.7 Observation
The Observation type is serialized as native boolean (for TrueObs and FalseObs)
or as an object with different properties, depending on the constructor.
instance ToJSON Observation where
toJSON (AndObs lhs rhs) = object
["both" .=lhs
,"and" .=rhs
]
toJSON (OrObs lhs rhs) = object
["either" .=lhs
,"or" .=rhs
]
toJSON (NotObs v) = object
["not" .=v]
toJSON (ChoseSomething choiceId ) = object
["chose_something_for" .=choiceId ]
toJSON (ValueGE lhs rhs) = object
["value" .=lhs
,"ge_than" .=rhs
]
toJSON (ValueGT lhs rhs) = object
51
+
["value" .=lhs
,"gt" .=rhs
]
toJSON (ValueLT lhs rhs) = object
["value" .=lhs
,"lt" .=rhs
]
toJSON (ValueLE lhs rhs) = object
["value" .=lhs
,"le_than" .=rhs
]
toJSON (ValueEQ lhs rhs) = object
["value" .=lhs
,"equal_to" .=rhs
]
toJSON TrueObs =toJSON True
toJSON FalseObs =toJSON False
instance FromJSON Observation where
parseJSON (JSON .Bool True) = return TrueObs
parseJSON (JSON .Bool False) = return FalseObs
parseJSON (JSON .Object v) =
(AndObs <$>(v.:"both")
<∗>(v.:"and"))
<|>(OrObs <$>(v.:"either")
<∗>(v.:"or"))
<|>(NotObs <$>(v.:"not"))
<|>(ChoseSomething <$>(v.:"chose_something_for"))
<|>(ValueGE <$>(v.:"value")
<∗>(v.:"ge_than"))
<|>(ValueGT <$>(v.:"value")
<∗>(v.:"gt"))
<|>(ValueLT <$>(v.:"value")
<∗>(v.:"lt"))
<|>(ValueLE <$>(v.:"value")
<∗>(v.:"le_than"))
<|>(ValueEQ <$>(v.:"value")
<∗>(v.:"equal_to"))
parseJSON =fail "Observation must be either an object or a boolean"
Some examples for each Observation type
52
+
TrueObs
trueExample :: Observation
trueExample =TrueObs
is serialized as true
FalseObs
falseExample :: Observation
falseExample =FalseObs
is serialized as false
AndObs
andExample :: Observation
andExample =AndObs TrueObs FalseObs
is serialized as {"and" :false,"both" :true }
OrObs
orExample :: Observation
orExample =OrObs TrueObs FalseObs
is serialized as {"either" :true,"or" :false }
NotObs
notExample :: Observation
notExample =NotObs TrueObs
is serialized as {"not" :true }
53
+
ChoseSomething
choseExample :: Observation
choseExample =ChoseSomething choiceIdExample
is serialized as
{
"chose_something_for": {
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
}
}
ValueGE
valueGEExample :: Observation
valueGEExample =ValueGE (Constant 1) (Constant 2)
is serialized as {"ge_than" : 2,"value" : 1}
ValueGT
valueGTExample :: Observation
valueGTExample =ValueGT (Constant 1) (Constant 2)
is serialized as {"gt" : 2,"value" : 1}
ValueLT
valueLTExample :: Observation
valueLTExample =ValueLT (Constant 1) (Constant 2)
is serialized as {"lt" : 2,"value" : 1}
54
+
ValueLE
valueLEExample :: Observation
valueLEExample =ValueLE (Constant 1) (Constant 2)
is serialized as {"le_than" : 2,"value" : 1}
ValueEQ
valueEQExample :: Observation
valueEQExample =ValueEQ (Constant 1) (Constant 2)
is serialized as {"equal_to" : 2,"value" : 1}
D.8 Action
The Action type is serialized as an object with different properties, depending
the constructor.
instance ToJSON Action where
toJSON (Deposit accountId party token val ) = object
["into_account" .=accountId
,"party" .=party
,"of_token" .=token
,"deposits" .=val
]
toJSON (Choice choiceId bounds) = object
["for_choice" .=choiceId
,"choose_between" .=toJSONList (map toJSON bounds)
]
toJSON (Notify obs) = object
["notify_if" .=obs ]
instance FromJSON Action where
parseJSON =withObject "Action" (λv→
(Deposit <$>(v.:"into_account")
<∗>(v.:"party")
<∗>(v.:"of_token")
<∗>(v.:"deposits"))
<|>(Choice <$>(v.:"for_choice")
55
+
<∗>((v.:"choose_between")>>=
withArray "Bound list" (λbl →
mapM parseJSON (F.toList bl )
)))
<|>(Notify <$>(v.:"notify_if"))
)
Some examples for each Action type
Deposit
depositExample :: Action
depositExample =Deposit
addressExample
roleExample
dolarToken
constantExample
is serialized as
{
"deposits": 1,
"into_account": {
"address": "example address"
},
"of_token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
},
"party": {
"role_token": "example role"
}
}
Choice
choiceExample :: Action
choiceExample =Choice
choiceIdExample
[Bound 0 1,Bound 4 8]
is serialized as
56
+
{
"choose_between": [
{
"from": 0,
"to": 1
},
{
"from": 4,
"to": 8
}
],
"for_choice": {
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
}
}
Notify
notifyExample :: Action
notifyExample =Notify (ChoseSomething choiceIdExample)
is serialized as
{
"notify_if": {
"chose_something_for": {
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
}
}
}
D.9 Case
The Case type is serialized as an object with two properties (case and then).
57
+
instance ToJSON Case where
toJSON (Case act cont) = object
["case" .=act
,"then" .=cont
]
instance FromJSON Case where
parseJSON =withObject "Case"
(λv→
Case <$>(v.:"case")<∗>(v.:"then")
)
For example, the following Case
caseExample :: Case
caseExample =Case notifyExample Close
is serialized as
{
"case": {
"notify_if": {
"chose_something_for": {
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
}
}
},
"then": "close"
}
D.10 Contract
The Contract type is serialized as the literal string "close" or as an object,
depending on the constructor
instance ToJSON Contract where
toJSON Close =JSON .String $T.pack "close"
toJSON (Pay accountId payee token value contract) = object
58
+
["from_account" .=accountId
,"to" .=payee
,"token" .=token
,"pay" .=value
,"then" .=contract
]
toJSON (If obs cont1 cont2 ) = object
["if" .=obs
,"then" .=cont1
,"else" .=cont2
]
toJSON (When caseList timeout cont) = object
["when" .=toJSONList (map toJSON caseList)
,"timeout" .=timeout
,"timeout_continuation" .=cont
]
toJSON (Let valId value cont) = object
["let" .=valId
,"be" .=value
,"then" .=cont
]
toJSON (Assert obs cont) = object
["assert" .=obs
,"then" .=cont
]
instance FromJSON Contract where
parseJSON (JSON .String "close") = return Close
parseJSON (JSON .Object v) =
(Pay <$>(v.:"from_account")
<∗>(v.:"to")
<∗>(v.:"token")
<∗>(v.:"pay")
<∗>(v.:"then"))
<|>(If <$>(v.:"if")
<∗>(v.:"then")
<∗>(v.:"else"))
<|>(When <$>((v.:"when")>>=
withArray "Case list" (λcl →
mapM parseJSON (F.toList cl )
))
59
+
<∗>(withInteger "when timeout" =<< (v.:"timeout"))
<∗>(v.:"timeout_continuation"))
<|>(Let <$>(v.:"let")
<∗>(v.:"be")
<∗>(v.:"then"))
<|>(Assert <$>(v.:"assert")
<∗>(v.:"then"))
parseJSON =
fail "Contract must be either an object or a the string \"close\""
Some examples for each Contract type
Close
closeExample :: Contract
closeExample =Close
is serialized as "close"
Pay
payExample :: Contract
payExample =Pay
roleExample
internalPayeeExample
dolarToken
(Constant 10)
Close
is serialized as
{
"from_account": {
"role_token": "example role"
},
"pay": 10,
"then": "close",
"to": {
"account": {
"address": "example address"
60
+
}
},
"token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
}
}
If
ifExample :: Contract
ifExample =If
TrueObs
Close
Close
is serialized as
{
"else": "close",
"if": true,
"then": "close"
}
When
whenExample :: Contract
whenExample =When
[Case (Notify TrueObs)Close
,Case (Notify FalseObs)Close
]
20
Close
is serialized as
{
"timeout": 20,
"timeout_continuation": "close",
"when": [
61
+
{
"case": {
"notify_if": true
},
"then": "close"
},
{
"case": {
"notify_if": false
},
"then": "close"
}
]
}
Let
letExample :: Contract
letExample =Let (ValueId "var") (Constant 10) Close
is serialized as
{
"be": 10,
"let": "var",
"then": "close"
}
Assert
assertExample :: Contract
assertExample =Assert choseExample Close
is serialized as
{
"assert": {
"chose_something_for": {
"choice_name": "ada price",
"choice_owner": {
62
+
"address": "example address"
}
}
},
"then": "close"
}
D.11 Input
The Input type is serialized as the literal string "input_notify" or as an object,
depending on the constructor.
instance ToJSON Input where
toJSON (IDeposit accId party tok amount) = object
["input_from_party" .=party
,"that_deposits" .=amount
,"of_token" .=tok
,"into_account" .=accId
]
toJSON (IChoice choiceId chosenNum) = object
["input_that_chooses_num" .=chosenNum
,"for_choice_id" .=choiceId
]
toJSON INotify =JSON .String $T.pack "input_notify"
instance FromJSON Input where
parseJSON (JSON .String "input_notify") = return INotify
parseJSON (JSON .Object v) =
IChoice <$>v.:"for_choice_id"
<∗>v.:"input_that_chooses_num"
<|>IDeposit <$>v.:"into_account"
<∗>v.:"input_from_party"
<∗>v.:"of_token"
<∗>v.:"that_deposits"
parseJSON =
fail "Input must be either an object or the string \"input_notify\""
Some examples for each Input type
63
+
INotify
iNotifyExample :: Input
iNotifyExample =INotify
is serialized as "input_notify"
IChoice
iChoiceExample :: Input
iChoiceExample =IChoice choiceIdExample 3
is serialized as
{
"for_choice_id": {
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
},
"input_that_chooses_num": 3
}
IDeposit
iDepositExample :: Input
iDepositExample =IDeposit addressExample roleExample dolarToken 5
is serialized as
{
"input_from_party": {
"role_token": "example role"
},
"into_account": {
"address": "example address"
},
"of_token": {
"currency_symbol": "85bb65",
64
+
"token_name": "dolar"
},
"that_deposits": 5
}
D.12 Transaction
The Transaction type is serialized as an object with two properties, tx_in-
terval and tx_inputs.
instance ToJSON (Transaction_ext a)where
toJSON (Transaction_ext (from,to)txInps ) = object
["tx_interval" .=timeIntervalJSON
,"tx_inputs" .=toJSONList (map toJSON txInps)
]
where timeIntervalJSON =object ["from" .=from
,"to" .=to
]
instance FromJSON (Transaction_ext ()) where
parseJSON (JSON .Object v) =
Transaction_ext <$>(parseTimeInterval =<< (v.:"tx_interval"))
<∗>((v.:"tx_inputs")>>=
withArray "Transaction input list" (λcl →
mapM parseJSON (F.toList cl )
))
<∗>pure ()
where parseTimeInterval =withObject "TimeInterval" (λv→
do from ←withInteger "TimeInterval from" =<< (v.:"from")
to ←withInteger "TimeInterval to" =<< (v.:"to")
return (from,to)
)
parseJSON =fail "Transaction must be an object"
for example, the following Transaction
transactionExample :: Transaction_ext ()
transactionExample =Transaction_ext
(10,100)
[iChoiceExample
,iNotifyExample
65
+
]
()
is serialized as
{
"tx_inputs": [
{
"for_choice_id": {
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
},
"input_that_chooses_num": 3
},
"input_notify"
],
"tx_interval": {
"from": 10,
"to": 100
}
}
D.13 Payment
The Payment type is serialized as a single object with three properties
instance ToJSON Payment where
toJSON (Payment from to token amount) = object
["payment_from" .=from
,"to" .=to
,"token" .=token
,"amount" .=amount
]
instance FromJSON Payment where
parseJSON =withObject "Payment"
(λv→
Payment <$>(v.:"payment_from")
<∗>(v.:"to")
66
+
<∗>(v.:"token")
<∗>(v.:"amount")
)
for example, the following Payment
paymentExample :: Payment
paymentExample =Payment
addressExample
externalPayeeExample
dolarToken
10
is serialized as
{
"amount": 10,
"payment_from": {
"address": "example address"
},
"to": {
"party": {
"role_token": "example role"
}
},
"token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
}
}
D.14 State
The State type is serialized as a single object with four properties. Each Map
is represented by a list of key value tuples.
instance ToJSON (State_ext ()) where
toJSON (State_ext accounts choices boundValues minTime ) = object
["accounts" .=toJSON accounts
,"choices" .=toJSON choices
,"boundValues" .=toJSON boundValues
67
+
,"minTime" .=minTime
]
instance FromJSON (State_ext ()) where
parseJSON =withObject "State"
(λv→
State_ext <$>(v.:"accounts")
<∗>(v.:"choices")
<∗>(v.:"boundValues")
<∗>(v.:"minTime")
<∗>pure ()
)
for example, the following state
stateExample :: State_ext ()
stateExample =State_ext
[((roleExample,dolarToken),20)]
[(choiceIdExample,10)]
[(ValueId "example",30)]
90
()
is serialized as
{
"accounts": [
[
[
{
"role_token": "example role"
},
{
"currency_symbol": "85bb65",
"token_name": "dolar"
}
],
20
]
],
"boundValues": [
[
68
+
"example",
30
]
],
"choices": [
[
{
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
},
10
]
],
"minTime": 90
}
D.15 TransactionWarning
The TransactionWarning type is serialized as a literal string (in case of Trans-
actionAssertionFailed) or as an object with different properties, depending
the constructor.
instance ToJSON TransactionWarning where
toJSON (TransactionNonPositiveDeposit party accId tok amount) = object
["party" .=party
,"asked_to_deposit" .=amount
,"of_token" .=tok
,"in_account" .=accId
]
toJSON (TransactionNonPositivePay accId payee tok amount) = object
["account" .=accId
,"asked_to_pay" .=amount
,"of_token" .=tok
,"to_payee" .=payee
]
toJSON (TransactionPartialPay accId payee tok paid expected) = object
["account" .=accId
,"asked_to_pay" .=expected
69
+
,"of_token" .=tok
,"to_payee" .=payee
,"but_only_paid" .=paid
]
toJSON (TransactionShadowing valId oldVal newVal) = object
["value_id" .=valId
,"had_value" .=oldVal
,"is_now_assigned" .=newVal
]
toJSON TransactionAssertionFailed =JSON .String $T.pack "assertion_failed"
instance FromJSON TransactionWarning where
parseJSON (JSON .String "assertion_failed") =
return TransactionAssertionFailed
parseJSON (JSON .Object v) =
(TransactionNonPositiveDeposit <$>(v.:"party")
<∗>(v.:"in_account")
<∗>(v.:"of_token")
<∗>(v.:"asked_to_deposit"))
<|>(do maybeButOnlyPaid ←v.:? "but_only_paid"
case maybeButOnlyPaid :: Maybe Scientific of
Nothing →TransactionNonPositivePay <$>(v.:"account")
<∗>(v.:"to_payee")
<∗>(v.:"of_token")
<∗>(v.:"asked_to_pay")
Just butOnlyPaid →TransactionPartialPay <$>(v.:"account")
<∗>(v.:"to_payee")
<∗>(v.:"of_token")
<∗>getInteger "but only paid" butOnlyPaid
<∗>(v.:"asked_to_pay"))
<|>(TransactionShadowing <$>(v.:"value_id")
<∗>(v.:"had_value")
<∗>(v.:"is_now_assigned"))
parseJSON =
fail "Contract must be either an object or a the string \"close\""
Some examples for each TransactionWarning type
TransactionNonPositiveDeposit
transactionNonPositiveDepositExample :: TransactionWarning
transactionNonPositiveDepositExample =TransactionNonPositiveDeposit
70
+
addressExample
roleExample
dolarToken
20
is serialized as
{
"asked_to_deposit": 20,
"in_account": {
"role_token": "example role"
},
"of_token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
},
"party": {
"address": "example address"
}
}
TransactionNonPositivePay
transactionNonPositivePayExample :: TransactionWarning
transactionNonPositivePayExample =TransactionNonPositivePay
addressExample
internalPayeeExample
dolarToken
20
is serialized as
{
"account": {
"address": "example address"
},
"asked_to_pay": 20,
"of_token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
},
71
+
"to_payee": {
"account": {
"address": "example address"
}
}
}
TransactionPartialPay
transactionPartialPayExample :: TransactionWarning
transactionPartialPayExample =TransactionPartialPay
addressExample
internalPayeeExample
dolarToken
20
30
is serialized as
{
"account": {
"address": "example address"
},
"asked_to_pay": 30,
"but_only_paid": 20,
"of_token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
},
"to_payee": {
"account": {
"address": "example address"
}
}
}
TransactionShadowing
transactionShadowingExample :: TransactionWarning
transactionShadowingExample =TransactionShadowing
72
+
(ValueId "example")
4
5
is serialized as
{
"had_value": 4,
"is_now_assigned": 5,
"value_id": "example"
}
TransactionAssertionFailed
transactionAssertionFailedExample :: TransactionWarning
transactionAssertionFailedExample =TransactionAssertionFailed
is serialized as "assertion_failed"
D.16 IntervalError
The IntervalError type is serialized as an object with a single property (de-
pending on the constructor) and in a tuple, the values.
instance ToJSON IntervalError where
toJSON (InvalidInterval (s,e)) = object
[("invalidInterval" .=toJSON (s,e))]
toJSON (IntervalInPastError t (s,e)) = object
[("intervalInPastError" .=toJSON (t,s,e))]
instance FromJSON IntervalError where
parseJSON (JSON .Object v) =
let
parseInvalidInterval =do
(s,e)←v.:"invalidInterval"
pure $InvalidInterval (s,e)
parseIntervalInPastError =do
(t,s,e)←v.:"intervalInPastError"
pure $IntervalInPastError t (s,e)
in
parseIntervalInPastError <|>parseInvalidInterval
73
+
parseJSON invalid =
JSON .prependFailure "parsing IntervalError failed, " (JSON .typeMismatch "Object" invalid )
Some examples for each IntervalError type
InvalidInterval
invalidIntervalExample :: IntervalError
invalidIntervalExample =InvalidInterval (10,20)
is serialized as {"invalidInterval" : [10,20]}
IntervalInPastError
intervalInPastErrorExample :: IntervalError
intervalInPastErrorExample =IntervalInPastError 30 (10,20)
is serialized as {"intervalInPastError" : [30,10,20]}
D.17 TransactionError
The TransactionError type is serialized as an object with a tag property that
differentiates the type, and a contents property that includes the parameter
if any.
instance ToJSON TransactionError where
toJSON TEAmbiguousTimeIntervalError =object
["tag" .=JSON .String "TEAmbiguousTimeIntervalError"
,"contents" .=JSON .Null
]
toJSON TEApplyNoMatchError =object
["tag" .=JSON .String "TEApplyNoMatchError"
,"contents" .=JSON .Null
]
toJSON (TEIntervalError e) = object
["tag" .=JSON .String "TEIntervalError"
,"contents" .=toJSON e
]
toJSON TEUselessTransaction =object
74
+
["tag" .=JSON .String "TEUselessTransaction"
,"contents" .=JSON .Null
]
instance FromJSON TransactionError where
parseJSON =withObject "TransactionError"
(λv→
do
tag :: String ←v.:"tag"
case tag of
"TEAmbiguousTimeIntervalError" →
pure TEAmbiguousTimeIntervalError
"TEApplyNoMatchError" →
pure TEApplyNoMatchError
"TEIntervalError" →
TEIntervalError <$>v.:"contents"
"TEUselessTransaction" →
pure TEUselessTransaction
)
Some examples for each TransactionError type
TEAmbiguousTimeIntervalError
teAmbiguousTimeIntervalErrorExample :: TransactionError
teAmbiguousTimeIntervalErrorExample =TEAmbiguousTimeIntervalError
is serialized as
{
"contents": null,
"tag": "TEAmbiguousTimeIntervalError"
}
TEApplyNoMatchError
teApplyNoMatchErrorExample :: TransactionError
teApplyNoMatchErrorExample =TEApplyNoMatchError
is serialized as
75
+
{
"contents": null,
"tag": "TEApplyNoMatchError"
}
TEIntervalError
teIntervalErrorExample :: TransactionError
teIntervalErrorExample =TEIntervalError intervalInPastErrorExample
is serialized as
{
"contents": {
"intervalInPastError": [
30,
10,
20
]
},
"tag": "TEIntervalError"
}
TEUselessTransaction
teUselessTransactionExample :: TransactionError
teUselessTransactionExample =TEUselessTransaction
is serialized as
{
"contents": null,
"tag": "TEUselessTransaction"
}
D.18 TransactionOutput
The TransactionOutput is serialized as a single object with one property
(transaction_error) in case of an error, or 4 properties in case of success.
76
+
instance ToJSON TransactionOutput where
toJSON (TransactionError err ) = object
["transaction_error" .=toJSON err ]
toJSON (TransactionOutput out)
=object
["warnings" .=toJSON (txOutWarnings out)
,"payments" .=toJSON (txOutPayments out)
,"state" .=toJSON (txOutState out)
,"contract" .=toJSON (txOutContract out)
]
instance FromJSON TransactionOutput where
parseJSON =withObject "TransactionOutput"
(λv→
(TransactionError <$>(v.:"transaction_error"))
<|>(TransactionOutput <$>
(TransactionOutputRecord_ext
<$>(v.:"warnings")
<∗>(v.:"payments")
<∗>(v.:"state")
<∗>(v.:"contract")
<∗>pure ()
)
)
)
Some examples for each TransactionOutput type
TransactionError
transactionOutputErrorExample :: TransactionOutput
transactionOutputErrorExample =TransactionError teUselessTransactionExample
is serialized as
{
"transaction_error": {
"contents": null,
"tag": "TEUselessTransaction"
}
}
77
+
TransactionOutput
transactionOutputSuccessExample :: TransactionOutput
transactionOutputSuccessExample =playTrace
0
Examples.Swap.swapExample
Examples.Swap.happyPathTransactions
is serialized as
{
"contract": "close",
"payments": [
{
"amount": 10,
"payment_from": {
"role_token": "Ada Provider"
},
"to": {
"party": {
"role_token": "Dollar Provider"
}
},
"token": {
"currency_symbol": "",
"token_name": ""
}
},
{
"amount": 20,
"payment_from": {
"role_token": "Dollar Provider"
},
"to": {
"party": {
"role_token": "Ada Provider"
}
},
"token": {
"currency_symbol": "85bb65",
"token_name": "dollar"
78
+
}
}
],
"state": {
"accounts": [],
"boundValues": [],
"choices": [],
"minTime": 1664812900000
},
"warnings": []
}
D.19 Full Contract Example
The Swap Example, defined in section §A.1.2 is serialized as
{
"timeout": 1664812800000,
"timeout_continuation": "close",
"when": [
{
"case": {
"deposits": 10,
"into_account": {
"role_token": "Ada Provider"
},
"of_token": {
"currency_symbol": "",
"token_name": ""
},
"party": {
"role_token": "Ada Provider"
}
},
"then": {
"timeout": 1664816400000,
"timeout_continuation": "close",
"when": [
{
"case": {
79
+
"deposits": 20,
"into_account": {
"role_token": "Dollar Provider"
},
"of_token": {
"currency_symbol": "85bb65",
"token_name": "dollar"
},
"party": {
"role_token": "Dollar Provider"
}
},
"then": {
"from_account": {
"role_token": "Ada Provider"
},
"pay": 10,
"then": {
"from_account": {
"role_token": "Dollar Provider"
},
"pay": 20,
"then": "close",
"to": {
"party": {
"role_token": "Ada Provider"
}
},
"token": {
"currency_symbol": "85bb65",
"token_name": "dollar"
}
},
"to": {
"party": {
"role_token": "Dollar Provider"
}
},
"token": {
"currency_symbol": "",
"token_name": ""
80
+
}
}
}
]
}
}
]
}
D.20 Parse utils
These are some Aeson utils to help parse a number to the Isabelle exported
Arithİnt
getInteger :: String →Scientific →Parser Arith.Int
getInteger ctx x =case (floatingOrInteger x :: Either Double Integer )of
Right a →return $Int_of _integer a
Left →fail $"parsing " ++ ctx ++ " failed, expected integer, but encountered floating point"
withInteger :: String →JSON .Value →Parser Arith.Int
withInteger ctx =withScientific ctx $getInteger ctx
instance ToJSON Arith.Int where
toJSON (Int_of _integer x ) = toJSON x
instance FromJSON Arith.Int where
parseJSON (JSON .Number x ) = getInteger "Int" x
parseJSON =fail "expecting integer"
81
+
+
+ +
+ + diff --git a/specification-v3.pdf b/specification-v3.pdf new file mode 100644 index 0000000..c5f38d3 Binary files /dev/null and b/specification-v3.pdf differ