The Marlowe data types

Marlowe

Ngôn ngữ dành riêng cho miền Marlowe (DSL) được mô hình hóa như được sử dụng ở trên, một tập hợp các loại đại số trong Haskell, với các hợp đồng được đưa ra theo loại Contract:

data Contract = Close
              | Pay Party Payee Token Value Contract
              | If Observation Contract Contract
              | When [Case] Timeout Contract
              | Let ValueId Value Contract
              | Assert Observation Contract

Basic components (Thành phần cơ bản)

Khi lập mô hình các phần cơ bản của Marlowe, chúng tôi sử dụng kết hợp datacác loại Haskell để xác định các loại mới và typecác từ đồng nghĩa đặt tên mới cho loại hiện có. 1

A Partytrong hợp đồng được thể hiện như đã sử dụng ở trên, là khóa chung hoặc tên vai trò.

data Party = PubKey PubKeyHash
           | Role   TokenName

Để tiến triển hợp đồng Marlowe, một bên phải cung cấp bằng chứng. Đối với PubKeybên đó, đó sẽ là chữ ký hợp lệ của giao dịch được ký bằng khóa riêng của khóa chung, tương tự như Pay to Public Key Hashcơ chế của Bitcoin.

newtype PubKeyHash = PubKeyHash { getPubKeyHash :: ByteString }

Đối với một Rolebên, bằng chứng là việc sử dụng mã thông báo vai trò trong cùng một giao dịch, thường là cho cùng một chủ sở hữu.

newtype TokenName = TokenName { unTokenName :: ByteString }

Role tham gia sẽ trông như thế nào Role "alice", Role "bob"v.v. Tuy nhiên, Haskell cho phép chúng ta trình bày và đọc các giá trị này chính xác hơn (bằng cách khai báo một phiên bản tùy chỉnh của Showvà sử dụng các chuỗi quá tải ) để chúng có thể được nhập và đọc như được sử dụng ở trên, "alice", "bob", v.v.

Tài khoản Marlowe nắm giữ số lượng nhiều loại tiền tệ và/hoặc mã thông báo có thể thay thế và không thay thế được. Một số tiền cụ thể được lập chỉ mục bởi a Token, là một cặp ký hiệu tiền tệ và tên mã thông báo , cả hai đều được cung cấp bởi a ByteString.

newtype CurrencySymbol = CurrencySymbol { unCurrencySymbol :: ByteString }
data Token = Token CurrencySymbol TokenName

Mã thông báo Ada của Cardano là:

ada = Token adaSymbol adaToken

Nhưng bạn có thể tự do tạo tiền tệ và mã thông báo của riêng mình bằng cách sử dụng cơ sở mã thông báo gốc của Cardano. Bạn có thể nghĩ về an Accountnhư đã sử dụng ở trên, bản đồ từ Tokenđến Integervà tất cả các tài khoản trong hợp đồng có thể được mô hình hóa như thế này:

type AccountId = Party
type Accounts = Map (AccountId, Token) Integer

Mã thông báo của một loại tiền tệ có thể đại diện cho các vai trò trong hợp đồng, ví dụ: "buyer" và "seller". Hãy nghĩ về một hợp đồng pháp lý theo nghĩa "sau đây được gọi như được sử dụng ở trên, Người biểu diễn/Nhà cung cấp/Nghệ sĩ/Nhà tư vấn". Bằng cách này, chúng tôi có thể tách rời khái niệm quyền sở hữu vai trò hợp đồng và làm cho nó có thể giao dịch được. Vì vậy, bạn có thể bán khoản vay của mình hoặc mua một phần vai trò trong một số hợp đồng.

Thời gian chờ và số tiền được xử lý theo cách tương tự; với cách tiếp cận hiển thị/quá tải tương tự như đã sử dụng ở trên, chúng sẽ xuất hiện trong hợp đồng dưới dạng số:

newtype POSIXTime = POSIXTime { getPOSIXTime :: Integer }
type Timeout = POSIXTime

Con số này biểu thị số giây sau nửa đêm ngày 1 tháng 1 năm 1970 (UTC).

Lưu ý rằng cô ấy "alice"là chủ sở hữu ở đây với nghĩa là cô ấy sẽ được hoàn lại bất kỳ khoản tiền nào có trong tài khoản khi hợp đồng chấm dứt.

