Bài 17: Ngữ nghĩa của Marlowe 2.0

Hướng dẫn này cung cấp ngữ nghĩa chính thức cấp cao của Marlowe 2.0 bằng cách mô tả các loại đầu vào được hỗ trợ và các chức năng ngữ nghĩa chính.

Nói chung, những người tham gia hợp đồng Marlowe giao tiếp với hợp đồng bằng cách phát hành giao dịch. Tại mỗi khối, một chuỗi gồm 0 hoặc nhiều giao dịch có thể được xử lý -- theo trình tự -- bằng một hợp đồng.

Từ quan điểm về ngữ nghĩa, một giao dịch bao gồm một danh sách các đầu vào và toàn bộ giao dịch có thể được ký bởi một hoặc nhiều người tham gia. Cụ thể, chúng ta biểu thị một giao dịch dưới dạng danh sách AnyInput cùng với một tập hợp các số nguyên biểu thị tập hợp các bên ký kết.

Như chúng ta đã đề cập trong hướng dẫn trước <marlowe-data>{.interpreted-text role="ref"}, đầu vào có thể có một trong bốn loại: Commit, Pay, Choice và Oracle . Trong số này, Commit và Pay được coi là hành động và thường được liên kết với việc chuyển tiền giữa người tham gia và hợp đồng. Choice và Oracle được sử dụng để cung cấp thông tin từ thế giới bên ngoài cho hợp đồng.

Hàm applyTransaction

Tác động của việc thực hiện một giao dịch trong hợp đồng Marlowe được mô hình hóa bằng chức năng cấp cao nhất applyTransaction. Thao tác này sẽ xử lý giao dịch và trạng thái hiện tại của hợp đồng (bao gồm trạng thái bên trong, hợp đồng còn lại và số tiền còn lại trong hợp đồng), đồng thời trả về trạng thái mới của hợp đồng cùng với số tiền mà mỗi người tham gia được cho là chuyển đến hoặc từ hợp đồng như một phần của giao dịch.

Hàm applyTransaction có loại Haskell sau:

applyTransaction :: [AnyInput] -> S.Set Person -> BlockNumber -> State -> Contract -> Integer
                -> MApplicationResult (Integer, TransactionOutcomes, State, Contract)

Đổi lại, hàm applyTransaction gọi ba hàm phụ trợ chính: reduce, fetchPrimitive và eval.

• Hàm reduce (và hàm phụ của nó reduceRec) được ứng dụng trước và sau mỗi lần nhập,
• fetchPrimitive chỉ được ứng dụng cho đầu vào là các hành động (tức là: Commit và Pay) và
• eval được ứng dụng cho kết quả của fetchPrimitive bất cứ khi nào thích hợp.

Ngoài ba chức năng này, có ba chức năng bổ sung được ứng dụng trong mọi giao dịch. Trước khi xử lý thông tin đầu vào, hàm expireCommits được ứng dụng và sau khi xử lý thông tin đầu vào, các hàm redeemMoney và simplify được ứng dụng.

Xử lý hành động

Chúng ta hãy bắt đầu bằng cách xem xét các phần của quá trình xử lý mà ngữ nghĩa thực hiện riêng cho các hành động (tức là các đầu vào thuộc loại Commit và Pay).

Một hành động được đại diện bởi IdAction của nó. Hàm fetchPrimitive sẽ duyệt qua các phần của hợp đồng hiện đang có hiệu lực (được kích hoạt) và tìm kiếm một nguyên hàm khớp với IdAction do đầu vào cung cấp. fetchPrimitive sẽ chỉ thành công nếu có chính xác một nguyên hàm tương ứng với IdAction đã cho.

fetchPrimitive idAction blockNum state (Both leftContract rightContract) =
    case (go leftContract, go rightContract) of
        (Picked (result, cont), NoMatch) -> Picked (result, (Both cont rightContract))
        (NoMatch, Picked (result, cont)) -> Picked (result, (Both leftContract cont))
        (NoMatch, NoMatch) -> NoMatch
        _                  -> MultipleMatches
    where go = fetchPrimitive idAction blockNum state

