Trong loạt blog kỹ thuật không thường xuyên dành cho Nhà phát triển của chúng tôi, chúng tôi mời các nhà nghiên cứu và kỹ sư của IOHK thảo luận về công việc và thông tin chi tiết mới nhất của họ.

Marlowe là ngôn ngữ dành riêng cho miền dành cho các hợp đồng thông minh tài chính an toàn đang được IOHK phát triển cho các khả năng Goguen của chuỗi khối Cardano. Tiếp theo bài đăng giới thiệu của tôi trên Marlowe , trong bài đăng Deep Dive này, chúng ta sẽ xem xét chi tiết về ngôn ngữ và các cách khác nhau để viết hợp đồng thông minh Marlowe khi chúng ta chuyển sang kỷ nguyên tài chính phi tập trung (DeFi). Sau khi giải thích cách tiếp cận của chúng tôi đối với oracles, nhập thông tin ‘thế giới thực’ vào một hợp đồng đang chạy, chúng tôi xem Tiêu chuẩn thống nhất các loại hợp đồng thuật toán ( Actus ) cho các hợp đồng tài chính và giải thích cách chúng tôi đã thực hiện đổi mới này trong Marlowe.

Tóm lại Marlowe

Marlowe là một ngôn ngữ nhỏ, với một số cấu trúc, đối với mỗi hợp đồng, mô tả hành vi liên quan đến một nhóm vai trò cố định, hữu hạn .

  • Một hợp đồng đang chạy có thể thực hiện thanh toán cho một vai trò hoặc cho một khóa công khai.
  • Theo một cách bổ sung, hợp đồng có thể chờ một hành động của một trong các vai trò, chẳng hạn như đặt cọc tiền tệ hoặc lựa chọn từ một tập hợp các tùy chọn. Điều quan trọng là, một hợp đồng không thể chờ vô thời hạn: nếu không có hành động nào được bắt đầu trong một thời gian nhất định ( thời gian chờ ), thì hợp đồng sẽ tiếp tục với một hành vi khác, chẳng hạn như hoàn trả bất kỳ khoản tiền nào trong hợp đồng.
  • Tùy thuộc vào trạng thái hiện tại của hợp đồng, nó có thể đưa ra lựa chọn giữa hai hướng hành động trong tương lai, bản thân chúng là hợp đồng.
  • Khi không cần thực hiện thêm hành động nào nữa, hợp đồng sẽ đóng và mọi đơn vị tiền tệ còn lại trong hợp đồng sẽ được hoàn lại.

Khi một hợp đồng được chạy, các vai trò mà nó liên quan được thực hiện bởi những người tham gia , đó là danh tính trên blockchain. Mô hình này cho phép một vai trò được chuyển giao trong quá trình thực hiện hợp đồng, để các vai trò trong một hợp đồng đang chạy có thể được giao dịch . Mỗi vai trò được đại diện bởi một mã thông báo trên chuỗi và việc chuyển giao này sẽ chuyển khả năng thực hiện các hành động của vai trò. Tiếp tục điều này, chúng tôi có thể đại diện cho một vai trò duy nhất với nhiều mã thông báo, do đó cho phép vai trò được chia sẻ: điều này có thể được gọi là ‘chứng khoán hóa’.

Hệ thống Marlowe

Chúng tôi đã cố tình chọn làm cho ngôn ngữ đơn giản nhất có thể để dễ dàng triển khai trên Cardano và trong Sân chơi Marlowe. Marlowe mô tả luồng tiền điện tử giữa những người tham gia và để điều này được triển khai trên thực tế trên chuỗi khối Cardano, mã phải được thực thi cả trên chuỗi và ngoài chuỗi: tuy nhiên, hãy nhớ rằng chỉ một hợp đồng Marlowe mô tả cả hai phần. Phần trên chuỗi chấp nhận và xác thực các giao dịch tuân theo các yêu cầu của hợp đồng thông minh: phần này được triển khai dưới dạng một tập lệnh Plutus duy nhất cho tất cả các hợp đồng Marlowe, với hợp đồng Marlowe cụ thể bao gồm một dữ liệu được chuyển qua các giao dịch. Ngoài chuỗi, hợp đồng Marlowe sẽ được trình bày qua giao diện người dùng và ví, cung cấp hoặc thực sự là tự động hóa các khoản tiền gửi và lựa chọn cũng như nhận các khoản thanh toán bằng tiền điện tử.