Chúng tôi có thể sử dụng các chuỗi quá tải để cho phép chúng tôi viết tắt tài khoản này bằng tên của chủ sở hữu nó: trong trường hợp này là "alice".

Khoản thanh toán có thể được thực hiện cho một trong các bên của hợp đồng hoặc cho một trong các tài khoản của hợp đồng và điều này được phản ánh trong định nghĩa này:

data Payee = Account AccountId
           | Party Party

Các lựa chọn -- của số nguyên -- được xác định bằng cách ChoiceIdkết hợp tên của lựa chọn với Partyngười đã đưa ra lựa chọn:

type ChoiceName = ByteString
data ChoiceId   = ChoiceId ChoiceName Party
type ChosenNum  = Integer

Các giá trị được xác định bằng cách sử dụng Letđược xác định bằng chuỗi văn bản. 2

data ValueId    = ValueId ByteString

Values, observations and actions (Giá trị, quan sát và hành động)

Dựa trên các loại cơ bản, chúng ta có thể mô tả ba thành phần cấp cao hơn của hợp đồng: một loại giá trị , trên hết là một loại quan sát và cả một loại hành động kích hoạt các trường hợp cụ thể. Đầu tiên nhìn vào Valuechúng ta có:

data Value = AvailableMoney Party Token
           | Constant Integer
           | NegValue Value
           | AddValue Value Value
           | SubValue Value Value
           | MulValue Value Value
           | DivValue Value Value
           | ChoiceValue ChoiceId
           | TimeIntervalStart
           | TimeIntervalEnd
           | UseValue ValueId
           | Cond Observation Value Value

Các loại giá trị khác nhau -- tất cả đều Integer-- khá dễ hiểu, nhưng để đầy đủ, chúng ta có:

• Tra cứu giá trị trong một tài khoản AvailableMoney, được thực hiện theo lựa chọn ChoiceValuevà theo mã định danh đã được xác định UseValue.
• Các hằng số và toán tử.
• Điểm bắt đầu và kết thúc của khoảng thời gian hiện tại ; xem bên dưới để thảo luận thêm về điều này.
• Condđại diện cho biểu thức if, nghĩa là - đối số đầu tiên Cond là điều kiện ( Observation) cần kiểm tra, thứ hai là a Valuecần lấy khi điều kiện được thỏa mãn và đối số cuối cùng là a Valuecho điều kiện không thỏa mãn; ví dụ: (Cond FalseObs (Constant 1) (Constant 2))tương đương với (Constant 2)

Tiếp theo chúng ta có những quan sát:

data 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

Những điều này thực sự dễ hiểu: chúng ta có thể so sánh các giá trị về đẳng thức và thứ tự (trong) và kết hợp các quan sát bằng cách sử dụng các kết nối Boolean. Cấu trúc duy nhất khác ChoseSomethingcho biết liệu có bất kỳ lựa chọn nào đã được thực hiện cho một giá trị nhất định hay không ChoiceId.

Các trường hợp và hành động được đưa ra bởi các loại sau:

data Case = Case Action Contract

data Action = Deposit AccountId Party Token Value
            | Choice ChoiceId [Bound]
            | Notify Observation

data Bound = Bound Integer Integer

Có thể thực hiện ba loại hành động:

• A Deposit n p t vgửi giá trị vtoken ttừ bên pvào tài khoản n.
• Một lựa chọn được thực hiện cho một id cụ thể với danh sách giới hạn trên các giá trị có thể chấp nhận được. Ví dụ: đưa ra [Bound 0 0, Bound 3 5] lựa chọn một trong 0, 3và 4.5
• Hợp đồng được thông báo rằng một quan sát cụ thể sẽ được thực hiện. Thông thường, việc này sẽ được thực hiện bởi một trong các bên hoặc một trong các ví của họ hoạt động tự động.

Điều này hoàn thành cuộc thảo luận của chúng tôi về các loại hợp đồng tạo nên hợp đồng Marlowe.

Extended Marlowe (Marlowe mở rộng)

Marlowe mở rộng bổ sung chức năng tạo khuôn mẫu cho ngôn ngữ Marlowe, do đó các hằng số không cần phải "nối cứng" vào hợp đồng Marlowe mà có thể được thay thế bằng các tham số . Các đối tượng trong Extended Marlowe được gọi là mẫu hoặc mẫu hợp đồng .

Cụ thể, Extended Marlowe mở rộng Valueloại với các giá trị tham số sau:

ConstantParam "string"

có thể được sử dụng để hình thành các giá trị phức tạp hơn giống như cách tạo các hằng số. Tương tự, Timeoutloại được mở rộng với các giá trị sau:

TimeParam "string"

Marlowe mở rộng không thể thực thi trực tiếp, nó phải được dịch sang Marlowe lõi trước khi thực thi, triển khai hoặc phân tích thông qua quá trình khởi tạo . Mục đích của Extended Marlowe là cho phép các hợp đồng Marlowe có thể được tái sử dụng trong các tình huống khác nhau mà không làm lộn xộn mã đi trên chuỗi (Marlowe cốt lõi). Trong Marlowe Playground, các mẫu cần được khởi tạo trước khi mô phỏng.

Transactions (Giao dịch)

Như chúng tôi đã lưu ý trước đó, ngữ nghĩa của Marlowe bao gồm việc xây dựng các giao dịch , như thế này:

Một giao dịch được xây dựng từ một loạt các bước, một số bước sử dụng giá trị đầu vào và các bước khác tạo ra hiệu ứng hoặc thanh toán. Khi mô tả điều này, chúng tôi đã giải thích rằng một giao dịch đã sửa đổi một hợp đồng (để tiếp tục hợp đồng) và trạng thái, nhưng chính xác hơn là chúng tôi có một hàm:

computeTransaction :: TransactionInput -> State -> Contract -> TransactionOutput

nơi các loại được định nghĩa như thế này:

data TOR = TOR { txOutWarnings :: [TransactionWarning]
               , txOutPayments :: [Payment]
               , txOutState    :: State
               , txOutContract :: Contract }
            deriving (Eq,Ord,Show,Read)

data TransactionOutput =
   TransactionOutput TOR
 | Error TransactionError
deriving (Eq,Ord,Show,Read)

data TransactionInput = TransactionInput
      { txInterval :: TimeInterval
      , txInputs   :: [Input] }
   deriving (Eq,Ord,Show,Read)

Ký hiệu được sử dụng ở đây thêm tên trường vào các đối số của hàm tạo, cung cấp bộ chọn cho dữ liệu (như được sử dụng ở trên), cũng như làm rõ mục đích của từng trường.

Loại này TransactionInputcó hai thành phần: thành phần TimeIntervaltrong đó nó có thể được thêm vào blockchain một cách hợp lệ và một chuỗi các Inputgiá trị được sắp xếp để xử lý trong giao dịch đó.

Một TransactionOutputgiá trị có bốn thành phần: hai thành phần cuối cùng là giá trị được cập nhật Statevà Contract, trong khi giá trị thứ hai đưa ra một chuỗi có thứ tự do Paymentsgiao dịch tạo ra. Thành phần đầu tiên chứa danh sách mọi cảnh báo được tạo ra bằng cách xử lý giao dịch.

Time intervals (Các khoảng thời gian)

Đây là một phần trong kiến ​​trúc của Cardano/Plutus, thừa nhận rằng không thể dự đoán chính xác thời điểm một giao dịch cụ thể sẽ được xử lý. Do đó, các giao dịch được đưa ra một khoảng thời gian mà chúng dự kiến ​​sẽ được xử lý và điều này được chuyển sang Marlowe: mỗi bước của hợp đồng Marlowe được xử lý trong bối cảnh một khoảng thời gian.

type TimeInterval = (POSIXTime, POSIXTime)

Điều này ảnh hưởng như thế nào đến việc xử lý hợp đồng Marlowe? Mỗi bước được xử lý tương ứng với một khoảng thời gian và giá trị thời gian hiện tại cần nằm trong khoảng thời gian đó.

Các điểm cuối của khoảng có thể truy cập được dưới dạng các giá trị TimeIntervalStartvà TimeIntervalEnd(như được sử dụng ở trên) và chúng có thể được sử dụng trong các quan sát. Thời gian chờ cần phải được xử lý rõ ràng để tất cả các giá trị trong khoảng thời gian phải vượt quá thời gian chờ để giá trị đó có hiệu lực hoặc giảm trước thời gian chờ để quá trình thực thi bình thường có hiệu lực. Nói cách khác, giá trị thời gian chờ cần phải nhỏ hơn hoặc bằng TimeIntervalStart(để thời gian chờ có hiệu lực) hoặc lớn hơn TimeIntervalEnd (để thực thi bình thường).