Nếu thành công, fetchPrimitive sẽ trả về một DetachedPrimitive:

data DetachedPrimitive = DCommit IdCommit Person Integer Timeout
                       | DPay IdCommit Person Integer

fetchPrimitive cũng sẽ trả lại hợp đồng sau khi loại bỏ nguyên mẫu đã chọn; hợp đồng mới này sẽ được coi là hợp đồng còn lại nếu đánh giá thành công. DetachedPrimitive được chuyển đến eval, cùng với Trạng thái hiện tại của hợp đồng.

fetchPrimitive :: IdAction -> BlockNumber -> State -> Contract
                -> FetchResult (DetachedPrimitive, Contract)

Commit

Một Commit cho phép person tham gia chuyển vào hợp đồng một số tiền value. Số tiền này sẽ được ghi lại trong hợp đồng theo số nhận dạng idCommit và các khoản thanh toán trong tương lai có thể sử dụng số nhận dạng này làm nguồn tiền. Sau khi đạt đến khối được chỉ định bởi timeout (khối Timeout thứ hai trong Commit), bất kỳ khoản tiền nào từ Commit chưa được chi tiêu (thông qua các khoản thanh toán) sẽ bị đóng băng và người tham gia đã thực hiện cam kết sẽ có thể rút nó với giao dịch tiếp theo mà người đó ký.

eval (DCommit idCommit person value timeout) state =
    if (isCurrentCommit idCommit state) || (isExpiredCommit idCommit state)
    then InconsistentState
    else Result ( addOutcome person (- value) emptyOutcome
                , addCommit idCommit person value timeout state)
                NoProblem

Để một cam kết có hiệu lực, không có cam kết nào với số nhận dạng idCommit được phát hành trước đó (chỉ cho phép một Commit trên mỗi số nhận dạng).

Nếu Commit không timeout và được phát hành chính xác, thì hợp đồng còn lại, do hàm fetchPrimitive trả về, sẽ sử dụng sự tiếp tục đầu tiên (contract đầu tiên trong Commit).

fetchPrimitive idAction blockNum state (Commit idActionC idCommit person value _ timeout continuation _) =
    if (idAction == idActionC && notCurrentCommit && notExpiredCommit)
    then Picked ((DCommit idCommit person actualValue timeout),
                continuation)
    else NoMatch
    where notCurrentCommit = not (isCurrentCommit idCommit state)
            notExpiredCommit = not (isExpiredCommit idCommit state)
            actualValue = evalValue blockNum state value

Mặt khác, nếu bất kỳ thời gian chờ nào của Commit đã hết, reduceRec (hàm phụ của reduce) chỉ định rằng Commit sẽ bị giảm xuống tiếp tục thứ hai.

reduceRec blockNum state env c@(Commit _ _ _ _ timeout_start timeout_end _ continuation) =
    if (isExpired blockNum timeout_start) || (isExpired blockNum timeout_end)
    then reduceRec blockNum state env continuation
    else c

Pay

Một Pay cho phép person tham gia yêu cầu từ hợp đồng một số tiền value. Số tiền này sẽ được chiết khấu từ số tiền cam kết theo định danh idCommit và hợp đồng sẽ chỉ thanh toán tối đa số tiền còn lại theo idCommit, ngay cả khi có thêm tiền trong hợp đồng. Trong mọi trường hợp, Pay sẽ không trả tiền nếu cam kết idCommit đã hết hạn.

eval (DPay idCommit person value) state =
    if (not $ isCurrentCommit idCommit state)
    then (if (not $ isExpiredCommit idCommit state)
            then Result (emptyOutcome, state) CommitNotMade
            else Result (emptyOutcome, state) CommitIsExpired)
    else (if value > maxValue
            then Result ( addOutcome person maxValue emptyOutcome
                        , fromJust $ discountAvailableMoneyFromCommit idCommit maxValue state)
                        NotEnoughMoneyLeftInCommit
            else Result ( addOutcome person value emptyOutcome
                        , fromJust $ discountAvailableMoneyFromCommit idCommit value state)
                        NoProblem)
    where maxValue = getAvailableAmountInCommit idCommit state