Hình 1. Sân chơi Marlowe mô phỏng cách thức hoạt động của các hợp đồng

Trong Playground, chúng tôi có thể mô phỏng hành vi hợp đồng, để người dùng tiềm năng có thể thực hiện các cách khác nhau mà hợp đồng sẽ phát triển, tùy theo các hành động khác nhau mà người tham gia thực hiện. Trong mô phỏng chính, Hình 1, người dùng có quan điểm toàn diện và có thể thực hiện các hành động bởi bất kỳ người tham gia nào, với tùy chọn tại mỗi điểm để hoàn tác các hành động đã thực hiện và sau đó đi theo một con đường khác. Các  mô phỏng cho phép người dùng xem hành vi từ góc độ một đặc biệt của người tham gia, do đó mô phỏng cách người dùng sẽ tương tác với các hợp đồng chạy khi nó được triển khai trên các blockchain.

Sự đơn giản này cũng giúp chúng ta có thể lập mô hình các hợp đồng Marlowe trong bộ giải SMT , một hệ thống logic để tự động kiểm tra các thuộc tính của hệ thống. Sử dụng mô hình này, chúng tôi gọi là phân tích tĩnh , đối với mỗi hợp đồng, chúng tôi có thể kiểm tra xem liệu nó có thể không thực hiện được khoản thanh toán hay không và nếu hợp đồng có thể thất bại, chúng tôi lấy bằng chứng về việc nó không thành công như thế nào, giúp tác giả viết lại hợp đồng nếu họ muốn.

Chúng tôi có thể xây dựng một mô hình chính thức về việc triển khai của chúng tôi trong một trợ lý chứng minh , trong đó chúng tôi có thể tạo ra các bằng chứng được kiểm tra bằng máy về cách ngôn ngữ hoạt động. Trong khi trình giải quyết SMT hoạt động cho các hợp đồng riêng lẻ, trợ lý bằng chứng có thể chứng minh các thuộc tính của các mẫu hợp đồng, cũng như bản thân hệ thống: ví dụ: chúng tôi có thể cho thấy rằng trong bất kỳ hợp đồng đang chạy nào, các tài khoản mà nó tham chiếu không bao giờ được ghi nợ. Mô phỏng, phân tích tĩnh và bằng chứng cung cấp các mức độ đảm bảo bổ sung cho một hợp đồng mà người dùng sẽ cam kết tài sản để đảm bảo rằng hợp đồng hoạt động như bình thường.

Viết hợp đồng Marlowe

Chúng ta đã thấy các hợp đồng Marlowe có thể được phân tích theo nhiều cách khác nhau, nhưng làm thế nào để các tác giả thực sự viết các hợp đồng thông minh trong Marlowe? Sân chơi cung cấp một số cách tạo hợp đồng Marlowe. Người dùng có thể viết Marlowe trực tiếp, nhưng người mới bắt đầu thường chọn xây dựng hợp đồng một cách trực quan, sử dụng trình chỉnh sửa Blockly tương tác. Hình 2 cho thấy một phần của hợp đồng ký quỹ.

Hình 2. Một hợp đồng ký quỹ trong trình chỉnh sửa Blockly tương tác của Playground

Làm việc trong trình chỉnh sửa trực quan này có lợi thế là hiển thị tất cả các tùy chọn khi bạn chọn cách điền vào một phần của hợp đồng đang được phát triển. Ngoài ra, bạn có thể phát triển các hợp đồng trong Haskell, vì Marlowe DSL trên thực tế đã được nhúng trong Haskell. Hình 3 cho thấy hợp đồng tương tự trong Haskell: các phần màu xanh lam và màu tím là Marlowe, và các thành phần màu đen được xác định trong Haskell, là chữ viết tắt làm cho hợp đồng tổng thể dễ đọc hơn. Cách tiếp cận này cho phép người dùng xây dựng hợp đồng thông minh từng bước từ các thành phần. Trong đoạn mã hiển thị trong Hình 3, mỗi vai trò, Alice và Bob, được yêu cầu đưa ra lựa chọn: nếu lựa chọn của họ phù hợp, họ đồng ý và hợp đồng tiến hành theo một chiều; nếu không, thì người tham gia thứ ba, Carol, được yêu cầu phân xử giữa họ. Các hợp đồng thỏa thuậnvà phân xử trọng tài được xác định sau này trong tệp Haskell.

