Di chuyển từ các phiên bản trước đó của Marlowe

Hướng dẫn này giải thích phiên bản mới nhất của Marlowe khác với các phiên bản ngôn ngữ trước đó như thế nào.

Bỏ Both

Chúng tôi không bao gồm một cấu trúc Both trong phiên bản Marlowe mới nhất, cấu trúc này làm cho tất cả các hợp đồng có trình tự.

Vì không có phiên bản nào của Marlowe có giao tiếp giữa các chi nhánh của Bothnên chức năng bổ sung duy nhất được cung cấp Bothtrên thực tế là khả năng đợi nhiều khoản tiền gửi cùng một lúc.

Chúng tôi cải thiện chức năng này bằng cách cập nhật cấu trúc When. Thay vì để các nhánh khác nhau chờ các đầu vào khác nhau, chúng ta chuyển sang một mô hình hoàn toàn tuần tự và đồng bộ, nơi chúng ta có thể chờ một trong một số đầu vào có thể cùng một lúc (như trong select).

Lý do chúng tôi loại bỏ cấu trúc này là các chương trình tuần tự dễ phân tích hơn và dễ lý luận hơn, vì không cần đồng bộ hóa và không có cơ hội cho các race conditions.

Bao gồm các tài khoản

Trong các phiên bản Marlowe trước đó, mỗi cam kết có thời gian chờ riêng. Điều này có nghĩa là tiền được ký gửi trong một hợp đồng không thể thay thế được , bởi vì nó có thể được phân biệt bằng thời gian chờ của nó. Để đạt được khả năng thay thế, chúng tôi đã loại bỏ thời gian chờ khỏi các cấu trúc riêng lẻ và có một thời gian chờ duy nhất cho tất cả các cam kết. Thời hạn hợp đồng này có thể suy ra đơn giản từ thời gian chờ trong hợp đồng.

Tuy nhiên, chúng tôi bao gồm các tài khoản (accounts) để tổ chức số tiền được gửi vào hợp đồng. Điều này giúp minh bạch hơn cách tiền luân chuyển trong hợp đồng và đặc biệt xác định tiền sẽ được hoàn trả (refunded) cho ai khi hợp đồng chấm dứt.

Mỗi tài khoản được xác định bởi một người tham gia; người tham gia cho biết ai sẽ nhận được tiền trong tài khoản theo mặc định khi Closeđạt được.

Lý do chúng tôi chọn bao gồm các tài khoản là vì không có chúng, chúng tôi nhận thấy rằng về cơ bản chúng tôi đang theo dõi các tài khoản theo cách thủ công. Ngoài ra, trong mỗi lá của AST, chúng tôi thấy mình phải tính toán xem chúng tôi phải trả lại bao nhiêu cho mỗi người tham gia, làm lộn xộn cái cây với “boilerplate” lặp đi lặp lại. Do đó, việc tổ chức tiền trong tài khoản có thể làm cho các hợp đồng dễ dàng lập luận hơn và ít bị sai sót hơn.

Lưu ý rằng chúng tôi có thể cung cấp đầy đủ khả năng thay thế bằng cách sử dụng một tài khoản. Chúng ta chỉ cần viết các Paylệnh thích hợp trong các lá của hợp đồng. Nếu tất cả tiền được trả cho người tham gia, thì Closekhông có hiệu lực. 1

Thảo luận: Tài khoản ẩn và tài khoản rõ ràng

Nhiều trường hợp sử dụng cho tài khoản - và tất cả những trường hợp mà chúng tôi có thể xác định cho hợp đồng ACTUS - có một tài khoản cho mỗi người tham gia và một người tham gia cho mỗi tài khoản (“mô hình 1-1”). Điều này đặt ra câu hỏi liệu chúng ta có nên xử lý ngầm các tài khoản hay không, với mỗi người tham gia sở hữu một tài khoản.

Mặt khác, có nhiều tình huống hợp lý cho các tài khoản không tuân theo mô hình 1-1.

Ví dụ khi nhiều người tham gia sử dụng một tài khoản.

• Alice sở hữu một tài khoản mà cô ấy cam kết chi tiền cho Bob (hãy nghĩ Alice là chủ của Bob). Bob có thể chi tiêu đến giới hạn trong tài khoản, nhưng sau khi hết thời gian cam kết, Alice sẽ thu hồi bất cứ thứ gì còn lại.

• Alice sở hữu một tài khoản mà cô ấy cam kết chi tiền cho Bob và Carol (hãy nghĩ Alice là chủ của Bob và Carol). Họ có thể chi tiêu (cùng nhau) đến giới hạn trong tài khoản, nhưng sau khi hết thời gian cam kết, Alice thu hồi bất cứ thứ gì còn lại.

• Mặt khác, mỗi người có thể được cấp một tài khoản riêng để chi tiêu: điều đó sẽ thực thi các giới hạn riêng lẻ cũng như giới hạn tổng hợp.