Nếu Pay không timeout và được xác nhận quyền sở hữu chính xác, hợp đồng còn lại, như được trả về bởi hàm fetchPrimitive , sẽ sử dụng tiếp tục đầu tiên (contract đầu tiên trong Pay).

fetchPrimitive idAction blockNum state (Pay idActionC idCommit person value _ continuation _) =
    if (idAction == idActionC)
    then Picked ((DPay idCommit person actualValue), continuation)
    else NoMatch
    where actualValue = evalValue blockNum state value

Mặt khác, nếu timeout của Pay , reduceRec (chức năng phụ trợ của reduce) chỉ định rằng Pay sẽ bị giảm xuống tiếp tục thứ hai.

reduceRec blockNum state env c@(Pay _ _ _ _ timeout _ continuation) =
    if isExpired blockNum timeout
    then reduceRec blockNum state env continuation
    else c

Quá trình xử lý thông tin đầu vào không phải hành động

Đầu vào Choice+ và +Oracle+ được xử lý rất khác với các hành động. Chúng tương đối độc lập với trạng thái của hợp đồng và chúng có thể được phát hành bất cứ lúc nào, miễn là các giá trị được cung cấp có thể được hợp đồng sử dụng. Nói cách khác, phải có một nơi nào đó trong mã của hợp đồng kiểm tra giá trị [+Choice]{.title-ref} hoặc Oracle để người tham gia có thể cung cấp giá trị đó. Mặt khác, hợp đồng không cần biết giá trị và dù sao việc cung cấp nó sẽ chỉ làm tăng thêm sự lộn xộn và tải cho hợp đồng và blockchain, điều này cuối cùng có thể dẫn đến các vấn đề như DoS. Vì những lý do này, ngữ nghĩa của Marlowe 2.0 không cho phép cung cấp thông tin không cần thiết.

Ngoài ra, điều duy nhất mà Marlowe làm khi được cung cấp Choice+s và +Oracle+s là ghi lại chúng ở trạng thái để hàm [+reduce]{.title-ref} có thể truy cập chúng.

Combinators và Null

Trong phần này, chúng ta mô tả ngữ nghĩa của các hợp đồng Marlowe còn lại, có thể được sử dụng để kết hợp các hợp đồng khác lại với nhau và quyết định giữa chúng, tùy thuộc vào thông tin được biết về hợp đồng tại bất kỳ thời điểm nào. Ngữ nghĩa của các tổ hợp này chủ yếu được xác định bởi reduceRec (hàm phụ trợ của reduce). Tuy nhiên, hành vi của chúng cũng ảnh hưởng đến các chức năng khác, đặc biệt là fetchPrimitive và simplify.

Ví dụ: các quy tắc kích hoạt của từng cấu trúc được phản ánh trong fetchPrimitive, tức là nếu cấu trúc kích hoạt ngay lập tức các hợp đồng phụ được dịch trong fetchPrimitive thì sẽ có thể kiểm tra đệ quy một số hợp đồng phụ của nó. Đây là trường hợp của hợp đồng phụ thứ hai của Let:

fetchPrimitive idAction blockNum state (Let label boundContract subContract) =
    case fetchPrimitive idAction blockNum state subContract of
        Picked (result, cont) -> Picked (result, Let label boundContract cont)
        NoMatch -> NoMatch
        MultipleMatches -> MultipleMatches

Trong khi đó, trong trường hợp các cấu trúc khác như When, fetchPrimitive sẽ không thay đổi toàn bộ cấu trúc:

fetchPrimitive _ _ _ _ = NoMatch

Null

Hợp đồng Null không làm gì cả và không hoạt động mãi mãi.

reduceRec _ _ _ Null = Null

Tuy nhiên, nó được sử dụng bởi chức năng đơn giản hóa và nó có thể được dùng để thay thế một hợp đồng bằng một hợp đồng nhỏ hơn nhưng tương đương. Ví dụ: Both Null Null có thể rút gọn thành Null.

Both

