Bài 16: Triển khai Marlowe trong Plutus

Cho đến nay, những hướng dẫn này đã xử lý Marlowe như một hiện vật 'độc lập'; hướng dẫn này mô tả cách Marlowe được triển khai trên blockchain, sử dụng 'chuỗi mô phỏng' cung cấp mô phỏng có độ chính xác cao của lớp Cardano SL.

Triển khai

Để triển khai các hợp đồng Marlowe, chúng ta sử dụng trình biên dịch PlutusTx, trình biên dịch này sẽ biên dịch mã Haskell thành mã Plutus Core được tuần tự hóa, để tạo một tập lệnh Trình xác thực Cardano đảm bảo thực hiện hợp đồng chính xác. Hình thức triển khai này dựa trên các phần mở rộng của mô hình UTXO được mô tả trong bài viết này.

Việc thực thi hợp đồng Marlowe trên blockchain bao gồm một chuỗi các giao dịch, ở mỗi giai đoạn, hợp đồng còn lại và trạng thái của nó được chuyển qua tập lệnh dữ liệu, đồng thời các hành động và đầu vào (tức là lựa chọn và giá trị Oracles) được chuyển dưới dạng redeeemer Scripts. Mỗi bước trong quá trình thực thi hợp đồng là một giao dịch sử dụng đầu ra tập lệnh hợp đồng Marlowe bằng cách cung cấp đầu vào hợp lệ trong tập lệnh redeeemer và tạo đầu ra giao dịch với hợp đồng Marlowe là phần tiếp theo (hợp đồng còn lại) ngoài các đầu vào và đầu ra khác.

Không gian thiết kế

Có một số cách để thực hiện hợp đồng Marlowe trên Plutus. Chúng ta có thể viết một trình biên dịch Marlowe thành Plutus để chuyển đổi từng hợp đồng Marlowe thành một tập lệnh Plutus cụ thể. Thay vào đó, chúng ta đã chọn thực hiện một phiên dịch viên của hợp đồng Marlowe. Cách tiếp cận này có một số ưu điểm:

• Rất đơn giản: chúng ta triển khai một tập lệnh Plutus duy nhất có thể được sử dụng cho tất cả các hợp đồng Marlowe, do đó, việc triển khai, xem xét và kiểm tra những gì chúng ta đã thực hiện trở nên dễ dàng hơn.
• Nó gần với ngữ nghĩa của Marlowe, như được mô tả trong hướng dẫn trước đó, vì vậy, nó dễ dàng xác thực hơn.
• Điều đó có nghĩa là cùng một cách triển khai có thể được sử dụng cho cả việc thực thi mã Marlowe trên và off-chain (ví).
• Nó cho phép đánh giá hợp đồng phía máy khách, trong đó chúng ta sử dụng lại cùng một mã để thực hiện mô phỏng thực thi hợp đồng (ví dụ: trong IDE) và biên dịch nó thành WASM/JavaScript ở phía máy khách (ví dụ: trong Plutus hoặc Marlowe Playground).
• Có một trình thông dịch duy nhất cho tất cả (hoặc một nhóm cụ thể) hợp đồng Marlowe cho phép giám sát blockchain đối với các loại hợp đồng này, nếu muốn.
• Cuối cùng, có khả năng xử lý trường hợp đặc biệt loại tập lệnh này và triển khai một trình thông dịch chuyên dụng, hiệu quả cao trong chính Cardano CL.

Trong quá trình triển khai, chúng ta lưu trữ hợp đồng còn lại trong tập lệnh dữ liệu (xem Phần 4) để mọi người có thể nhìn thấy hợp đồng đó. Điều này đơn giản hóa việc phản ánh và xem xét lại hợp đồng.

Vòng đời hợp đồng trên mô hình UTXO mở rộng

Việc triển khai hiện tại hoạt động trên mô hình chuỗi, như được mô tả trong TODO. Chúng ta hy vọng chỉ phải thực hiện những thay đổi tối thiểu để chạy trong quá trình triển khai sản xuất vì chuỗi mô phỏng được thiết kế để trung thành với điều đó.

Như chúng ta đã mô tả ở trên, trình thông dịch Marlowe được hiện thực hóa dưới dạng tập lệnh xác thực. Chúng ta có thể chia việc thực hiện Hợp đồng Marlowe thành ba giai đoạn: khởi tạo/tạo, thực hiện và hoàn thành.

