Bài 2: Mô hình Marlowe

Marlowe được thiết kế để hỗ trợ thực hiện các hợp đồng tài chính trên blockchain và đặc biệt là hoạt động trên Cardano. Hợp đồng được xây dựng bằng cách tập hợp một số lượng nhỏ các cấu trúc có thể được kết hợp để mô tả nhiều loại hợp đồng tài chính khác nhau.

Trước khi chúng ta mô tả các cấu trúc đó, chúng ta cần xem xét cách tiếp cận chung của chúng ta để tạo mô hình hợp đồng trong Marlowe và bối cảnh mà các hợp đồng Marlowe được thực hiện, blockchain Cardano. Khi làm điều này, chúng ta cũng giới thiệu một số thuật ngữ mà chúng ta sẽ sử dụng, chỉ ra các định nghĩa bằng cách in nghiêng.

Hợp đồng

Các hợp đồng trong Marlowe chạy trên một blockchain, nhưng cần phải tương tác với thế giới ngoài chuỗi. Các bên của hợp đồng, mà chúng ta còn gọi là những người tham gia, có thể tham gia vào các thực thi khác nhau : họ có thể được yêu cầu gửi tiền hoặc lựa chọn giữa các lựa chọn thay thế khác nhau. Thông báo về giá trị bên ngoài (còn được gọi là giá trị Oracle ), chẳng hạn như giá hiện tại của một loại hàng hóa cụ thể, là một hình thức đầu vào có thể có khác. [1]

Việc thực hiện hợp đồng cũng sẽ tạo ra các tác động bên ngoài, bằng cách thanh toán cho các bên trong hợp đồng.

Những người tham gia và vai trò

Chúng ta nên tách biệt khái niệm về người tham gia và vai trò trong hợp đồng Marlowe. Các vai trò trong hợp đồng là cố định và không thay đổi, và có thể được đặt tên party, counterparty v.v. Mặt khác, những người tham gia bị ràng buộc với vai trò hợp đồng có thể thay đổi trong quá trình thực hiện phiên bản hợp đồng cụ thể. Điều này cho phép các vai trò trong việc chạy hợp đồng được giao dịch giữa những người tham gia, thông qua cơ chế mã hóa. Điều này sẽ có sẵn trong quá trình triển khai trên chuỗi của Marlowe nhưng mô phỏng trong Marlowe Playground chỉ đơn giản là trình bày các vai trò hợp đồng.

Tài khoản

Mô hình Marlowe cho phép hợp đồng lưu trữ tài sản. Tất cả các bên tham gia hợp đồng đều mặc nhiên sở hữu một tài khoản mang tên mình. Tất cả tài sản được lưu trữ trong hợp đồng phải có trong tài khoản của một trong các bên; theo cách này, khi hợp đồng được kết thúc, tất cả tài sản còn lại trong hợp đồng đều thuộc về một người nào đó và do đó có thể được hoàn lại cho chủ sở hữu tương ứng của họ. Các tài khoản này là cục bộ : chúng chỉ tồn tại trong thời gian thực hiện hợp đồng và trong thời gian đó, chúng chỉ có thể truy cập được từ bên trong hợp đồng.

Các bước và trạng thái

Hợp đồng Marlowe mô tả một loạt các bước, thường bằng cách mô tả bước đầu tiên, cùng với một hợp đồng (phụ) khác mô tả những việc cần làm tiếp theo. Ví dụ: hợp đồng Pay a p t v cont có nội dung “thanh toán giá trị v token t cho bên p từ tài khoản a, sau đó thực hiện theo hợp đồng cont". chúng ta gọi cont là sự tiếp tục của hợp đồng.

Khi thực hiện hợp đồng, chúng ta cần theo dõi hợp đồng hiện tại : sau khi thực hiện một bước trong ví dụ trên, hợp đồng hiện tại là sự tiếp tục, cont. chúng ta cũng phải theo dõi một số thông tin khác, chẳng hạn như số tiền được giữ trong mỗi tài khoản: chúng ta gọi thông tin này là trạng thái: điều này cũng có thể thay đổi ở mỗi bước. Một bước cũng có thể thấy một thực thi đang diễn ra, chẳng hạn như tiền được gửi hoặc một hiệu ứng được tạo ra, ví dụ như một khoản thanh toán.

