Bài 14: Các phiên bản 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.

Loại bỏ Both

chúng ta không bao gồm một Both cấu trúc 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 Bot hnên chức năng bổ sung duy nhất được cung cấp Both trê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 ta chăm sóc 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ể đợi một trong một số đầu vào có thể cùng một lúc (như trong select).

Lý do chúng ta 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 điều kiện chủng tộc.

Thêm vào 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 ta đã 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 ta bao gồm các tài khoản để 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ả 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 ta chọn bao gồm các tài khoản là vì không có chúng, chúng ta nhận thấy rằng về cơ bản chúng ta đ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 ta thấy mình phải tính toán xem chúng ta 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 "bảng nấu sôi" 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 ta 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 Pay lệ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ì Close khô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 ta 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 mọi thứ 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 sẽ 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 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.

Close replaces 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 hợp đồng chấm dứt, tức là: khi nào thì chỉ Nullcòn lại. chúng ta 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 ta đã đổi tên thành Null (Close trợ 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 một cách tĩnh và hiệu quả giới hạn trên 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.

Trả tiền (Pay)

Pay bâ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 ta đã loại bỏ PayAll, vì nó có thể được mô phỏng như một chuỗi hữu hạn của Pay. Trên thực tế, chúng ta có thể định nghĩa payAll như một hàm Haskell (xem ví dụ zeroCouponBond).

Đó là hệ quả của việc loại bỏ Both cấ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 Both cấu trúc, chúng ta có thể có khả năng Pay sxả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).

Nhiều mệnh đề When

Chúng ta đã sửa đổi When để bao gồm một tập hợp các thực thi khả thi có thể được nhập vào trong khi When chờ đợi. chúng ta 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 thực thi trong số nhiều thực thi được phép tiềm năng. Whenvẫn như sau:

    When [Case] Timeout Contract

When sẽ đợi Timeout và 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à Action như:

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 Actions khớp, cái đầu tiên trong danh sách sẽ được thực thi.

Ba loại thực thi đượ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 Integer giá trị (được chỉ định bởi danh sách Bounds).
• Notify sẽ đợi một Notify thực thi được đưa ra khi Observation đúng. chúng ta gọi nó là Notify để làm rõ rằng chúng ta không thể chỉ chờ đợi Observations mà phải có người kích hoạt hợp đồng trong một thời điểm khi an Observation là đúng.

chúng ta đã loại bỏ việc bổ sung các quan sát vào Deposit và Choice vì sẽ không rõ liệu các quan sát Observation sẽ được đánh giá trước hay sau khi áp dụng thực thi.

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].

Quan sát và Giá trị

chúng ta đã loại bỏ Observations và 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 ta đã giữ lại ChoseSomething quan sát, mặc dù, trong ngữ nghĩa được đề xuất, mọi sự xuất hiện của ChoseSomething có 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 ChoseSomething sẽ đánh giá True và 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 ta đã 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 cấu trúc When để hỗ trợ “nhiều trong số nhiều” đầu vào.

Thêm SlotIntervals

Đặc tả EUTxO cung cấp các tập lệnh xác thực với các khoảng thời gian thay vì với số slot. Đ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 ta đã giữ thời gian chờ When (thời gian chờ duy nhất) như một số slot. Cách chúng ta xử lý các khoảng thời gian là bằng cách 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 chờ nào mà ngữ nghĩa phải lựa chọn. Ví dụ: nếu thời gian chờ là 10, giao dịch với khoảng thời gian 5-15 sẽ không thành công với AmbiguousSlotInterval. Những người tham gia sẽ phải thực hiện một giao dịch với khoảng thời gian 5-9 hoặc 10-15 (hoặc cả hai).

Tuy nhiên, đối với Values, chúng ta cung cấp hai cấu trúc SlotIntervalStart và SlotIntervalEnd. 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 một CurrentSlot cấu trúc và chỉ làm mất hiệu lực các giao dịch mơ hồ, 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 ta 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 Close đến hạn 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 Notify vì mặc dù Observations có thể xen kẽ giữa True và 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, Case không còn có thể đưa ra một thông báo rõ ràng 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 Inputs cầ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.

---