Cấu trúc Both cho phép hai hợp đồng hoạt động đồng thời. Nó giống như có hai hợp đồng riêng biệt được triển khai đồng thời, ngoại trừ khi sử dụng Cả hai chúng sẽ chia sẻ Trạng thái và do đó, Cam kết+ được thực hiện trong một trong các hợp đồng có thể được sử dụng cho +Trả+ trong hợp đồng kia. Chúng ta cũng đã rất cẩn thận để đảm bảo rằng [+Both]{.title-ref} đối xứng, nghĩa là viết Cả A B phải tương đương với viết Cả B A, bất kể A và B là gì.

reduceRec blockNum state env (Both cont1 cont2) = Both (go cont1) (go cont2)
    where go = reduceRec blockNum state env

Choice

Cấu trúc Choice ngay lập tức chọn giữa hai hợp đồng tùy thuộc vào giá trị của Observation. Thời điểm Choice được kích hoạt, giá trị của obs sẽ quyết định liệu Choice có bị giảm xuống còn cont1 (nếu giá trị này đúng) hay thành cont2 (nếu giá trị này sai).

reduceRec blockNum state env (Choice obs cont1 cont2) =
    reduceRec blockNum state env (if (evalObservation blockNum state obs)
                                    then cont1
                                    else cont2)

When

Cấu trúc When làm chậm hợp đồng trong thời gian cho đến khi Observation trở thành sự thật. When sẽ không kích hoạt bất kỳ hợp đồng phụ nào cho đến khi Observation trở thành sự thật hoặc cho đến khi đạt đến timeout khối. Nếu obs là đúng thì When được giảm xuống còn cont1, nếu timeout thì When được giảm xuống còn cont2.

reduceRec blockNum state env c@(When obs timeout cont1 cont2) =
    if isExpired blockNum timeout
    then go cont2
    else if evalObservation blockNum state obs
        then go cont1
        else c
    where go = reduceRec blockNum state env

Điều đáng chú ý là vì Marlowe tuân theo mô hình pull, nên chỉ +Observation+ trở thành sự thật đối với When tiến hóa là không đủ; hợp đồng cần được kích hoạt trong khi Observation là đúng. Hợp đồng có thể được kích hoạt bất cứ lúc nào bằng cách phát hành một giao dịch không cần có bất kỳ đầu vào nào và không cần phải ký; thực sự bất cứ ai cũng có thể kích hoạt hợp đồng.

While

Cấu trúc While hoạt động theo cách ngược lại với When, theo nghĩa là trong khi When được giảm khi Observation trở thành đúng, While được giảm khi Observation của nó trở thành sai.

reduceRec blockNum state env (While obs timeout contractWhile contractAfter) =
    if isExpired timeout blockNum
    then go contractAfter
    else if evalObservation blockNum state obs
        then (While obs timeout (go contractWhile) contractAfter)
        else go contractAfter
    where go = reduceRec blockNum state env

Tuy nhiên, có một điểm khác biệt cơ bản: When không kích hoạt hợp đồng phụ cho đến khi hợp đồng đó bị giảm giá trị và While kích hoạt hợp đồng phụ ngay lập tức, tương tự như hành vi của Both. Và có một điểm độc đáo về While: nó có thể xóa một hợp đồng đã được kích hoạt sau khi Observation trở thành sự thật. Ví dụ, trong hợp đồng sau:

While
    (NotObs
        (ChoseSomething (1, 1))) 20
    (Commit 1 1 1
        (ValueFromChoice (1, 1)
            (Constant 20)) 10 20 Null Null) Null

sau khi lựa chọn (1, 1) được thực hiện, bạn sẽ không thể sử dụng Commit nữa.

Scale

Cấu trúc Scale chia tỷ lệ số tiền được trả bởi Commit và Pay. Phải mất ba value, giá trị đầu tiên là tử số, giá trị thứ hai là mẫu số và giá trị thứ ba là giá trị mặc định.

Ngay sau khi cấu trúc Scale được kích hoạt, nó sẽ kích hoạt hợp đồng phụ contract của nó và nó đánh giá tất cả ba Giá trị+ và thay thế chúng bằng một +Hằng số (để chúng không thể thay đổi nữa).

