Bài 6: Các kiểu dữ liệu 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 Extended Marlowe mà chúng ta sử dụng để mô tả các mẫu hợp đồng trong Marlowe.

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

Marlowe

Ngôn ngữ ngành riêng biệt 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 kiểu 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

Chúng ta đã thấy 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à thực thi. 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 ta sử dụng kết hợp các kiểu Haskell data, xác định các kiểu mới và type từ đồng nghĩa đặt tên mới cho một kiểu hiện có. [1]

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

data Party = PubKey ByteString
           | Role   ByteString

Để tiến hành hợp đồng Marlowe, một bên phải cung cấp bằng chứng. Đối với PubKey bê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ế của Pay to Public Key Hash của Bitcoin. Đối với một bên Role, bằng chứng đang sử dụng token vai trò trong cùng một giao dịch, thường cho cùng một chủ sở hữu.

Các bên Role sẽ là 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 Show tùy chỉnh của và sử dụng các chuỗi được nạp chồng ) để 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 token 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 token, cả hai đều được cho bởi a ByteString.

data Token = Token ByteString ByteString

token Ada của Cardano là

ada = Token adaSymbol adaToken

Nhưng bạn có thể tự do tạo tiền tệ và token của riêng mình bằng cách sử dụng cơ sở token gốc của Cardano. Bạn có thể nghĩ về một Tài khoản như được sử dụng ở trên, 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 Accounts = Map (AccountId, Token) Integer

Token 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 đó.

Số xèng 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ố:

data Slot    = Slot Integer
type Timeout = Slot

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 ta có thể sử dụng các chuỗi quá tải để cho phép chúng ta viết tắt tài khoản này bằng tên của chủ sở hữu tài khoản: 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 Party
           | Party Party

Lựa chọn - trong số các số nguyên - được xác định bằng cách ChoiceId kết hợp tên cho lựa chọn với Party người đã đưa ra lựa chọn:

type ChoiceName = Text
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 Text

Giá trị, quan sát và thực thi

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 đó là một loại quan sát và cũng là một loại thực thi, 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
           | SlotIntervalStart
           | SlotIntervalEnd
           | UseValue ValueId
           | Cond Observation Value Value

Các loại giá trị khác nhau - tất cả đều như vậy Integer - đều có thể tự giải thích được, 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 ChoiceValue và trong số nhận dạng đã được xác định UseValue.
• Hằng số học và toán tử.
• Khoảng thời gian 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 các biểu thức if, nghĩa là - đối số đầu tiên Cond là điều kiện (Observation) để kiểm tra, đối số thứ hai là Value để lấy 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 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ó 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 ChoseSomething cho 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à thực thi được đưa ra bởi các loại sau:

data Case = Case Action Contract

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

data Bound = Bound Integer Integer

Có thể thực hiện ba loại thực thi:

• A Deposit n p t v thực hiện một khoản tiền gửi v có giá trị của token 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 và 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 ta về các loại hợp đồng Marlowe.

Marlowe mở rộng

Marlowe mở rộng thêm hàm tạo khuôn mẫu cho ngôn ngữ Marlowe, để các hằng số không cần phải “có dây cứng” vào các 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 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ự, Slotkiểu được mở rộng với các giá trị sau:

SlotParam "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. 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 ta đã 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 ta giải thích rằng một giao dịch đã sửa đổi hợp đồng (để tiếp tục nó) và trạng thái, nhưng chính xác hơn là chúng ta có một hàm

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 :: SlotInterval
                      , 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 TransactionInput có hai thành phần: SlotInterval trong đó nó có thể được thêm vào blockchain một cách hợp lệ và một chuỗi Input giá trị có thứ tự sẽ được xử lý trong giao dịch đó.

Giá trị TransactionOutput có bốn thành phần: hai thành phần cuối cùng là giá trị được cập nhật State và Contract, trong khi giá trị thứ hai cung cấp một chuỗi có thứ tự Payments do 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.

Khoảng Slot

Đâ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 slot mà một giao dịch cụ thể sẽ được xử lý. Do đó, các giao dịch được cung cấp 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 loạt các slot.

data Slot         = Slot Integer

data SlotInterval = SlotInterval Slot Slot

ivFrom, ivTo :: SlotInterval -> Slot
ivFrom (SlotInterval from _) = from
ivTo   (SlotInterval _ to)   = to

Đ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 khoảng thời gian slot và giá trị slot 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ị SlotIntervalStart và SlotIntervalEnd (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 slot phải vượt quá thời gian chờ để nó có hiệu lực hoặc giảm 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 SlotIntervalStart (để thời gian chờ có hiệu lực) hoặc lớn hơn hoàn toàn SlotIntervalEnd (để 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 hàm 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.
• chúng ta giả định rằng thời gian là "dạng hạt thô" và được đo bằng số khối hoặc slot, do đó, cụ thể là thời gian chờ được phân định bằng số khối / slot.
• đặt cược không phải là điều 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 đó là đầ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 thời điểm Close .

[1] Trên thực tế, chúng ta đã sử dụng các newtype khai 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.

•