Hình 3. Hợp đồng ký quỹ trong Haskell

Người dùng cũng sẽ có thể viết các hợp đồng thông minh tài chính của họ bằng JavaScript, trong khi vẫn tận hưởng tất cả các lợi thế của phân tích, mô phỏng và bằng chứng, như được cung cấp bởi triển khai Marlowe.

Oracles

Một trong những câu hỏi đầu tiên mà chúng tôi nhận được khi mô tả Marlowe là về các kỳ tích tài chính hoặc cách chúng tôi có thể có được hợp đồng để tính đến các giá trị dữ liệu bên ngoài, chẳng hạn như tỷ giá hối đoái giữa ada và bitcoin. Tóm lại, một nhà tiên tri giống như một người tham gia đưa ra lựa chọn, và do đó ngữ nghĩa của Marlowe đã có thể xử lý các giá trị bên ngoài. Tuy nhiên, chúng tôi có kế hoạch hỗ trợ các giá trị tiên tri như một phần của việc triển khai, cho phép các hợp đồng truy cập giá trị trực tiếp từ mã thị trường chứng khoán hoặc nguồn cấp dữ liệu như Coinbase. Đồng thời, nhóm Plutus đang nghiên cứu cách tốt nhất để đối phó với oracles nói chung và chúng tôi có thể mong đợi sự hỗ trợ cho điều đó trong thời gian thích hợp, mặc dù có thể không có trong bản phát hành đầy đủ đầu tiên của Marlowe và Khung ứng dụng Plutus.

Actus cho các hợp đồng tài chính

Marlowe có tiềm năng mang đến cho mọi người cơ hội thực hiện các cam kết tài chính và giao dịch mà không cần bên thứ ba tạo điều kiện: blockchain đảm bảo rằng hợp đồng được tuân thủ.

Chúng tôi đang xây dựng việc triển khai Marlowe các hợp đồng không qua trung gian để cung cấp cho người dùng cuối muốn thực hiện các giao dịch tài chính ngang hàng trực tiếp mà không có sự can thiệp của bất kỳ bên thứ ba nào.

Tổ chức Nghiên cứu Tài chính Actus phân loại các hợp đồng tài chính bằng phương pháp phân loại được mô tả trong đặc tả kỹ thuật chi tiết .

Actus dựa trên sự hiểu biết rằng các hợp đồng tài chính là các thỏa thuận pháp lý giữa hai (hoặc nhiều) đối tác về việc trao đổi các dòng tiền trong tương lai. Về mặt lịch sử, các thỏa thuận pháp lý như vậy được mô tả bằng ngôn ngữ tự nhiên, dẫn đến sự mơ hồ và đa dạng giả tạo. Để phản hồi, Actus định nghĩa hợp đồng bằng một tập hợp các điều khoản hợp đồng và các chức năng xác định ánh xạ các điều khoản này với các nghĩa vụ thanh toán trong tương lai. Qua đó, có thể mô tả hầu hết các công cụ tài chính thông qua 31 loại hợp đồng hoặc mẫu mô-đun.

Tiếp theo, chúng tôi xem xét một ví dụ đơn giản và sau đó chúng tôi giải thích cách tiếp cận đầy đủ của chúng tôi để triển khai Actus, với các cách tiếp cận bổ sung cung cấp các ưu và nhược điểm khác nhau.

Ví dụ về Actus đầu tiên

Trái phiếu không phiếu giảm giá là một chứng khoán nợ không trả lãi (phiếu giảm giá) nhưng được phát hành với giá chiết khấu, tạo ra lợi nhuận khi đáo hạn khi trái phiếu được mua lại cho đủ mệnh giá của nó.

