diff --git a/src/lib_base/bounded.ml b/src/lib_base/bounded.ml index d31bd44a0fb1ab1bc3bcf8374b4589a9a8cb4769..24a46987a82940050178e05c3543ffa28f6d9172 100644 --- a/src/lib_base/bounded.ml +++ b/src/lib_base/bounded.ml @@ -65,4 +65,10 @@ module Int32 = struct | Some x -> Ok x) int32) end + + module NonNegative = Make (struct + let min_int = 0l + + let max_int = Int32.max_int + end) end diff --git a/src/lib_base/bounded.mli b/src/lib_base/bounded.mli index 46539808d0884e20c02aa453b83a4f157c4de1e4..58b341f6f49acd12b156df8c797b7aa44bd30aec 100644 --- a/src/lib_base/bounded.mli +++ b/src/lib_base/bounded.mli @@ -67,4 +67,6 @@ module Int32 : sig redundant bytes to each message. *) module Make (_ : BOUNDS) : S + + module NonNegative : S end diff --git a/src/lib_protocol_environment/environment_V6.ml b/src/lib_protocol_environment/environment_V6.ml index 687c637789cfacf056d6ece596c85ea508fb5089..9efd77c123fed38cd1d990fad9d91a76c4e9faff 100644 --- a/src/lib_protocol_environment/environment_V6.ml +++ b/src/lib_protocol_environment/environment_V6.ml @@ -1101,15 +1101,60 @@ struct end module Wasm_2_0_0 = struct + type input = { + inbox_level : Bounded.Int32.NonNegative.t; + message_counter : Z.t; + } + + type output = { + outbox_level : Bounded.Int32.NonNegative.t; + message_index : Z.t; + } + + type input_request = No_input_required | Input_required + + type info = { + current_tick : Z.t; + last_input_read : input option; + input_request : input_request; + } + module Make (Tree : Context.TREE with type key = string list and type value = bytes) = struct - (* TODO: https://gitlab.com/tezos/tezos/-/issues/3090 - The expected implementation of this function is the step - function implemented in `lib_webassembly'. *) module Wasm = Tezos_scoru_wasm.Make (Tree) - let step (t : Tree.tree) = Wasm.step t + (* TODO: https://gitlab.com/tezos/tezos/-/issues/3214 + The rest of the module is pure boilerplate converting between + the types of [Tezos_scoru_wasm] and [Environment_V6.Wasm_2_0_0]. + *) + + let compute_step (tree : Tree.tree) = Wasm.compute_step tree + + let set_input_step {inbox_level; message_counter} payload + (tree : Tree.tree) = + Wasm.set_input_step {inbox_level; message_counter} payload tree + + let get_output {outbox_level; message_index} (tree : Tree.tree) = + Wasm.get_output {outbox_level; message_index} tree + + let convert_input : Tezos_scoru_wasm.input -> input = function + | {inbox_level; message_counter} -> {inbox_level; message_counter} + + let get_info (tree : Tree.tree) = + let open Lwt_syntax in + let* info = Wasm.get_info tree in + match info with + | {current_tick; last_input_read; input_request} -> + Lwt.return + { + current_tick; + last_input_read = Option.map convert_input last_input_read; + input_request = + (match input_request with + | No_input_required -> No_input_required + | Input_required -> Input_required); + } end end diff --git a/src/lib_protocol_environment/sigs/v6/bounded.mli b/src/lib_protocol_environment/sigs/v6/bounded.mli index 46539808d0884e20c02aa453b83a4f157c4de1e4..58b341f6f49acd12b156df8c797b7aa44bd30aec 100644 --- a/src/lib_protocol_environment/sigs/v6/bounded.mli +++ b/src/lib_protocol_environment/sigs/v6/bounded.mli @@ -67,4 +67,6 @@ module Int32 : sig redundant bytes to each message. *) module Make (_ : BOUNDS) : S + + module NonNegative : S end diff --git a/src/lib_protocol_environment/sigs/v6/wasm_2_0_0.mli b/src/lib_protocol_environment/sigs/v6/wasm_2_0_0.mli index ca448ec3bcd8ab1d8041c08d30734b7e7b549339..3d9b45fea9c5c8999c4003832c04ef3fa577a67b 100644 --- a/src/lib_protocol_environment/sigs/v6/wasm_2_0_0.mli +++ b/src/lib_protocol_environment/sigs/v6/wasm_2_0_0.mli @@ -23,7 +23,25 @@ (* *) (*****************************************************************************) +type input = {inbox_level : Bounded.Int32.NonNegative.t; message_counter : Z.t} + +type output = {outbox_level : Bounded.Int32.NonNegative.t; message_index : Z.t} + +type input_request = No_input_required | Input_required + +type info = { + current_tick : Z.t; + last_input_read : input option; + input_request : input_request; +} + module Make (Tree : Context.TREE with type key = string list and type value = bytes) : sig - val step : Tree.tree -> Tree.tree Lwt.t + val compute_step : Tree.tree -> Tree.tree Lwt.t + + val set_input_step : input -> string -> Tree.tree -> Tree.tree Lwt.t + + val get_output : output -> Tree.tree -> string Lwt.t + + val get_info : Tree.tree -> info Lwt.t end diff --git a/src/lib_scoru_wasm/tezos_scoru_wasm.ml b/src/lib_scoru_wasm/tezos_scoru_wasm.ml index cbf96acaeb614c640f146ab39cf3bdcdbfb38e93..73b47e4aaf983f7e35e468f277736cbd25f3bbe8 100644 --- a/src/lib_scoru_wasm/tezos_scoru_wasm.ml +++ b/src/lib_scoru_wasm/tezos_scoru_wasm.ml @@ -32,12 +32,216 @@ open Sigs +type input = { + inbox_level : Tezos_base.Bounded.Int32.NonNegative.t; + message_counter : Z.t; +} + +type output = { + outbox_level : Tezos_base.Bounded.Int32.NonNegative.t; + message_index : Z.t; +} + +type input_request = No_input_required | Input_required + +type info = { + current_tick : Z.t; + (** The number of ticks processed by the VM, zero for the initial state. + + [current_tick] must be incremented for each call to [step] *) + last_input_read : input option; + (** The last message to be read by the VM, if any. *) + input_request : input_request; (** The current VM input request. *) +} + +exception Malformed_origination_message + +exception Malformed_inbox_message + module Make (T : TreeS) : sig - val step : T.tree -> T.tree Lwt.t + (** [compute_step] forwards the VM by one compute tick. + + If the VM is expecting input, it gets stuck. + + If the VM is already stuck, this function may raise an exception. *) + val compute_step : T.tree -> T.tree Lwt.t + + (** [set_input_step] forwards the VM by one input tick. + + If the VM is not expecting input, it gets stuck. + + If the VM is already stuck, this function may raise an exception. *) + val set_input_step : input -> string -> T.tree -> T.tree Lwt.t + + (** [get_output output state] returns the payload associated with the given output. + + The result is meant to be deserialized using [Sc_rollup_PVM_sem.output_encoding]. + + If the output is missing, this function may raise an exception. + *) + val get_output : output -> T.tree -> string Lwt.t + + (** [get_info] provides a typed view of the current machine state. + + Should not raise. *) + val get_info : T.tree -> info Lwt.t + + + val kernel_loading_step : string -> T.tree -> T.tree Lwt.t end = struct module Tree = struct include T end - let step = Lwt.return + module Decoding = Tree_decoding.Make(Tree) + + + (* Update/set value in tree *) + + let update_set key value t = + Lwt.return t (* TODO *) + + (* TYPES *) + + (* From the outside the PVM is either computing or waiting for input. The internal + * status also includes _what_ is done with the input we are expecting - loading a + * kernel or waiting for input to a running kernel; and what kind of computation is + * running - parsing a kernel image or executing a kernel. *) + type internal_status = Parsing | Computing | WaitingForInput | GatheringFloppies + + (* The public key that is included in the initial (origination) operation + * that created the rollup in case the origination operation contained an + * in-complete kernel image. The rest of the kernel image chunks must be + * signed with this key. *) + type initial_boot_pk = bytes + + (* Each chunk of the kernel image needs a signature matching the public key + * included in the origination message - so that not just anyone can add + * arbitrary chunks to the kernel image. *) + type kernel_image_signature = bytes + + (* The first message containing the kernel image. In case the whole kernel + * fits (less than 32kb in size) it is a `CompleteKernel`. Otherwise we'll + * also need a public key to check signatures of the following kernel image + * chunks. *) + type origination_message = + | CompleteKernel of bytes + | InCompleteKernel of bytes * initial_boot_pk + + (* The following messages containing the kernel image. Each chunk must be + * signed (validate with public key in origination message). *) + type inbox_kernel_message = InboxKernelMessage of bytes * kernel_image_signature + + (* STORAGE KEYS *) + + (* The key to the storage tree where the _internal_ status is stored *) + let internal_status_key = ["pvm"; "status"] + + (* Where the initial boot public key is stored in the tree *) + let initial_boot_pk_key = ["pvm"; "public_key"] + + (* Where the chunks are stored *) + let kernel_image_chunks_key = ["pvm"; "kernel_image"] + + (* ENCODINGS *) + + (* Decodes the status as it is stored in the tree *) + let internal_status_encoding = + let open Data_encoding in + union [ + case + ~title:"parsing" + (Tag 0) + unit + (function Parsing -> Some () | _ -> None) + (fun () -> Parsing); + case + ~title:"computing" + (Tag 1) + unit + (function Computing -> Some () | _ -> None) + (fun () -> Computing); + case + ~title:"waiting for input" + (Tag 2) + unit + (function WaitingForInput -> Some () | _ -> None) + (fun () -> WaitingForInput); + case + ~title:"gathering floppies" + (Tag 3) + unit + (function GatheringFloppies -> Some () | _ -> None) + (fun () -> GatheringFloppies) + ] + + let initial_boot_pk_encoding = Data_encoding.bytes + + let origination_message_encoding = + failwith "not implemented" + + let inbox_kernel_message_encoding = + failwith "not implemented" + + (* STORAGE/TREE INTERACTION *) + + let get_internal_status = + Decoding.(run (value internal_status_key internal_status_encoding)) + + let set_internal_status v t = + update_set internal_status_key v t + + (* Get the initial boot public key from the tree *) + let get_initial_boot_pk = + Decoding.(run (value initial_boot_pk_key initial_boot_pk_encoding)) + + let set_initial_boot_pk = + update_set initial_boot_pk_key + + let store_kernel_image_chunk chunk t = + failwith "Not implemented yet" + + (* PROCESS MESSAGES *) + + (* Process and store the kernel image in the origination message + * This message contains either the entire (small) kernel image or the first + * chunk of it. *) + let origination_kernel_loading_step message t = + match Data_encoding.Binary.of_string origination_message_encoding message with + | Error error -> raise Malformed_origination_message + | Ok (CompleteKernel chunk) -> Lwt.Syntax.( + let* t2 = store_kernel_image_chunk chunk t in + set_internal_status Parsing t2) + | Ok (InCompleteKernel (chunk, boot_pk)) -> Lwt.Syntax.( + let* t2 = store_kernel_image_chunk chunk t in + let* t3 = set_initial_boot_pk boot_pk t2 in + set_internal_status GatheringFloppies t3) + + (* Process sub-sequent kernel image chunks. If the chunk has zero length it + * means we're done and we have the entire kernel image. *) + let kernel_loading_step message t = + match Data_encoding.Binary.of_string inbox_kernel_message_encoding message with + | Error error -> raise Malformed_inbox_message + | Ok (InboxKernelMessage (chunk, _signature)) -> + if Bytes.length chunk = 0 + then set_internal_status Parsing t + else store_kernel_image_chunk chunk t + + let compute_step = Lwt.return + + let set_input_step i chunk t = Lwt.return t + (* TODO: https://gitlab.com/tezos/tezos/-/issues/3092 + + Implement handling of input logic. + *) + + let get_output _ _ = Lwt.return "" + + let get_info _ = + Lwt.return + { + current_tick = Z.of_int 0; + last_input_read = None; + input_request = No_input_required; + } end diff --git a/src/proto_alpha/lib_protocol/raw_level_repr.ml b/src/proto_alpha/lib_protocol/raw_level_repr.ml index 82aa2ef9b5d76047f7c135a6fb21d1370197a924..8a888f0f2d3f47e42a635c7517eea64d680c71e4 100644 --- a/src/proto_alpha/lib_protocol/raw_level_repr.ml +++ b/src/proto_alpha/lib_protocol/raw_level_repr.ml @@ -62,6 +62,11 @@ let diff = Int32.sub let to_int32 l = l +let to_int32_non_negative l = + match Bounded.Int32.NonNegative.of_int32 l with + | Some x -> x + | _ -> assert false (* invariant: raw_levels are non-negative *) + type error += Unexpected_level of Int32.t (* `Permanent *) let () = @@ -87,6 +92,11 @@ let of_int32_exn l = | Ok l -> l | Error _ -> invalid_arg "Level_repr.of_int32" +let of_int32_non_negative l = + match of_int32 (Bounded.Int32.NonNegative.to_int32 l) with + | Ok l -> l + | Error _ -> assert false (* invariant: raw_levels are non-negative *) + let encoding = Data_encoding.conv_with_guard to_int32 diff --git a/src/proto_alpha/lib_protocol/raw_level_repr.mli b/src/proto_alpha/lib_protocol/raw_level_repr.mli index a10ebdaa31eaf14112ae4d2b8f759d7b34022a1a..bc6540be1d64a38706b19b382e4092fa9b24a3fc 100644 --- a/src/proto_alpha/lib_protocol/raw_level_repr.mli +++ b/src/proto_alpha/lib_protocol/raw_level_repr.mli @@ -41,12 +41,16 @@ include Compare.S with type t := raw_level val to_int32 : raw_level -> int32 +val to_int32_non_negative : raw_level -> Bounded.Int32.NonNegative.t + (** @raise Invalid_argument when the level to encode is negative *) val of_int32_exn : int32 -> raw_level (** Can trigger Unexpected_level error when the level to encode is negative *) val of_int32 : int32 -> raw_level tzresult +val of_int32_non_negative : Bounded.Int32.NonNegative.t -> raw_level + val diff : raw_level -> raw_level -> int32 val root : raw_level diff --git a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml index 22156b964fedbc8dc43fb4ac1185cf1cf2148ca8..4485fa03e32f1d188bd7167c935b55afcf705697 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml @@ -40,6 +40,8 @@ let of_int x = if Compare.Int.(x < 0) then None else Some (Z.of_int x) let to_int x = if Z.fits_int x then Some (Z.to_int x) else None +let of_z x = x + let of_number_of_ticks x = Z.of_int (Int32.to_int (Sc_rollup_repr.Number_of_ticks.to_int32 x)) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli index feb5c90eb63f6c8088cd85e8a48679ef3c301126..802e86a9dcec090bd46f56449a6cd330cb2b3457 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli @@ -53,6 +53,8 @@ val to_int : t -> int option a negative number so an [option] isn't required. *) val of_number_of_ticks : Sc_rollup_repr.Number_of_ticks.t -> t +val of_z : Z.t -> t + val encoding : t Data_encoding.t val pp : Format.formatter -> t -> unit diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml index 8243b7403fc735cf4c55e8c4e02d0b9cf7131b13..67d9c7e040abb0bb9af31c83506e19bc6df5acc0 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml @@ -133,7 +133,7 @@ module V2_0_0 = struct module Monad : sig type 'a t - val run : 'a t -> state -> (state * 'a option) Lwt.t + val run : 'a t -> state -> (state * 'a) Lwt.t val return : 'a -> 'a t @@ -146,21 +146,15 @@ module V2_0_0 = struct val set : tree -> unit t val lift : 'a Lwt.t -> 'a t - - val find_value : Tree.key -> 'a Data_encoding.t -> 'a option t - - val set_value : Tree.key -> 'a Data_encoding.t -> 'a -> unit t end = struct - type 'a t = state -> (state * 'a option) Lwt.t + type 'a t = state -> (state * 'a) Lwt.t - let return x state = Lwt.return (state, Some x) + let return x state = Lwt.return (state, x) let bind m f state = let open Lwt_syntax in let* state, res = m state in - match res with - | None -> return (state, None) - | Some res -> f res state + f res state module Syntax = struct let ( let* ) = bind @@ -168,143 +162,12 @@ module V2_0_0 = struct let run m state = m state - let internal_error_key = ["internal_error"] - - let internal_error msg tree = - let open Lwt_syntax in - let* tree = Tree.add tree internal_error_key (Bytes.of_string msg) in - return (tree, None) - - let decode encoding bytes state = - let open Lwt_syntax in - match Data_encoding.Binary.of_bytes_opt encoding bytes with - | None -> internal_error "Error during decoding" state - | Some v -> return (state, Some v) - - let get s = Lwt.return (s, Some s) - - let set s _ = Lwt.return (s, Some ()) + let get s = Lwt.return (s, s) - let lift m s = Lwt.map (fun r -> (s, Some r)) m - - let find_value key encoding state = - let open Lwt_syntax in - let* obytes = Tree.find state key in - match obytes with - | None -> return (state, Some None) - | Some bytes -> - let* state, value = decode encoding bytes state in - return (state, Some value) - - let set_value key encoding value tree = - let open Lwt_syntax in - Data_encoding.Binary.to_bytes_opt encoding value |> function - | None -> internal_error "Internal_Error during encoding" tree - | Some bytes -> - let* tree = Tree.add tree key bytes in - return (tree, Some ()) - end - - open Monad - - module MakeVar (P : sig - type t - - val name : string - - val initial : t - - val encoding : t Data_encoding.t - end) = - struct - let key = [P.name] - - let get = - let open Monad.Syntax in - let* v = find_value key P.encoding in - match v with None -> return P.initial | Some v -> return v + let set s _ = Lwt.return (s, ()) - let set = set_value key P.encoding + let lift m s = Lwt.map (fun r -> (s, r)) m end - - module CurrentTick = MakeVar (struct - include Sc_rollup_tick_repr - - let name = "tick" - end) - - module Boot_sector = MakeVar (struct - type t = string - - let name = "boot_sector" - - let initial = "" - - let encoding = Data_encoding.string - - let _pp fmt s = Format.fprintf fmt "%s" s - end) - - module Status = MakeVar (struct - type t = status - - let initial = Computing - - let encoding = - Data_encoding.string_enum - [ - ("Computing", Computing); - ("WaitingForInputMessage", WaitingForInputMessage); - ] - - let name = "status" - - let string_of_status = function - | Computing -> "Computing" - | WaitingForInputMessage -> "WaitingForInputMessage" - - let _pp fmt status = Format.fprintf fmt "%s" (string_of_status status) - end) - - module CurrentLevel = MakeVar (struct - type t = Raw_level_repr.t - - let initial = Raw_level_repr.root - - let encoding = Raw_level_repr.encoding - - let name = "current_level" - - let _pp = Raw_level_repr.pp - end) - - module MessageCounter = MakeVar (struct - type t = Z.t option - - let initial = None - - let encoding = Data_encoding.option Data_encoding.n - - let name = "message_counter" - - let _pp fmt = function - | None -> Format.fprintf fmt "None" - | Some c -> Format.fprintf fmt "Some %a" Z.pp_print c - end) - - module NextMessage = MakeVar (struct - type t = string option - - let initial = None - - let encoding = Data_encoding.(option string) - - let name = "next_message" - - let _pp fmt = function - | None -> Format.fprintf fmt "None" - | Some s -> Format.fprintf fmt "Some %s" s - end) end module WASM_machine = Wasm_2_0_0.Make (Tree) @@ -315,88 +178,101 @@ module V2_0_0 = struct open Monad let initial_state ctxt _boot_sector = + let open Lwt_syntax in let state = Tree.empty ctxt in + let* state = Tree.add state ["wasm-version"] (Bytes.of_string "2.0.0") in Lwt.return state let state_hash state = let m = - let open Monad.Syntax in - let* status = Status.get in - match status with - | _ -> - Context_hash.to_bytes @@ Tree.hash state |> fun h -> - return @@ State_hash.hash_bytes [h] + Context_hash.to_bytes @@ Tree.hash state |> fun h -> + return @@ State_hash.hash_bytes [h] in let open Lwt_syntax in let* state = Monad.run m state in - match state with - | _, Some hash -> return hash - | _ -> (* Hash computation always succeeds. *) assert false + match state with _, hash -> return hash - let result_of ~default m state = + let result_of m state = let open Lwt_syntax in let* _, v = run m state in - match v with None -> return default | Some v -> return v + return v let state_of m state = let open Lwt_syntax in let* s, _ = run m state in return s - let get_tick = - result_of ~default:Sc_rollup_tick_repr.initial CurrentTick.get + let get_tick : Sc_rollup_tick_repr.t Monad.t = + let open Monad.Syntax in + let* s = get in + let* info = lift (WASM_machine.get_info s) in + return @@ Sc_rollup_tick_repr.of_z info.current_tick + + let get_tick : state -> Sc_rollup_tick_repr.t Lwt.t = result_of get_tick - let is_input_state_monadic = + let get_status : status Monad.t = let open Monad.Syntax in - let* status = Status.get in - match status with - (* TODO: https://gitlab.com/tezos/tezos/-/issues/3092 + let* s = get in + let* info = lift (WASM_machine.get_info s) in + return + @@ + match info.input_request with + | No_input_required -> Computing + | Input_required -> WaitingForInputMessage + + let get_last_message_read : _ Monad.t = + let open Monad.Syntax in + let* s = get in + let* info = lift (WASM_machine.get_info s) in + return + @@ + match info.last_input_read with + | Some {inbox_level; message_counter} -> + let inbox_level = Raw_level_repr.of_int32_non_negative inbox_level in + Some (inbox_level, message_counter) + | _ -> None - Implement handling of input logic. - *) + let is_input_state = + let open Monad.Syntax in + let* status = get_status in + match status with | WaitingForInputMessage -> ( - let* level = CurrentLevel.get in - let* counter = MessageCounter.get in - match counter with - | Some n -> return (PS.First_after (level, n)) + let* last_read = get_last_message_read in + match last_read with + | Some (level, n) -> return (PS.First_after (level, n)) | None -> return PS.Initial) - | _ -> return PS.No_input_required + | Computing -> return PS.No_input_required - let is_input_state = - result_of ~default:PS.No_input_required @@ is_input_state_monadic + let is_input_state = result_of is_input_state - let get_status = result_of ~default:Computing @@ Status.get + let get_status : state -> status Lwt.t = result_of get_status - let set_input_monadic input = + let set_input_state input = let open PS in let {inbox_level; message_counter; payload} = input in let open Monad.Syntax in - let* boot_sector = Boot_sector.get in - let msg = boot_sector ^ payload in - let* () = CurrentLevel.set inbox_level in - let* () = MessageCounter.set (Some message_counter) in - let* () = NextMessage.set (Some msg) in - return () + let* s = get in + let* s = + lift + (WASM_machine.set_input_step + { + inbox_level = Raw_level_repr.to_int32_non_negative inbox_level; + message_counter; + } + payload + s) + in + set s - let set_input input = state_of @@ set_input_monadic input + let set_input input = state_of @@ set_input_state input let eval_step = - (* TODO: https://gitlab.com/tezos/tezos/-/issues/3090 - - Call into tickified parsing/evaluation exposed in lib_webassembly. - *) let open Monad.Syntax in let* s = get in - let* s = lift (WASM_machine.step s) in + let* s = lift (WASM_machine.compute_step s) in set s - let ticked m = - let open Monad.Syntax in - let* tick = CurrentTick.get in - let* () = CurrentTick.set (Sc_rollup_tick_repr.next tick) in - m - - let eval state = state_of (ticked eval_step) state + let eval state = state_of eval_step state let step_transition input_given state = let open Lwt_syntax in @@ -434,6 +310,7 @@ module V2_0_0 = struct | None -> fail WASM_proof_production_failed type output_proof = { + output_proof : Context.proof; output_proof_state : hash; output_proof_output : PS.output; } @@ -441,28 +318,63 @@ module V2_0_0 = struct let output_proof_encoding = let open Data_encoding in conv - (fun {output_proof_state; output_proof_output} -> - (output_proof_state, output_proof_output)) - (fun (output_proof_state, output_proof_output) -> - {output_proof_state; output_proof_output}) - (obj2 - (req "output_proof" State_hash.encoding) - (req "output_proof_state" PS.output_encoding)) - - (* FIXME: #3176 - The WASM PVM must provide an implementation for these - proofs. These are likely to be similar to the proofs about the - PVM execution steps. *) + (fun {output_proof; output_proof_state; output_proof_output} -> + (output_proof, output_proof_state, output_proof_output)) + (fun (output_proof, output_proof_state, output_proof_output) -> + {output_proof; output_proof_state; output_proof_output}) + (obj3 + (req "output_proof" Context.proof_encoding) + (req "output_proof_state" State_hash.encoding) + (req "output_proof_output" PS.output_encoding)) + let output_of_output_proof s = s.output_proof_output let state_of_output_proof s = s.output_proof_state - let verify_output_proof _proof = Lwt.return true + let has_output : PS.output -> bool Monad.t = function + | {outbox_level; message_index; message} -> + let open Monad.Syntax in + let* s = get in + let* result = + lift + (WASM_machine.get_output + { + outbox_level = + Raw_level_repr.to_int32_non_negative outbox_level; + message_index; + } + s) + in + let message_encoded = + Data_encoding.Binary.to_string_exn + Sc_rollup_outbox_message_repr.encoding + message + in + return @@ Compare.String.(result = message_encoded) + + let verify_output_proof p = + let open Lwt_syntax in + let transition = run @@ has_output p.output_proof_output in + let* result = Context.verify_proof p.output_proof transition in + match result with None -> return false | Some _ -> return true + + type error += Wasm_output_proof_production_failed - let produce_output_proof _context state output_proof_output = + type error += Wasm_invalid_claim_about_outbox + + let produce_output_proof context state output_proof_output = let open Lwt_result_syntax in let*! output_proof_state = state_hash state in - return {output_proof_state; output_proof_output} + let*! result = + Context.produce_proof context state + @@ run + @@ has_output output_proof_output + in + match result with + | Some (output_proof, true) -> + return {output_proof; output_proof_state; output_proof_output} + | Some (_, false) -> fail Wasm_invalid_claim_about_outbox + | None -> fail Wasm_output_proof_production_failed end module ProtocolImplementation = Make (struct