- 1 Marlowe
- 1.1 Introduction
- 1.2 The Marlowe Model.
- 1.2.1 Data types.
- 1.2.2 Quiescent
- 1.2.3 Participants, accounts and state
- 1.2.4 Core and Extended
- 1.3 Specification generation and nomenclature
- 1.4 Blockchain agnostic
- 2 Marlowe Core
- 2.1 Types
- 2.1.1 Participants, roles and addresses
- 2.1.2 Multi-Asset token.
- 2.1.3 Accounts
- 2.1.4 Choices
- 2.1.5 Values and Observations
- 2.1.6 Actions and inputs
- 2.1.7 Contracts
- 2.1.8 State and Environment
- 2.2 Semantics
- 2.2.1 Compute Transaction.
- 2.2.2 Fix Interval
- 2.2.3 Apply All Inputs
- 2.2.4 Reduce Contract Until Quiescent
- 2.2.5 Reduction Loop
- 2.2.6 Reduce Contract Step
- 2.2.7 Apply Input
- 2.2.8 Apply Cases
- 2.2.9 Utilities
- 2.2.10 Evaluate Value
- 2.2.11 Evaluate Observation.
- 2.1 Types
- 3 Marlowe Guarantees
- 3.1 Money Preservation.
- 3.2 Contracts Always Close.
- 3.3 Positive Accounts
- 3.4 Quiescent Result
- 3.5 Reducing a Contract until Quiescence Is Idempotent
- 3.6 Split Transactions Into Single Input Does Not Affect the Result
- 3.6.1 Termination Proof
- 3.6.2 All Contracts Have a Maximum Time.
- 3.6.3 Contract Does Not Hold Funds After it Closes
- 3.6.4 Transaction Bound
- A Contract examples
- A.1 Simple Swap.
- A.1.1 Contract definition
- A.1.2 Example execution
- A.1.3 Contract guarantees
- A.1 Simple Swap.
- B ByteString
- B.1 Ordering
- C Code exports
- D Marlowe Core JSON
- D.1 Party.
- D.2 Token
- D.3 Payee
- D.4 ChoicesId
- D.5 Bound
- D.6 Values
- D.7 Observation
- D.8 Action
- D.9 Case
- D.10 Contract
- D.11 Input.
- D.12 Transaction
- D.13 Payment
- D.14 State
- D.15 TransactionWarning.
- D.16 IntervalError
- D.17 TransactionError
- D.18 TransactionOutput
- D.19 Full Contract Example
- D.20 Parse utils
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 §1 provides an overview of the Marlowe language. Chapter §2 defines the Core language and semantics in detail. Chapter §3 presents proofs that (^1) https://www.lexifi.com/
guarantee that Marlowe contracts possess properties desirable for financial agreements.
Marlowe Contract s 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 v number of tokens t to the party p from the account a , and then follow the contract c ”. We call c the continuation of the contract. All paths of the contract are made explicit this way, and each Contract term is executed at most once.
The Value s and Observation s § 2.1.5only 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 Timeout s and they are absolute, but it is likely we’ll add relative times in a future version.
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.
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.
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.8are global to that contract.
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 Value s and Timeout s. For the moment, the extended language is not formalized in this specification but it will be added in the future
The Marlowe specification is formalized using the proof assistant Isabelle^2. 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.
Marlowe is currently implemented on the Cardano Blockchain, but it is de- signed to be Blockchain agnostic.
(^2) https://isabelle.in.tum.de/
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 Token s 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.1and 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 Timeout s that prevent us from waiting forever for external Input s 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
(^3) January 1st, 1970 at 00:00:00 UTC
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 a Contract definition §2.1.7.
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).
A Role , 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 tokens^1 that can be
(^1) In the Cardano implementation roles are represented by native tokens and they are
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.
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.
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
A Pay 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
(^2) https://docs.cardano.org/native-tokens/learn
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 Bound ed. As an argument for the Choice action §2.1.6, we pass a list of Bound s 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
We can store a Value in the Marlowe State §2.1.8using the Let construct §2.1.7, and we use a ValueId to referrence it
datatype ValueId = ValueId ByteString
Value s and Observation s 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.10and evalObservation §2.2.11respectively.
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
| 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 t in 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 x if b is true and to y otherwise.
The last Value s, 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 ∨ y are 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 = y are represented by ValueLT x y , ValueLE x y , ValueGT x y , ValueGE x y , and ValueEQ x y.
Action s and Input s are closely related. An Action can be added in a list of Case s § 2.1.7as a way to declare the possible external Input s 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
A Deposit a p t v makes a deposit of # v Token s t from Party p into account a.
A choice Choice i bs is made for a particular choice identified by the ChoiceId §2.1.4 i with 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 a Transaction
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 Bound s 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
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
| 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 Payment s § ?? for the assets in the internal accounts to their default owners^3.
The contract Pay a p t v c , generates a Payment from the internal account a to a payee §2.1.3 p of # v Token s and then continues to contract c. Warnings will be generated if the value v is 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 x if the Observation obs evaluates to true , or to branch y otherwise.
When is the most complex constructor for contracts, with the form When cs t c. The list cs contains zero or more pairs of Action s 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 a TimeInterval with a start time bigger than the Timeout t , the contingency continuation c is evaluated. The explicit timeout mechanism is what allows Marlowe to avoid waiting forever for external inputs.
A Let contract Let i v c allows a contract to record a value using an identifier i. In this case, the expression v is 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 b evaluates 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.
(^3) Even if the payments are generated one at a time (per account and per Token), the cardano implementation generates a single transaction
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
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.
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 ->
TransactionError TEAmbiguousTimeIntervalError;
});
IntervalError errora -> TransactionError (TEIntervalError errora);
});
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));
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 [] [];
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; });
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 [] [];
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; });
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.
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 {
(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;
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;
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) =
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;
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);
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;
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 Token s that a Party has in their internal account.
evalValue env state ( AvailableMoney accId token ) = findWithDefault 0 ( accId , token ) ( accounts state )
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 x there 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
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 )= ( letn = evalValue env state lhs ; d = evalValue env state rhs in ifd = 0 then 0 elsen quot d )
TODO: lemmas around division? maybe extend the following to proof eval- Value and not just div
c 6 = 0 =⇒ c ∗ a div ( c ∗ b ) = a div b
c 6 = 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 )
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 ) = ( ifevalObservation env state cond thenevalValue env state thnelseevalValue env state els )
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.
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 i was previously made in the history of the contract.
evalObservation env state ( ChoseSomething choId ) = member choId ( choices state )
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
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”.
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.
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 )
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:
- The lists represent maps, so they should have no repeated keys.
- We want two maps that are equal to be represented the same, so we force keys to be in ascending order.
- 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?".
[[ validAndPositive-state ( txOutState txIn ); playTraceAux txIn transList = Trans- actionOutput txOut ]] =⇒ validAndPositive-state ( txOutState txOut )
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 )
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
Applying a list of inputs to a contract produces the same result as applying each input singly.
playTraceAux acc tral = playTraceAux acc ( traceListToSingleInput tral )
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
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 )
Funds are not held in a contract after it closes.
computeTransaction tra sta Close = TransactionOutput trec =⇒ txOutWarn- ings trec = []
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
This appendix includes some example contracts embedded inside isabelle with their corresponding guarantees:
A simple swap contract consists on two parties exchanging some amount of Token s 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.
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
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 )))
Let’s define two participants that want to trade USD and ADA in the cardano blockchain.
definition adaProvider = Role ( BS ′′ Ada Provider ′′) definition dollarProvider = Role ( BS ′′ Dollar Provider ′′)
In cardano, the ADA symbol is represented by the empty string
definition adaToken = Token ( BS ′′′′)( BS ′′′′) definition dollarToken = Token ( BS ′′ 85bb65 ′′)( BS ′′ dollar ′′)
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 =[
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 =[]
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
Expressed in a different way, if we use the lemma defined in §3.6.4we 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
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
= 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 ′′ abc ′′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
We define the(<)and(≤)functions that provide ord ering.
instantiation ByteString :: ord begin
fun less-eq-BS ′::( 8 word ) list ⇒( 8 word ) list ⇒ bool where less-eq-BS ′ Nil Nil = True |
less-eq-BS ′( Cons - - ) Nil = False | less-eq-BS ′ Nil ( Cons - - )= True | less-eq-BS ′( Cons h1 t1 )( Cons h2 t2 )= ( if h2 < h1 then False else ( if h1 = h2 then less-eq-BS ′ t1 t2 else True ))
fun less-eq-BS :: ByteString ⇒ ByteString ⇒ bool where less-eq-BS ( ByteString xs )( ByteString ys )= less-eq-BS ′ xs 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 ′:¬ less-eq-BS ′ bs2 bs1 =⇒ less-eq-BS ′ bs1 bs2 lemma oneLessEqBS :¬ less-eq-BS bs2 bs1 =⇒ less-eq-BS bs1 bs2 lemma less-eq-BS-trans ′: less-eq-BS ′ x y =⇒ less-eq-BS ′ y z =⇒ less-eq-BS ′ x z lemma less-eq-BS-trans : less-eq-BS x y =⇒ less-eq-BS y z =⇒ less-eq-BS x z lemma byteStringLessEqTwiceEq ′: less-eq-BS ′ x y =⇒ less-eq-BS ′ y 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
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
⇀( 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
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 )
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).
Parties are serialized as a simple object with an address or role_token key, depending on the Party type.
instanceToJSON Partywhere
toJSON (Address address) =
object["address".=address]
toJSON (Role name) =
object["role_token".=name]
instanceFromJSON Partywhere
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"
is serialized as{"address":"example address"}, and
roleExample::Party
roleExample=Role"example role"
is serialized as{"role_token":"example role"}
The Token type is serialized as an object with two properties, currency_sym- bol and token_name
instanceToJSON Tokenwhere
toJSON (Token currSym tokName) =object
["currency_symbol".=currSym
,"token_name".=tokName
]
instanceFromJSON Tokenwhere
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"}
Payees are serialized as a simple object with an account or party key, de- pending on the Payee type.
instanceToJSON Payeewhere
toJSON (Account account) =
object["account".=account]
toJSON (Party party) =
object["party".=party]
instanceFromJSON Payeewhere
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"}}
The ChoiceId type is serialized as an object with two properties, choice_name and choice_owner
instanceToJSON ChoiceIdwhere
toJSON (ChoiceId name party) =object
["choice_name".=name
,"choice_owner".=party
]
instanceFromJSON ChoiceIdwhere
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
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
}
The Bound type is serialized as an object with two properties, from and to
instanceToJSON Boundwhere
toJSON (Bound from to) =object
["from".=from
,"to".=to
]
instanceFromJSON Boundwhere
parseJSON =withObject"Bound"(λv→
Bound<$>(getInteger"lower bound"=<<(v.:"from"))
<∗>(getInteger"higher bound"=<<(v.:"to"))
)
for example, the following Bound
exampleBound::Bound
exampleBound=Bound2 10
is serialized as{"from": 2,"to": 10}
The ValueId type is serialized as a literal string.
instanceToJSON ValueIdwhere
toJSON (ValueId x) =toJSON x
instanceFromJSON ValueIdwhere
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
strings, and the rest are serialized as a single object (with keys depending on the constructor).
instanceToJSON Valuewhere
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
]
instanceFromJSON Valuewhere
parseJSON (JSON.Object v) =
(AvailableMoney<$>(v.:"in_account")
<∗>(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 Value s 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"
AddValue
addExample::Value
addExample=AddValue(Constant1) (Constant2)
is serialized as{"add": 1,"and": 2}
SubValue
subExample::Value
subExample=SubValue(Constant4) (Constant2)
is serialized as{"minus": 2,"value": 4}
MulValue
mulExample::Value
mulExample=MulValue(Constant3) (Constant6)
is serialized as{"multiply": 3,"times": 6}
DivValue
divExample::Value
divExample=DivValue(Constant8) (Constant4)
is serialized as{"by": 4,"divide": 8}
NegValue
negateExample::Value
negateExample=NegValue(Constant3)
is serialized as{"negate": 3}
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
}
}
AvailableMoney
availableMoneyExample::Value
availableMoneyExample=AvailableMoney addressExample dolarToken
is serialized as
{
"amount_of_token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
},
"in_account": {
"address": "example address"
}
}
The Observation type is serialized as native boolean (for TrueObs and FalseObs ) or as an object with different properties, depending on the constructor.
instanceToJSON Observationwhere
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
["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
instanceFromJSON Observationwhere
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
TrueObs
trueExample::Observation
trueExample=TrueObs
is serialized astrue
FalseObs
falseExample::Observation
falseExample=FalseObs
is serialized asfalse
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}
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(Constant1) (Constant2)
is serialized as{"ge_than": 2,"value": 1}
ValueGT
valueGTExample::Observation
valueGTExample=ValueGT(Constant1) (Constant2)
is serialized as{"gt": 2,"value": 1}
ValueLT
valueLTExample::Observation
valueLTExample=ValueLT (Constant1) (Constant2)
is serialized as{"lt": 2,"value": 1}
ValueLE
valueLEExample::Observation
valueLEExample=ValueLE(Constant1) (Constant2)
is serialized as{"le_than": 2,"value": 1}
ValueEQ
valueEQExample::Observation
valueEQExample=ValueEQ(Constant1) (Constant2)
is serialized as{"equal_to": 2,"value": 1}
The Action type is serialized as an object with different properties, depending the constructor.
instanceToJSON Actionwhere
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]
instanceFromJSON Actionwhere
parseJSON =withObject"Action"(λv→
(Deposit<$>(v.:"into_account")
<∗>(v.:"party")
<∗>(v.:"of_token")
<∗>(v.:"deposits"))
<|>(Choice<$>(v.:"for_choice")
<∗>((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
[Bound0 1,Bound4 8]
is serialized as
"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"
}
}
}
}
The Case type is serialized as an object with two properties ( case and then ).
instanceToJSON Casewhere
toJSON (Case act cont) =object
["case".=act
,"then".=cont
]
instanceFromJSON Casewhere
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"
}
The Contract type is serialized as the literal string "close" or as an object, depending on the constructor
instanceToJSON Contractwhere
toJSON Close=JSON.String$T.pack"close"
toJSON (Pay accountId payee token value contract) =object
["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
]
instanceFromJSON Contractwhere 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) ))
<∗>(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
(Constant10)
Close
is serialized as
{
"from_account": {
"role_token": "example role"
},
"pay": 10,
"then": "close",
"to": {
"account": {
"address": "example address"
"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": [
"case": {
"notify_if": true
},
"then": "close"
},
{
"case": {
"notify_if": false
},
"then": "close"
}
]
}
Let
letExample::Contract
letExample=Let(ValueId"var") (Constant10)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": {
"address": "example address"
}
}
},
"then": "close"
}
The Input type is serialized as the literal string "input_notify" or as an object, depending on the constructor.
instanceToJSON Inputwhere
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"
instanceFromJSON Inputwhere
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
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",
"token_name": "dolar"
},
"that_deposits": 5
}
The Transaction type is serialized as an object with two properties, tx_in- terval and tx_inputs.
instanceToJSON(Transaction_ext a)where
toJSON (Transaction_ext(from,to)txInps ) =object
["tx_interval".=timeIntervalJSON
,"tx_inputs".=toJSONList(map toJSON txInps)
]
wheretimeIntervalJSON =object["from".=from
,"to".=to
]
instanceFromJSON(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()
whereparseTimeInterval=withObject"TimeInterval"(λv→
dofrom←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
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
}
}
The Payment type is serialized as a single object with three properties
instanceToJSON Paymentwhere
toJSON (Payment from to token amount) =object
["payment_from".=from
,"to".=to
,"token".=token
,"amount".=amount
]
instanceFromJSON Paymentwhere
parseJSON =withObject"Payment"
(λv→
Payment<$>(v.:"payment_from")
<∗>(v.:"to")
<∗>(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"
}
}
The State type is serialized as a single object with four properties. Each Map is represented by a list of key value tuples.
instanceToJSON(State_ext())where
toJSON (State_ext accounts choices boundValues minTime ) =object
["accounts".=toJSON accounts
,"choices".=toJSON choices
,"boundValues".=toJSON boundValues
,"minTime".=minTime
]
instanceFromJSON(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": [
["example",
30
]
],
"choices": [
[
{
"choice_name": "ada price",
"choice_owner": {
"address": "example address"
}
},
10
]
],
"minTime": 90
}The TransactionWarning type is serialized as a literal string (in case of Trans- actionAssertionFailed ) or as an object with different properties, depending the constructor.
instanceToJSON TransactionWarningwhere
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
,"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"
instanceFromJSON TransactionWarningwhere
parseJSON (JSON.String"assertion_failed") =
return TransactionAssertionFailed
parseJSON (JSON.Object v) =
(TransactionNonPositiveDeposit<$>(v.:"party")
<∗>(v.:"in_account")
<∗>(v.:"of_token")
<∗>(v.:"asked_to_deposit"))
<|>(domaybeButOnlyPaid←v.:?"but_only_paid"
casemaybeButOnlyPaid::Maybe Scientificof
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
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
20is serialized as
{
"account": {
"address": "example address"
},
"asked_to_pay": 20,
"of_token": {
"currency_symbol": "85bb65",
"token_name": "dolar"
},
"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
(ValueId"example")
4
5is serialized as
{
"had_value": 4,
"is_now_assigned": 5,
"value_id": "example"
}TransactionAssertionFailed
transactionAssertionFailedExample::TransactionWarning
transactionAssertionFailedExample=TransactionAssertionFailed
is serialized as"assertion_failed"
The IntervalError type is serialized as an object with a single property (de- pending on the constructor) and in a tuple, the values.
instanceToJSON IntervalErrorwhere
toJSON (InvalidInterval(s,e)) =object
[("invalidInterval".=toJSON(s,e))]
toJSON (IntervalInPastError t(s,e)) =object
[("intervalInPastError".=toJSON (t,s,e))]
instanceFromJSON IntervalErrorwhere
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<|>parseInvalidIntervalparseJSON 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=IntervalInPastError30 (10,20)
is serialized as{"intervalInPastError": [30, 10 ,20]}
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.
instanceToJSON TransactionErrorwhere
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
["tag".=JSON.String"TEUselessTransaction"
,"contents".=JSON.Null
]
instanceFromJSON TransactionErrorwhere
parseJSON=withObject"TransactionError"
(λv→
do
tag::String←v.:"tag"
casetagof
"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
"contents": null,
"tag": "TEApplyNoMatchError"
}TEIntervalError
teIntervalErrorExample::TransactionError
teIntervalErrorExample=TEIntervalError intervalInPastErrorExample
is serialized as
{
"contents": {
"intervalInPastError": [
30,
10,
20
]
},
"tag": "TEIntervalError"
}TEUselessTransaction
teUselessTransactionExample::TransactionError
teUselessTransactionExample=TEUselessTransactionis serialized as
{
"contents": null,
"tag": "TEUselessTransaction"
}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.
instanceToJSON TransactionOutputwhere
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)
]
instanceFromJSON TransactionOutputwhere
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"
}
}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"
}
}
],
"state": {
"accounts": [],
"boundValues": [],
"choices": [],
"minTime": 1664812900000
},
"warnings": []
}The Swap Example, defined in section §A.1.2is 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": {
"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": ""
} } } ] } } ] }
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
instanceToJSON Arith.Intwhere
toJSON (Int_of_integer x) =toJSON x
instanceFromJSON Arith.Intwhere
parseJSON (JSON.Number x) =getInteger"Int"x
parseJSON =fail"expecting integer"