Ví dụ, Hình 4 mô tả một hợp đồng theo đó một nhà đầu tư có thể mua một trái phiếu có giá 1.000 suất với chiết khấu 15%. Cô ấy trả 850 suất cho công ty phát hành trái phiếu trước thời gian bắt đầu, ở đây là vị trí số 10.

Sau đó, sau ngày đáo hạn, vị trí 20 tại đây, nhà đầu tư có thể đổi trái phiếu lấy toàn bộ giá trị danh nghĩa của nó, tức là 1.000 lovelaces.

Hình 4. Hợp đồng trái phiếu không coupon với chiết khấu 15%

Hợp đồng này có một nhược điểm đáng kể. Khi nhà đầu tư đã đặt cọc 850 suất, nó sẽ được thanh toán ngay cho công ty phát hành; nếu nhà đầu tư không đầu tư đủ nhanh, tức là trước khi hết thời gian, hợp đồng kết thúc. Sau đó, hai kết quả có thể xảy ra:

  • nhà phát hành gửi 1.000 suất vào tài khoản của nhà đầu tư và số tiền đó ngay lập tức được thanh toán đầy đủ cho nhà đầu tư;
  • Nếu chủ đầu tư không đặt cọc thì hợp đồng đóng và hoàn trả hết tiền trong hợp đồng, nhưng đến thời điểm này không có tiền trong hợp đồng nên chủ đầu tư mất tiền.

Làm thế nào chúng ta có thể tránh được vấn đề vỡ nợ của công ty phát hành trái phiếu? Có ít nhất hai cách để giải quyết vấn đề này: chúng tôi có thể yêu cầu công ty phát hành đặt cọc toàn bộ số tiền trước khi hợp đồng bắt đầu, nhưng điều đó sẽ đánh bại đối tượng phát hành trái phiếu ngay từ đầu. Thực tế hơn, chúng tôi có thể yêu cầu một bên thứ ba làm người bảo lãnh cho thỏa thuận, như được trình bày ở đây.

Hình 5. Cải thiện hợp đồng với người bảo lãnh

Các hành động trong Marlowe

Các sản phẩm trong phân loại Actus, chẳng hạn như hợp đồng gốc khi đáo hạn, có thể được trình bày theo nhiều cách khác nhau trong Marlowe, tùy theo mức độ mà họ có thể chấp nhận các thay đổi đối với các điều khoản của mình trong suốt thời hạn hợp đồng (Hình 6).

Hình 6. Phân loại Actus và Marlowe

Trong trường hợp đơn giản nhất, tất cả các dòng tiền đều được thiết lập hoặc đóng băng khi bắt đầu hợp đồng, do đó hoàn toàn có thể dự đoán được cách thức hoạt động của hợp đồng, giả sử rằng tất cả những người tham gia tiếp tục gắn bó với hợp đồng trong suốt thời gian tồn tại của nó. Hợp đồng kiểu này chúng tôi gọi là Actus-F (cố định hoặc đóng băng).

Động lực – đó là sự thay đổi trong quá trình phát triển hợp đồng – có thể xảy ra theo hai cách. Người tham gia có thể thực hiện các khoản thanh toán đột xuất yêu cầu tính toán lại các dòng tiền còn lại, và dòng tiền cũng có thể được sửa đổi bằng cách tính đến các yếu tố rủi ro bên ngoài . Tính tổng quát đầy đủ của các hợp đồng thực hiện cả hai đều được mô hình hóa trong Actus-M (cho Marlowe).

Cũng có các cấp độ trung gian: Actus-FS lập mô hình lịch trình cố định: cho phép tính đến các yếu tố rủi ro nhưng không có khoản thanh toán đột xuất; ngược lại, hợp đồng Actus-FR cho phép thực hiện thanh toán ở những điểm không mong muốn, nhưng không tính đến bất kỳ yếu tố rủi ro nào.

Cuối cùng, di chuyển ra ngoài Marlowe, Actus-H (H cho Haskell) lập mô hình hợp đồng trực tiếp dưới dạng các chương trình trong Plutus hoặc Haskell, sử dụng Marlowe để xác thực từng giao dịch trong thời hạn hợp đồng bằng cách tạo mã Plutus từ mô tả lôgic hợp đồng của Marlowe.