• Nếu Bob [và Carol] muốn tiêu tiền, họ cũng có thể thêm tiền vào tài khoản, nhưng họ nên nhận ra rằng bất cứ thứ gì không sử dụng sẽ được hoàn lại cho Alice.

Ví dụ về nhiều tài khoản cho một người:

• Ví dụ về bảo lãnh phát hành sẽ phù hợp ở đây. Một người chấp nhận rủi ro cấp độ một và rủi ro cấp độ thứ hai bằng cách sử dụng các tài khoản khác nhau. Chỉ khi bảo lãnh phát hành cấp một của tất cả những người tham gia được chi tiêu thì chi tiêu cấp hai mới xảy ra.

Closethay thế Null/Pay

Vì tất cả các hợp đồng bây giờ là tuần tự, chúng ta có thể dễ dàng biết khi nào một hợp đồng chấm dứt, tức là: khi nào thì chỉ Nullcòn lại. Chúng tôi sử dụng cơ hội này để đóng hợp đồng và hoàn trả bất kỳ khoản tiền nào còn lại trong tài khoản; vì lý do này, chúng tôi đã đổi tên thành Null thànhClose (giúp dễ hiểu).

Như đã lưu ý trước đó, không còn thời gian chờ rõ ràng nào trong các tài khoản nữa, vì tất cả các hợp đồng cuối cùng sẽ giảm xuống Close. Trên thực tế, chúng ta có thể tính toán giới hạn trên một cách tĩnh và hiệu quả cho thời điểm điều này xảy ra, làm cho khía cạnh này của Marlowe có thể phân tích được.

Pay

Paybây giờ là ngay lập tức và nó có một phần tiếp theo và ít tham số hơn. 2 Nó cho phép thanh toán từ một tài khoản cho một người tham gia hoặc đến một tài khoản khác. Chúng tôi đã loại bỏ PayAll, vì nó có thể được mô phỏng dưới dạng một chuỗi hữu hạn Pay. Trên thực tế, chúng ta có thể định nghĩa payAllnhư một hàm Haskell (xem zeroCouponBondví dụ).

Đó là hệ quả của việc loại bỏ Bothcấu trúc, đó là bây giờ nó không rõ ràng mà Payđi trước: tất cả chúng đều tuần tự, do đó hỗ trợ phân tích. Với Bothcấu trúc, chúng tôi có thể có khả năng Paysxảy ra theo bất kỳ thứ tự nào (vì cả hai bên của Bothđược cho là chạy đồng thời).

Multi-clause When

Chúng tôi đã sửa đổi Whenđể bao gồm một tập hợp các hành động khả thi có thể được nhập vào trong khi Whenchờ đợi. Chúng tôi gọi cách tiếp cận này là “Một trong nhiều”, bởi vì nó chấp nhận một hành động trong số nhiều hành động được phép tiềm năng. Whenvẫn như sau:

When [Case] Timeout Contract

Whensẽ đợi Timeoutvà tiếp tục ở đâu Contract, hoặc tiếp tục như được chỉ định trong một trong các Casesđiều kiện nào xảy ra trước. Caseđược định nghĩa là:

data Case = Case Action Contract

và Actionnhư:

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

Một Casemệnh đề sẽ chỉ được kích hoạt nếu điều tương ứng Action được tạo ra và nó sẽ tiếp tục như vậy Contract. Trong trường hợp có hai Actionskết quả khớp, cái đầu tiên trong danh sách sẽ được thực thi.

Ba loại hành động được hỗ trợ:

• Depositđại diện cho một khoản tiền gửi vào tài khoản; cái này ban đầu được gọi Commit.

• Choiceđại diện cho sự lựa chọn được thực hiện bởi một người tham gia từ bên trong một tập hợp các Integergiá trị (được chỉ định bởi danh sách Bounds).

• Notifysẽ đợi một Notifyhành động được đưa ra khi Observationđúng. Chúng tôi gọi nó là Notifyđể làm rõ rằng chúng tôi không thể chỉ chờ đợi Observationsmà phải có ai đó kích hoạt hợp đồng trong một thời điểm khi giá trị Observationlà sự thật.

Chúng tôi đã loại bỏ việc bổ sung các quan sát vào Depositvà Choice vì sẽ không rõ ràng liệu Observationsẽ được đánh giá trước hay sau khi áp dụng hành động.

Ngoài các trường hợp rõ ràng trong When, chúng ta phải nhớ rằng nhánh thời gian chờ cũng là một trường hợp và nó cũng cần được kích hoạt (tương tự như Notify). 3 4

Quan sát và Giá trị

Chúng tôi đã loại bỏ Observationsvà Valuesđiều đó có thể được thể hiện bằng cách kết hợp những thứ khác: như chung AvailableMoney(cho toàn bộ hợp đồng) hoặc tương tự DepositedMoneyBy, ghi nhớ số tiền mà người tham gia đã ký gửi, vì hợp đồng có thể được cấu trúc lại để tuân theo điều đó và hỗ trợ sẽ yêu cầu thông tin bổ sung trong trạng thái (tính đơn giản).