Khởi tạo/Tạo. Khởi tạo và khởi tạo hợp đồng được thực hiện dưới dạng một giao dịch có ít nhất một đầu ra tập lệnh (hiện tại nó phải là đầu ra đầu tiên), với hợp đồng Marlowe cụ thể trong tập lệnh dữ liệu và được bảo vệ bởi tập lệnh trình xác thực Marlowe. Giao dịch phải đặt một số tiền (ít nhất một Lovelace) vào đầu ra giao dịch đó để nó trở thành đầu ra giao dịch chưa chi tiêu (UTXO). Chúng ta coi giá trị này là tiền đặt cọc hợp đồng, có thể được chi tiêu trong giai đoạn hoàn thành. Lưu ý rằng chúng ta không đặt bất kỳ hạn chế nào đối với đầu vào giao dịch, vốn có thể sử dụng bất kỳ đầu ra giao dịch nào khác, bao gồm cả tập lệnh. Có thể khởi tạo hợp đồng với một trạng thái cụ thể, chứa một số cam kết, như được hiển thị ở đây.

Chấp hành. Việc thực thi hợp đồng Marlowe bao gồm một chuỗi các giao dịch, trong đó hợp đồng và trạng thái còn lại được chuyển qua tập lệnh dữ liệu, đồng thời các hành động và thông tin đầu vào (tức là lựa chọn và giá trị Oracles ) được chuyển dưới dạng redeeemer tập lệnh.

Mỗi bước là một giao dịch sử dụng đầu ra tập lệnh hợp đồng Marlowe bằng cách cung cấp đầu vào hợp lệ trong tập lệnh Redeemer và tạo đầu ra giao dịch với hợp đồng Marlowe dưới dạng tiếp tục, như có thể thấy ở đây.

Trình thông dịch Marlowe trước tiên xác nhận hợp đồng và trạng thái hiện tại. Nghĩa là, chúng ta kiểm tra xem hợp đồng có sử dụng đúng các mã định danh hay không và giữ ít nhất những gì cần có, cụ thể là khoản tiền đặt cọc và các khoản cam kết chưa thanh toán.

Sau đó, chúng ta đánh giá hợp đồng gia hạn và trạng thái của nó, sử dụng chức năng eval ,

eval :: Input -> Slot -> Ada -> Ada -> State -> Contract -> (State,Contract,Bool)

sử dụng số slot hiện tại và đồng thời kiểm tra xem đầu vào có hợp lý không và các khoản thanh toán có nằm trong giới hạn đã cam kết hay không; nếu đầu vào hợp lệ thì nó trả về State và Contract và Boolean True mới; nếu không, nó trả về State và Contract hiện tại, không thay đổi, cùng với giá trị False.

Chi tiết hơn một chút, trong loại đánh giá ở trên, Input là sự kết hợp của các hành động của người tham gia hợp đồng (tức là Commit, Pay, Redeem), các giá trị Oracles và các lựa chọn đã thực hiện. Hai tham số Ada là giá trị hợp đồng hiện tại và giá trị hợp đồng kết quả. Vì vậy, ví dụ: nếu hợp đồng thực hiện Thanh toán 20 Ada và số tiền hiện tại đầu vào là 100 Ada, thì giá trị kết quả sẽ là 80 Ada. Các giá trị Contract và State tương ứng là hợp đồng hiện tại và State của nó, được lấy từ tập lệnh dữ liệu.

Nói chung, mã on-chain không thể tạo đầu ra giao dịch mà chỉ có thể xác thực bất kỳ thứ gì người dùng cung cấp trong giao dịch. Mỗi bước trong quá trình đánh giá hợp đồng được tạo bởi người dùng, theo cách thủ công hoặc tự động (bằng ví chẳng hạn) và được xuất bản dưới dạng giao dịch. Do đó, người dùng có thể cung cấp bất kỳ Contract và State của nó dưới dạng phần tiếp theo. Ví dụ, xem xét hợp đồng sau

Commit id Alice 100 (Both (Pay Alice to Bob 30 Ada) (Pay Alice to Charlie 70 Ada))