blockchain

Mặc dù Marlowe được thiết kế để hoạt động với các blockchains nói chung, [2] một số chi tiết về cách nó tương tác với blockchain có liên quan khi mô tả ngữ nghĩa và cách triển khai của Marlowe.

Một blockchain dựa trên UTxO là một chuỗi các khối, mỗi khối chứa một tập hợp các giao dịch. Mỗi giao dịch có một tập hợp các đầu vào và đầu ra và blockchain được xây dựng bằng cách liên kết các đầu ra giao dịch chưa sử dụng (UTxO) với các đầu vào của một giao dịch mới. Có thể tạo nhiều nhất một khối trong mỗi slot, dài 1 giây.

Các cơ chế mà các khối này được tạo ra và do ai tạo ra, không có liên quan ở đây, nhưng các hợp đồng sẽ được thể hiện dưới dạng số slot, tính từ khối bắt đầu (“genesis”) của blockchain. Hiện tại, chúng ta sử dụng số slot trong mô phỏng Marlowe Playground, nhưng trên chuỗi, chúng ta sẽ sử dụng thời gian, áp dụng tiêu chuẩn thời gian Posix.

UTxO, ví và ứng dụng Marlowe Run

Giá trị trên blockchain nằm trong UTxO, được bảo vệ bằng mật mã bằng khóa riêng do chủ sở hữu nắm giữ. Các khóa này có thể được sử dụng để đổi đầu ra và do đó, để sử dụng chúng làm đầu vào cho các giao dịch mới, có thể được coi là chi tiêu giá trị trong đầu vào. Người dùng thường theo dõi các khóa cá nhân của họ và các giá trị được đính kèm với chúng, trong một chiếc ví an toàn bằng mật mã.

Để tương tác với một hợp đồng chạy trên blockchain, người dùng sẽ cần sử dụng ứng dụng khách Marlowe Run. Đổi lại, điều này sẽ tương tác với ví của người dùng để xác thực các giao dịch sử dụng tài sản tiền điện tử, vì tiền gửi được thực hiện từ ví của người dùng và các khoản thanh toán được họ nhận. Tuy nhiên, lưu ý rằng đây chắc chắn là những thực thi ngoài chuỗi cần được bắt đầu bằng mã chạy ngoài chuỗi, thường điều này sẽ có trong ứng dụng Marlowe Run: chúng không thể xảy ra bởi chính hợp đồng chạy trên chuỗi.

Mô phỏng toàn diện

Marlowe Playground hỗ trợ mô phỏng hợp đồng. Đây là một mô phỏng toàn diện, trong đó người dùng có thể thực hiện bất kỳ thực thi nào cho bất kỳ vai trò nào và do đó có thể quan sát việc thực hiện từ quan điểm của tất cả người dùng cùng một lúc. Điều này trái ngược với trải nghiệm chạy hợp đồng trong Marlowe Run, trong đó mỗi người tham gia nhìn nhận hợp đồng theo quan điểm của riêng họ. Đặc biệt, những người tham gia chỉ có thể tương tác với một hợp đồng đang chạy đang chờ đợi ý kiến đóng góp từ họ; nếu không phải như vậy, thì họ sẽ thấy rằng việc thực hiện hợp đồng đang chờ đợi sự tham gia của người khác.

Giá trị và token

Trong các ví dụ trước, bất cứ khi nào Value bắt buộc phải có, chúng ta đã sử dụng riêng Ada. Điều này rất có ý nghĩa, vì ADA là tiền tệ cơ bản được hỗ trợ bởi Cardano.

Tuy nhiên, Marlowe đưa ra một khái niệm tổng quát hơn về Value, hỗ trợ các token gốc, tùy chỉnh, có thể thay thế được, không thể thay thế hoặc thực sự là hỗn hợp [3]. Trong Marlowe Value là gì?

newtype Value = Value
    {getValue :: Map CurrencySymbol (Map TokenName Integer)}

Các loại CurrencySymbol và TokenName đều là các trình bao bọc đơn giản xung quanh ByteString.

Khái niệm giá trị này bao gồm Ada, token có thể thay thế (tiền tệ), token không thể thay thế hoặc NFT (token tùy chỉnh không thể hoán đổi với các token khác) và các trường hợp hỗn hợp kỳ lạ hơn:

• Ada có bytestring trống là CurrencySymbol và TokenName.
• Một token có thể thay thế được đại diện bởi một mã CurrencySymbol mà có chính xác một mã TokenName có thể có số lượng nguyên không âm tùy ý (trong đó Ada là một trường hợp đặc biệt).
• Một loại token không thể thay thế là một CurrencySymbol với một số TokenNames, mỗi mã có số lượng là một. Mỗi tên trong số này tương ứng với một token không thể thay thế duy nhất.
• token hỗn hợp là những mã có nhiều TokenNames và số lượng lớn hơn một.

Cardano cung cấp một cách đơn giản để giới thiệu một loại tiền mới bằng cách sử dụng các kịch bản chính sách đúc tiền. Điều này nhúng hiệu quả các tiêu chuẩn Ethereum ERC-20 / ERC-721 làm giá trị nguyên thủy trong Cardano. Ở Marlowe, chúng ta sử dụng token tùy chỉnh để đại diện cho những người tham gia trong mỗi hợp đồng thực thi trên chuỗi.

Thực hiện hợp đồng Marlowe

Thực thi hợp đồng Marlowe trên blockchain Cardano có nghĩa là ràng buộc các giao dịch do người dùng tạo theo logic của hợp đồng. Nếu, tại một thời điểm thực hiện cụ thể, một hợp đồng yêu cầu Alice đặt cược 100 Ada, thì chỉ một giao dịch như vậy sẽ thành công, mọi thứ khác sẽ bị từ chối.

Một giao dịch chứa danh sách các đầu vào hoặc thực thi được sắp xếp theo thứ tự. Trình thông dịch Marlowe được thực thi trong quá trình xác thực giao dịch. Đầu tiên, nó đánh giá hợp đồng từng bước cho đến khi không thể thay đổi được nữa mà không cần xử lý bất kỳ đầu vào nào, một điều kiện được gọi là tĩnh. Ở giai đoạn này, chúng ta tiến bộ qua bất kỳ thời gian chờ nào đã trôi qua, When và tất cả If, Let, Pay và Close cấu trúc mà không tiêu tốn bất kỳ đầu vào nào.

Đầu vào đầu tiên sau đó được xử lý, và sau đó hợp đồng được thực hiện lại một bước cho đến khi ổn định, và quá trình này được lặp lại cho đến khi tất cả các đầu vào được xử lý. Tại mỗi bước, địa chỉ liên hệ hiện tại và trạng thái sẽ thay đổi, một số thông tin đầu vào có thể được xử lý và các khoản thanh toán được thực hiện.

Một giao dịch như vậy, như được hiển thị trong sơ đồ bên dưới, được thêm vào blockchain. Những gì chúng ta làm tiếp theo là mô tả chi tiết các hợp đồng Marlowe trông như thế nào và chúng được đánh giá từng bước như thế nào.

Chúng ta đã chỉ ra rằng hành vi của Marlowe độc lập với cách thu thập đầu vào vào các giao dịch và vì vậy khi mô phỏng thực thi của một hợp đồng, chúng ta không cần phải nhóm các đầu vào vào giao dịch một cách rõ ràng. Để rõ ràng, chúng ta có thể nghĩ rằng mỗi giao dịch có nhiều nhất một đầu vào. Mặc dù ngữ nghĩa của hợp đồng độc lập với cách các đầu vào được nhóm thành các giao dịch, nhưng chi phí thực hiện có thể thấp hơn nếu nhiều đầu vào có thể được nhóm thành một giao dịch duy nhất.

Trong mô phỏng toàn trí có sẵn trong Marlowe Playground, chúng ta có thể tách khỏi nhóm giao dịch một cách an toàn, vì việc nhóm không ảnh hưởng đến hành vi của hợp đồng.

Xây dựng giao dịch

[1] Chúng ta có thể coi oracles như một loại bên khác của hợp đồng; dưới chế độ xem này, các thông báo trở thành lựa chọn của bên đó.

[2] Thật vậy, Marlowe có thể được sửa đổi để chạy khỏi blockchain hoặc hoạt động trên một blockchain được cấp phép.

[3] Điều này phản ánh mô hình giá trị cho Plutus.

[4] Trong bài báo của chúng ta [Marlowe: thực hiện và phân tích các hợp đồng tài chính trên blockchain]

•