Chúng tôi đã giữ lại ChoseSomethingquan sát, mặc dù, trong ngữ nghĩa được đề xuất, mọi sự xuất hiện của ChoseSomethingcó thể được đánh giá tĩnh và hiệu quả bằng cách kiểm tra ngữ cảnh của nó.

Ví dụ: trong hợp đồng sau, chúng ta có thể thấy rằng lần xuất hiện đầu tiên của ChoseSomethingsẽ đánh giá Truevà lần xuất hiện thứ hai là False:

When [ Case (Choice (ChoiceId 1 Alice) [(1,1)])
            (If (ChoseSomething (ChoiceId 1 Alice))
                Close
                Close)
     , Case (Choice (ChoiceId 2 Bob) [(2,2)])
            (If (ChoseSomething (ChoiceId 1 Alice))
                Close
                Close)]
     0
     Close

Tuy nhiên, chúng tôi đã chọn giữ nguyên cấu trúc vì hai lý do:

• Nó cho phép mã tái sử dụng (tiện lợi). Ví dụ, trong hợp đồng trước, chúng ta có thể xác định chosen1:

let chosen1 = If (ChoseSomething (ChoiceId 1 1))
                 Close
                 Close
in
When [ Case (Choice (ChoiceId 1 1) [(1,1)])
            chosen1
     , Case (Choice (ChoiceId 2 2) [(2,2)])
            chosen1]
     0
     Close

Nhưng điều này sẽ không thể thực hiện được nếu chúng ta không có cấu trúc ChoseSomething, vì giá trị mà nó giảm phụ thuộc vào ngữ cảnh.

• Có thể không còn xảy ra trường hợp các lần xuất hiện của cấu trúc có thể được đánh giá tĩnh nếu chúng ta mở rộng Whencấu trúc để hỗ trợ “nhiều trong số nhiều” đầu vào.

Bao gồm các khoảng thời gian

Đặc tả EUTxO cung cấp các tập lệnh xác thực với khoảng thời gian thay vì với số vị trí. Điều này là để thúc đẩy thuyết xác định trong các tập lệnh xác thực. Tuy nhiên, chúng tôi đã giữ thời gian chờ của When (thời gian chờ duy nhất) dưới dạng một dấu thời gian duy nhất mặc dù nó hiện được biểu thị bằng thời gian POSIX. Cách chúng tôi xử lý các khoảng thời gian là yêu cầu khoảng thời gian của một giao dịch không bao gồm bất kỳ khoảng thời gian nào mà ngữ nghĩa phải lựa chọn. Ví dụ: nếu thời gian chờ là trưa ngày 3 tháng 1, giao dịch trong khoảng thời gian từ ngày 2 tháng 1 đến ngày 4 tháng 1 sẽ không thành công với AmbiguousTimeInterval. Người tham gia sẽ phải thực hiện một giao dịch trong khoảng thời gian từ ngày 2 tháng 1 đến một giây trước buổi trưa hoặc một giây từ trưa ngày 3 tháng 1 đến ngày 4 (hoặc cả hai).

Tuy nhiên, đối với Giá trị, chúng tôi cung cấp hai cấu trúc TimeIntervalStart và TimeIntervalEnd. Một giải pháp thay thế để xem xét sẽ là sửa đổi ngữ nghĩa để Giá trị không mang tính xác định, theo cách đó chúng ta có thể bao gồm cấu trúc CurrentTime và chỉ làm mất hiệu lực của các giao dịch không rõ ràng, nhưng điều này sẽ làm phức tạp ngữ nghĩa và làm cho chúng khó dự đoán hơn.

[1] Chúng tôi có thể cung cấp một cách phân tích tĩnh hợp đồng để kiểm tra xem liệu có thể còn tiền trong bất kỳ tài khoản nào khi đến thời điểm Close hay không.

[2] Điều này có nghĩa là các khoản thanh toán hiện tuân theo mô hình “đẩy” thay vì mô hình “kéo”.

[3] Tuy nhiên, việc kích hoạt hợp đồng để xử lý thời gian chờ không phải là khẩn cấp Notifyvì mặc dù Observationscó thể xen kẽ giữa Truevà False, thời gian chờ chỉ có thể xảy ra một lần và, không phụ thuộc vào việc chúng đã được hợp đồng quan sát hay chưa, chúng không thể bị đảo ngược.

[4] Thật vậy, một Casethời gian chờ không còn có thể được đưa ra sau thời gian chờ, ngay cả khi thời gian chờ đó không được hợp đồng quan sát, vì thời gian chờ được kiểm tra trước Inputs. Tuy nhiên, một người tham gia có thể muốn kích hoạt thời gian chờ trong trường hợp không Inputscần người khác, ví dụ: để kích hoạt một hoặc nhiều khoản thanh toán. Trong việc triển khai ngữ nghĩa hiện tại sẽ được thực hiện bằng cách đưa ra một giao dịch với một danh sách trống Inputs.