Các kiểu dữ liệu trong Marlowe

Hướng dẫn này chính thức giới thiệu Marlowe như một kiểu dữ liệu Haskell, cũng như trình bày các kiểu khác nhau được sử dụng bởi mô hình và thảo luận một số giả định về cơ sở hạ tầng mà các hợp đồng sẽ được chạy. Nó cũng giới thiệu Marlowe mở rộng mà chúng tôi sử dụng để mô tả các mẫu hợp đồng trong Marlowe.

Mã nguồn mà chúng tôi mô tả ở đây đến từ các mô-đun Haskell Semantics / Types.hs , Semantics.hs và Util.hs.

Marlowe

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

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

Chúng ta đã xem trong phần hướng dẫn trước những gì mà các hợp đồng này thực hiện. Trong phần còn lại của hướng dẫn này, chúng ta sẽ tìm hiểu sâu hơn một chút về các loại Haskell được sử dụng để đại diện cho các thành phần khác nhau của hợp đồng, bao gồm tài khoản, giá trị, quan sát và hành động. Chúng ta cũng sẽ xem xét các loại liên quan đến việc thực hiện hợp đồng, bao gồm đầu vào, trạng thái, môi trường.

Thành phần cơ bản

Trong mô hình hóa các phần cơ bản của Marlowe, chúng tôi sử dụng kết hợp các kiểu Haskell data, xác định các kiểu mới và typetừ đồng nghĩa đặt tên mới cho một kiểu hiện có. 1

Một Partyhợp đồng được trình bày như đã sử dụng ở trên, một khóa công khai hoặc một tên vai trò.

data Party = PubKey PubKeyHash
           | Role   TokenName

Để tiến hành 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 công khai, tương tự như cơ chế Pay to Public Key Hash của Bitcoin.

newtype PubKeyHash = PubKeyHash { getPubKeyHash :: ByteString }

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

newtype TokenName = TokenName { unTokenName :: ByteString }

Role nhiều bên sẽ như 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 một cách ngắn gọn hơn (bằng cách khai báo một phiên bản tùy chỉnh Show và sử dụng các chuỗi được nạp chồng - overloaded strings) để chúng có thể được nhập và đọc như được sử dụng ở trên , "alice""bob", v.v.

Một tài khoản Marlowe chứa nhiều loại tiền tệ và / hoặc các mã thông báo có thể thay thế và không thể thay thế. Một số tiền cụ thể được lập chỉ mục bởi Token, là một cặp ký hiệu tiền tệ (currency symbol) và tên mã thông báo (token name), cả hai đều được cho bởi 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ề một Accountnhư đã sử dụng ở trên, một bản đồ từ Token đến Integervà vì vậy tất cả các tài khoản trong hợp đồng có thể được mô hình hóa như sau:

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 là đượ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 ta 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 hợp đồng nào đó.

Thời gian chờ và số tiền được xử lý theo cách tương tự; với cùng một cách tiếp cận hiển thị / quá tải 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ố đại diện cho số giây sau nửa đêm của ngày 1 tháng 1 năm 1970 (UTC).

Lưu ý rằng "alice"ở đây là chủ sở hữu với nghĩa là cô ấy sẽ được hoàn trả bất kỳ khoản tiền nào 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: trong trường hợp này "alice".

Một 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

data Payee = Account AccountId
           | Party Party

Lựa chọn - trong số các số nguyên - được xác định bằng cách ChoiceIdkết hợp tên cho 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

Giá trị, quan sát và hành động

Dựa trên các loại cơ bản, chúng tôi 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 đó là một loại quan sát và cũng là 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 là Integer- đều có thể tự giải thích được khá nhiều, nhưng để hoàn thiện chúng ta có

• Tra cứu giá trị trong tài khoản AvailableMoney, được thực hiện theo lựa chọn ChoiceValuevà trong số nhận dạng đã được xác định UseValue.

• Hằng số số học và toán tử.

