Here we illustrate a case study in monitoring a Solidity smart contract with a deontic logic specification language, as published in the proceedings of Jurix 2018. We consider a smart contract implementing a procurement process, involving a buyer and a seller that agree to certain terms (e.g. the minimum number of items that need to be ordered during the term of the contract) involving the procurement of goods. This contract is specified formally and informally below. We are currently working on an implementation of contractLarva (github.com/gordonpace/contractlarva) that can take as input such a deontic contract specification (with more code-like actions) for automated instrumented of a smart contract with a monitor checking for the deontic contract.
procurement-simple.sol is the Solidity smart contract implementing this procurement interaction between the buyer and the seller.
procurement-simple-monitored.sol is the Solidity smart contract procurement-simple.sol monitored for the contract as specified formally below.
- This contract is between buyer-name, henceforth referred to as 'the buyer' and seller-name, henceforth referred to as 'the seller'. The contract will hold until either party requests its termination.
- The buyer is obliged to order at least minimum-items, but no more than maximum-items items for a fixed price price before the termination of this contract.
- Notwithstanding clause 1, no request for termination will be accepted before contract-end-date. Furthermore, the seller may not terminate the contract as long as there are pending orders.
- Upon enactment of this contract, the buyer is obliged to place the cost of the minimum number of items to be ordered in escrow.
- Upon accepting this contract, the seller is obliged to place the amount of performance-guarantee in escrow, otherwise, if only a partial amount is placed, the seller is obliged to place the rest by a time period at the buyer's discretion.%the contract is terminated and the buyer's and seller's respective escrow is returned.
- While the contract has not been terminated, the buyer has the right to place an order for an amount of items and a specified time-frame as long as (i) the running number of items ordered does not exceed the maximum stipulated in clause 2; and (ii) the time-frame must be of at least 24 hours, but may not extend beyond the contract end date specified in clause 2/
- Upon placing an order, the buyer is obliged to ensure that there is enough money in escrow to cover payment of all pending orders.
- Before termination of the contract, upon delivery the seller must receive payment of the order.
- Upon termination of the contract, if either any orders were undelivered or more than 25% of the orders were delivered late, the buyer has the right to receive the performance guarantee placed in escrow according to clause 5.
C1. P(TerminateContractUnlessOtherwiseForbidden)
C2. F(TeminateContractWithItemsNotBetweenMinAndMaxItems)
C3. F(TerminateContractBeforeEndTimestamp) & F(TerminateContractBySellerAndWithPendingOrders)
C4. F(EnactmentWithLessThanCostOfMinimumItems)
C5. F(AcceptContractWithLessThanGuarantee) ▷ O(SendRestOfGuarantee)
C6. [ContractNotTerminated]P(OrderWithLessThanMaxItemsAndDeliveryTimeLessThanOneDayAndBeforeEnd)
C7. F(OrderWithLessThanEnoughMoneyForPendingOrders)
C8. [ContractNotTerminated]F(DeliveryWithPaymentLessThanCost)
C9. [TerminateContractWithPendingOrdersOrQuarterLateOrders]O(SendGuaranteeToBuyer)&[TerminateContractWithoutPendingOrdersAndQuarterLateOrders]O(SendGuaranteeToSeller)
ProcurementContract = rec X. [¬Ψ]((C4 & C5) ; X) & [¬Ψ](rec Y. (C1 & C2 & C3 & C6 & C7 & C8 & C9); Y)
where Ψ = EnactmentAndSellerAcceptanceWithEnoughInEscrow