reduceRec blockNum state env (Scale divid divis def contract) =
    Scale (Constant vsDivid) (Constant vsDivis) (Constant vsDef) (go contract)
    where go = reduceRec blockNum state env
            vsDivid = evalValue blockNum state divid
            vsDivis = evalValue blockNum state divis
            vsDef = evalValue blockNum state def

Sau khi được đánh giá, mọi Commit hoặc Pay (trong contract) sẽ nhận được số tiền theo tỷ lệ như sau:

• Nếu số chia là 0 thì số tiền sẽ được thay thế bằng giá trị mặc định.

• Nếu số chia không phải là 0, thì số tiền được nhân với tử số và chia (sử dụng phép chia số nguyên) cho mẫu số.

  scaleValue :: Integer -> Integer -> Integer -> Integer -> Integer scaleValue divid divis def val = if (divis == 0) then def else ((val * divid) div divis)

Quá trình mở rộng quy mô Commit+s và +Pay+s được thực hiện bởi hàm Pay[+fetchPrimitivePay]{.title-ref}.

fetchPrimitive idAction blockNum state (Scale divid divis def subContract) =
    case fetchPrimitive idAction blockNum state subContract of
        Picked (result, cont) -> Picked (scaleResult sDivid sDivis sDef result,
                                        Scale divid divis def cont)
        NoMatch -> NoMatch
        MultipleMatches -> MultipleMatches
    where sDivid = evalValue blockNum state divid
            sDivis = evalValue blockNum state divis
            sDef = evalValue blockNum state def

Sau khi không có Commit+ hoặc +Pay+ bên trong [+Scale]{.title-ref}, nó sẽ bị xóa bởi hàm simplify.

Let và Use

Cấu trúc Let liên kết hợp đồng phụ đầu tiên boundContract với một mã định danh label.

reduceRec blockNum state env (Let label boundContract contract) =
    case lookupEnvironment label env of
        Nothing -> let newEnv = addToEnvironment label checkedBoundContract env in
                Let label checkedBoundContract $ reduceRec blockNum state newEnv contract
        Just _ -> let freshLabel = getFreshLabel env contract in
                let newEnv = addToEnvironment freshLabel checkedBoundContract env in
                let fixedContract = relabel label freshLabel contract in
                Let freshLabel checkedBoundContract $ reduceRec blockNum state newEnv fixedContract
    where checkedBoundContract = nullifyInvalidUses env boundContract

Chúng ta cho rằng mỗi Let nên có một label mã định danh khác nhau, bởi vì việc sử dụng lại chúng dẫn đến nhầm lẫn, nhầm lẫn dẫn đến sai sót và sai sót dẫn đến tối tăm. hem. Ý tôi là. khả năng mất tiền bạc.

Tuy nhiên, chúng ta đã viết ngữ nghĩa Marlowe để lần xuất hiện gần đây nhất của Let (trong cùng) được ưu tiên trong trường hợp xung đột (điều này thường được gọi là tạo bóng). Cách triển khai điều này là bất cứ khi nào có xung đột về số nhận dạng, số nhận dạng mới được xác định sẽ được đổi tên thành số nhận dạng mới chưa được sử dụng (trong cây con hiện tại), đó là chức năng relabel thực hiện.

Bên trong phần tiếp theo thứ hai (contract) của Let có thể sử dụng cấu trúc Use để thể hiện một bản sao của boundContract sẽ chỉ được mở rộng khi hợp đồng Use được kích hoạt:

reduceRec blockNum state env (Use label) =
    case lookupEnvironment label env of
        Just contract -> reduceRec blockNum state env contract
        Nothing -> Null

Lưu ý rằng nếu Use không được xác định thì nó sẽ mở rộng thành Null.

Tương tự với Scale, Let cấu trúc sẽ chỉ bị giảm khi không có cấu trúc Use tương ứng nào sử dụng nó, quy trình dọn dẹp này được thực hiện bởi hàm simpleify .

---