Alice cam kết 100 Ada và sau đó cả Bob và Charlie có thể thu 30 và 70 Ada mỗi người bằng cách phát hành giao dịch có liên quan. Sau khi Alice đã đưa ra cam kết, hợp đồng sẽ trở thành

Both (Pay Alice to Bob 30 Ada) (Pay Alice to Charlie 70 Ada)

Bob hiện có thể phát hành giao dịch với đầu vào Pay trong tập lệnh Redeemer và đầu ra tập lệnh có giá trị ít hơn 30 Ada, được bảo vệ bởi tập lệnh trình xác thực Marlowe và với tập lệnh dữ liệu chứa hợp đồng tiếp tục được đánh giá

Pay Alice to Charlie 70 Ada

Charlie sau đó có thể thực hiện một giao dịch tương tự để nhận 70 Ada còn lại.

Đảm bảo hiệu lực thi hành. Nhìn lại ví dụ này, giả sử thay vào đó Bob chọn một cách ác ý để phát hành một giao dịch với phần tiếp theo sau:

Pay Alice to Bob 70 Ada

và lấy hết tiền, như ở đây, khiến Charlie thất vọng một cách hợp lý với tất cả những hợp đồng thông minh đó.

Để tránh điều này, chúng ta phải đảm bảo rằng hợp đồng tiếp tục mà chúng ta đánh giá là bằng với hợp đồng trong tập lệnh dữ liệu của đầu ra giao dịch.

Đây là phần phức tạp trong quá trình triển khai, bởi vì chúng ta chỉ có băm của tập lệnh dữ liệu của đầu ra giao dịch có sẵn trong quá trình thực thi tập lệnh trình xác thực. Nếu chúng ta có thể truy cập trực tiếp vào tập lệnh dữ liệu, chúng ta có thể chỉ cần kiểm tra xem hợp đồng dự kiến ​​có bằng với hợp đồng được cung cấp hay không. Nhưng điều đó sẽ làm phức tạp thêm mọi thứ, bởi vì chúng ta sẽ cần biết các loại của tất cả các tập lệnh dữ liệu trong một giao dịch, điều này nói chung là không thể.

Mẹo nhỏ là yêu cầu input redeemer script và output data script phải bằng nhau. Cả tập lệnh Redeemer và tập lệnh dữ liệu đều có cấu trúc giống nhau, cụ thể là một cặp (Input, MarloweData) trong đó

• Đầu vào chứa các hành động hợp đồng (tức là các giá trị Pay, Redeem), Choice và Oracle.
• MarloweData chứa Contract còn lại và State của nó.
• State ở đây là tập hợp Commit cộng với tập hợp Choice được thực hiện.

Để chi tiêu một đầu ra giao dịch được bảo đảm bởi tập lệnh trình xác thực Marlowe, người dùng phải cung cấp tập lệnh Redeemer, là một bộ của Input và đầu ra dự kiến ​​của việc diễn giải hợp đồng Marlowe cho Input đã cho, tức là a Hợp đồng, Bang cặp. Hợp đồng và trạng thái dự kiến ​​có thể được đánh giá chính xác trước bằng chức năng eval.

Để đảm bảo rằng người dùng cung cấp Contract và State hợp lệ còn lại, tập lệnh trình xác thực Marlowe sẽ so sánh hợp đồng và trạng thái được đánh giá với hợp đồng và trạng thái do người dùng cung cấp, đồng thời sẽ từ chối giao dịch nếu chúng không khớp. Để đảm bảo rằng tập lệnh dữ liệu của hợp đồng còn lại có cùng Contract và State như đã được thông qua với tập lệnh Redeemer, chúng ta kiểm tra xem hàm băm tập lệnh dữ liệu có giống với hàm băm của tập lệnh Redeemer hay không.

Hoàn thành. Khi một hợp đồng được đánh giá là Null và tất cả các số tiền Commit đã hết hạn được đổi, khoản ký gửi hợp đồng ban đầu có thể được chi tiêu, loại bỏ hợp đồng khỏi tập hợp các đầu ra giao dịch chưa chi tiêu.

Bài tập

Nâng cao. Khám phá các hợp đồng Marlowe đang chạy trong Plutus. Để có thể thực hiện việc này, bạn cần sử dụng phiên bản mới nhất của Marlowe, thay vì v1.3.

---