Tại sao chúng tôi cung cấp các mẫu hợp đồng Actus khác nhau này? Lý do là có sự đánh đổi giữa bản chất năng động của hợp đồng và sự đảm bảo mà chúng tôi có thể cung cấp cho người dùng về cách các hợp đồng sẽ thực hiện trước khi thực hiện hợp đồng.

  • Các hợp đồng Actus-F trình bày một lịch trình thanh toán hoàn toàn cố định, những người tham gia có thể trực tiếp xem xét kỹ lưỡng để có thể dễ dàng nhận thấy rằng tất cả các khoản thanh toán từ một hợp đồng như vậy sẽ thành công.
  • Các hợp đồng Actus-FS và -FR thể hiện tính năng động hơn, nhưng các hợp đồng này dễ đọc và dễ xem xét kỹ lưỡng. Hơn nữa, họ phải phân tích tĩnh (chậm hơn) để thiết lập, ví dụ, rằng tất cả các khoản thanh toán sẽ thành công.
  • Các hợp đồng Actus-M được thể hiện trong Marlowe, và do đó có thể được phân tích. Tuy nhiên, phân tích về cơ bản chậm hơn đáng kể do không thể đoán trước được các hành động mà hợp đồng sẽ thực hiện tại bất kỳ thời điểm cụ thể nào. Lưu ý rằng đảm bảo có thể được cung cấp cho các phiên bản thu nhỏ của hợp đồng, có cùng nội dung tính toán, nhưng phát triển trong thời gian ngắn hơn, do đó có ít tương tác hơn.
  • Các hợp đồng Actus-H được viết bằng sự kết hợp của Plutus và Marlowe, và do đó, không thể kiểm tra tĩnh theo cách tương tự như các hợp đồng khác. Tuy nhiên, nền tảng này cung cấp cho khách hàng doanh nghiệp khả năng mở rộng đầy đủ và điều chỉnh việc thực hiện tiêu chuẩn Actus.

Trong quá trình triển khai Actus của chúng tôi, có sẵn dưới dạng phiên bản phát hành trước trong tab Labs của Playground , người dùng có thể tạo các hợp đồng Actus-F và -FS từ các điều khoản của hợp đồng, bằng cách sử dụng bản trình bày trực quan về dữ liệu được yêu cầu.

Hình 7. Ba mục có dấu hoa thị được yêu cầu đối với hợp đồng gốc khi đáo hạn

Đối với hợp đồng gốc khi đáo hạn, cần có ba mục: ngày bắt đầu và ngày kết thúc, và số tiền danh nghĩa của hợp đồng (do đó các mục được gắn dấu sao trong mẫu). Một hợp đồng như vậy sẽ bao gồm một tải đơn giản, trong đó số tiền danh nghĩa được chuyển từ bên đối tác sang bên khi bắt đầu hợp đồng và theo hướng ngược lại vào ngày đáo hạn.

Thêm các mục bổ sung sẽ thay đổi hợp đồng đã tạo cho phù hợp. Trong Hình 7, bên này sẽ phải chuyển khoản tiền bảo hiểm cộng với phí bảo hiểm cho bên đối tác vào ngày đáo hạn, do đó tạo động lực cho bên đối tác thực hiện khoản vay ngay từ đầu.

Chuyển sang thế giới DeFi với các hợp đồng thông minh

Như chúng ta đã thấy, các chuyên gia tài chính và nhà phát triển hiện có cách để bắt đầu tạo các hợp đồng thông minh tài chính trực tiếp trong Haskell hoặc Marlowe thuần túy, hoặc trực quan bằng cách sử dụng Sân chơi Marlowe , tùy thuộc vào chuyên môn lập trình của họ. Trong Playground, bạn có thể mô phỏng và phân tích các hợp đồng bạn tạo để kiểm tra xem chúng hoạt động bình thường và sẵn sàng được phát hành vào thế giới tài chính phi tập trung khi giai đoạn Goguen của Cardano được triển khai. Nhóm Marlowe của IOHK sẽ tiếp tục triển khai các ví dụ từ tiêu chuẩn Actus, khi chúng tôi chuẩn bị hoàn thiện việc triển khai Marlowe trên Cardano và đưa các hợp đồng thông minh tài chính vào chính blockchain.