• Bắt đầu và kết thúc khoảng thời gian (time interval) 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 các biểu thức if, nghĩa là - đối số đầu tiên Condlà điều kiện ( Observation) để kiểm tra, đối số thứ hai là Valueđể nhận khi điều kiện được thỏa mãn và đối số cuối cùng là đối số Valueđối với điều kiện không được thỏa mãn; ví dụ: tương đương với (Cond FalseObs (Constant 1) (Constant 2))(Constant 2)

Tiếp theo, chúng tôi có 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ị cho (trong) bình đẳng và thứ tự, đồng thời 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 khác duy nhất ChoseSomethingcho biết liệu có bất kỳ sự 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:

• Deposit n p t v thực hiện một khoản tiền gửi có giá trị v của mã thông báo t từ bên p và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 các giới hạn trên các giá trị có thể chấp nhận được. Ví dụ: [Bound 0 0, Bound 3 5] cung cấp sự lựa chọn của một trong số 0, 3, 4, 5.

• Hợp đồng được thông báo rằng một quan sát cụ thể được thực hiện. Thông thường, điều 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 Marlowe.

Marlowe mở rộng

Extended Marlowe 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 "kết nối cứng" vào các hợp đồng Marlowe mà có thể được thay thế bằng các tham số (parameters). Các đối tượng trong Extended Marlowe được gọi là mẫu (templates) hoặc mẫu hợp đồng (contract templates).

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

ConstantParam "string"

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

ConstantParam "string"

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

TimeParam "string"

Extended Marlowe không thể thực thi trực tiếp, nó phải được dịch sang Marlowe cốt 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 (instantiation). Mục đích của Extended Marlowe là cho phép các hợp đồng Marlowe có thể được sử dụng lại 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 Run và các mẫu Marlowe Playground cần được khởi tạo trước khi chạy hoặc mô phỏng tương ứng.

Giao dịch

Như chúng tôi đã lưu ý trước đó, ngữ nghĩa của Marlowe bao gồm trong 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à một số 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 nó) và trạng thái, nhưng chính xác hơn là chúng tôi có một chức năng

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

trong đó 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 đố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õ ràng hơn mục đích của từng trường.

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

Giá TransactionOutputtrị 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 cung cấp một chuỗi có thứ tự Paymentsdo giao dịch tạo ra. Thành phần đầu tiên chứa danh sách bất kỳ cảnh báo nào được tạo ra bằng cách xử lý giao dịch.

Các khoảng thời gian

Đây là một phần của 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ể nào đó 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 cho Marlowe: mỗi bước của hợp đồng Marlowe được xử lý trong bối cảnh của 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ý liên quan đến 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 đượ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ờ để nó có hiệu lực hoặc rơi trước thời gian chờ để 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 hoàn toàn TimeIntervalEnd (để thực hiện bình thường diễn ra).

Ghi chú

Mô hình đưa ra một số giả định về cơ sở hạ tầng blockchain mà nó được chạy.

• Giả định rằng các chức năng và hoạt động mật mã được cung cấp bởi một lớp bên ngoài Marlowe, và vì vậy chúng không cần được mô hình hóa một cách rõ ràng.

• Đặt cọc không phải là việc mà hợp đồng có thể thực hiện; thay vào đó, nó có thể yêu cầu một khoản tiền gửi được thực hiện, nhưng sau đó phải được thiết lập bên ngoài: do đó, đầu vào của (một tập hợp) tiền gửi cho mỗi giao dịch.

• Mô hình quản lý việc hoàn lại tiền cho chủ sở hữu của một tài khoản cụ thể khi hợp đồng đạt đến điểm Close.

[1] Trên thực tế, chúng tôi đã sử dụng các newtypekhai báo hơn là datacác kiểu vì chúng được triển khai hiệu quả hơn.

[2] Điều này có thể được sửa đổi trong tương lai để cho phép các giá trị được đặt tên theo chuỗi.