From 12f81c1bdf86d942c134fae5aeeed0f0023b58cf Mon Sep 17 00:00:00 2001 From: Hans Hoglund Date: Wed, 25 May 2022 11:25:32 +0000 Subject: [PATCH 1/5] SCORU: Wasm PVM: Add skeleton --- src/proto_alpha/lib_protocol/TEZOS_PROTOCOL | 1 + .../lib_protocol/sc_rollup_wasm.ml | 997 ++++++++++++++++++ .../lib_protocol/sc_rollup_wasm.mli | 129 +++ 3 files changed, 1127 insertions(+) create mode 100644 src/proto_alpha/lib_protocol/sc_rollup_wasm.ml create mode 100644 src/proto_alpha/lib_protocol/sc_rollup_wasm.mli diff --git a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL index 6d543cc1a6c0..9ccf4eaca460 100644 --- a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL +++ b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL @@ -192,6 +192,7 @@ "Sc_rollup_operations", "Sc_rollup_PVM_sem", "Sc_rollup_arith", + "Sc_rollup_wasm", "Sc_rollups", "Baking", diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml new file mode 100644 index 000000000000..3590243dec30 --- /dev/null +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml @@ -0,0 +1,997 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2021 Nomadic Labs *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +open Alpha_context +open Sc_rollup + +module type P = sig + module Tree : Context.TREE with type key = string list and type value = bytes + + type tree = Tree.tree + + type proof + + val proof_encoding : proof Data_encoding.t + + val proof_start_state : proof -> State_hash.t + + val proof_stop_state : proof -> State_hash.t + + val verify_proof : + proof -> + (tree -> (tree * 'a) Lwt.t) -> + ( tree * 'a, + [ `Proof_mismatch of string + | `Stream_too_long of string + | `Stream_too_short of string ] ) + result + Lwt.t +end + +module type S = sig + include Sc_rollup_PVM_sem.S + + val name : string + + val parse_boot_sector : string -> string option + + val pp_boot_sector : Format.formatter -> string -> unit + + val pp : state -> (Format.formatter -> unit -> unit) Lwt.t + + val get_tick : state -> Sc_rollup.Tick.t Lwt.t + + type status = Halted | WaitingForInputMessage | Parsing | Evaluating + + val get_status : state -> status Lwt.t + + type instruction = + | IPush : int -> instruction + | IAdd : instruction + | IStore : string -> instruction + + val equal_instruction : instruction -> instruction -> bool + + val pp_instruction : Format.formatter -> instruction -> unit + + val get_parsing_result : state -> bool option Lwt.t + + val get_code : state -> instruction list Lwt.t + + val get_stack : state -> int list Lwt.t + + val get_var : state -> string -> int option Lwt.t + + val get_evaluation_result : state -> bool option Lwt.t + + val get_is_stuck : state -> string option Lwt.t +end + +module Make (Context : P) : + S with type context = Context.Tree.t and type state = Context.tree = struct + module Tree = Context.Tree + + type context = Context.Tree.t + + type hash = State_hash.t + + type proof = Context.proof + + let proof_encoding = Context.proof_encoding + + let proof_start_state = Context.proof_start_state + + let proof_stop_state = Context.proof_stop_state + + let name = "arith" + + let parse_boot_sector s = Some s + + let pp_boot_sector fmt s = Format.fprintf fmt "%s" s + + type tree = Tree.tree + + type status = Halted | WaitingForInputMessage | Parsing | Evaluating + + type instruction = + | IPush : int -> instruction + | IAdd : instruction + | IStore : string -> instruction + + let equal_instruction i1 i2 = + match (i1, i2) with + | IPush x, IPush y -> Compare.Int.(x = y) + | IAdd, IAdd -> true + | IStore x, IStore y -> Compare.String.(x = y) + | _, _ -> false + + let pp_instruction fmt = function + | IPush x -> Format.fprintf fmt "push(%d)" x + | IAdd -> Format.fprintf fmt "add" + | IStore x -> Format.fprintf fmt "store(%s)" x + + (* + + The machine state is represented using a Merkle tree. + + Here is the data model of this state represented in the tree: + + - tick : Tick.t + The current tick counter of the machine. + - status : status + The current status of the machine. + - stack : int deque + The stack of integers. + - next_message : string option + The current input message to be processed. + - code : instruction deque + The instructions parsed from the input message. + - lexer_state : int * int + The internal state of the lexer. + - parsing_state : parsing_state + The internal state of the parser. + - parsing_result : bool option + The outcome of parsing. + - evaluation_result : bool option + The outcome of evaluation. + + *) + module State = struct + type state = tree + + module Monad : sig + type 'a t + + val run : 'a t -> state -> (state * 'a option) Lwt.t + + val is_stuck : string option t + + val internal_error : string -> 'a t + + val return : 'a -> 'a t + + module Syntax : sig + val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t + end + + val remove : Tree.key -> unit t + + val find_value : Tree.key -> 'a Data_encoding.t -> 'a option t + + val children : Tree.key -> 'a Data_encoding.t -> (string * 'a) list t + + val get_value : default:'a -> Tree.key -> 'a Data_encoding.t -> 'a t + + val set_value : Tree.key -> 'a Data_encoding.t -> 'a -> unit t + end = struct + type 'a t = state -> (state * 'a option) Lwt.t + + let return x state = Lwt.return (state, Some 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 + + module Syntax = struct + let ( let* ) = bind + end + + 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 is_stuck tree = + let open Lwt_syntax in + let* v = Tree.find tree internal_error_key in + return (tree, Some (Option.map Bytes.to_string v)) + + let remove key tree = + let open Lwt_syntax in + let* tree = Tree.remove tree key in + return (tree, Some ()) + + 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 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 children key encoding state = + let open Lwt_syntax in + let* children = Tree.list state key in + let rec aux = function + | [] -> return (state, Some []) + | (key, tree) :: children -> ( + let* obytes = Tree.to_value tree in + match obytes with + | None -> internal_error "Invalid children" state + | Some bytes -> ( + let* state, v = decode encoding bytes state in + match v with + | None -> return (state, None) + | Some v -> ( + let* state, l = aux children in + match l with + | None -> return (state, None) + | Some l -> return (state, Some ((key, v) :: l))))) + in + aux children + + let get_value ~default key encoding = + let open Syntax in + let* ov = find_value key encoding in + match ov with None -> return default | Some x -> return x + + 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 pp : Format.formatter -> t -> unit + + val encoding : t Data_encoding.t + end) = + struct + let key = [P.name] + + let create = set_value key P.encoding P.initial + + let get = + let open Monad.Syntax in + let* v = find_value key P.encoding in + match v with + | None -> + (* This case should not happen if [create] is properly called. *) + return P.initial + | Some v -> return v + + let set = set_value key P.encoding + + let pp = + let open Monad.Syntax in + let* v = get in + return @@ fun fmt () -> Format.fprintf fmt "@[%s : %a@]" P.name P.pp v + end + + module MakeDict (P : sig + type t + + val name : string + + val pp : Format.formatter -> t -> unit + + val encoding : t Data_encoding.t + end) = + struct + let key k = [P.name; k] + + let get k = find_value (key k) P.encoding + + let set k v = set_value (key k) P.encoding v + + let pp = + let open Monad.Syntax in + let* l = children [P.name] P.encoding in + let pp_elem fmt (key, value) = + Format.fprintf fmt "@[%s : %a@]" key P.pp value + in + return @@ fun fmt () -> Format.pp_print_list pp_elem fmt l + end + + module MakeDeque (P : sig + type t + + val name : string + + val encoding : t Data_encoding.t + end) = + struct + (* + + A stateful deque. + + [[head; end[] is the index range for the elements of the deque. + + The length of the deque is therefore [end - head]. + + *) + + let head_key = [P.name; "head"] + + let end_key = [P.name; "end"] + + let get_head = get_value ~default:Z.zero head_key Data_encoding.z + + let set_head = set_value head_key Data_encoding.z + + let get_end = get_value ~default:(Z.of_int 0) end_key Data_encoding.z + + let set_end = set_value end_key Data_encoding.z + + let idx_key idx = [P.name; Z.to_string idx] + + let top = + let open Monad.Syntax in + let* head_idx = get_head in + let* end_idx = get_end in + let* v = find_value (idx_key head_idx) P.encoding in + if Z.(leq end_idx head_idx) then return None + else + match v with + | None -> (* By invariants of the Deque. *) assert false + | Some x -> return (Some x) + + let push x = + let open Monad.Syntax in + let* head_idx = get_head in + let head_idx' = Z.pred head_idx in + let* () = set_head head_idx' in + set_value (idx_key head_idx') P.encoding x + + let pop = + let open Monad.Syntax in + let* head_idx = get_head in + let* end_idx = get_end in + if Z.(leq end_idx head_idx) then return None + else + let* v = find_value (idx_key head_idx) P.encoding in + match v with + | None -> (* By invariants of the Deque. *) assert false + | Some x -> + let* () = remove (idx_key head_idx) in + let head_idx = Z.succ head_idx in + let* () = set_head head_idx in + return (Some x) + + let inject x = + let open Monad.Syntax in + let* end_idx = get_end in + let end_idx' = Z.succ end_idx in + let* () = set_end end_idx' in + set_value (idx_key end_idx) P.encoding x + + let to_list = + let open Monad.Syntax in + let* head_idx = get_head in + let* end_idx = get_end in + let rec aux l idx = + if Z.(lt idx head_idx) then return l + else + let* v = find_value (idx_key idx) P.encoding in + match v with + | None -> (* By invariants of deque *) assert false + | Some v -> aux (v :: l) (Z.pred idx) + in + aux [] (Z.pred end_idx) + + let clear = remove [P.name] + end + + module CurrentTick = MakeVar (struct + include Tick + + let name = "tick" + end) + + module Vars = MakeDict (struct + type t = int + + let name = "vars" + + let encoding = Data_encoding.int31 + + let pp fmt x = Format.fprintf fmt "%d" x + end) + + module Stack = MakeDeque (struct + type t = int + + let name = "stack" + + let encoding = Data_encoding.int31 + end) + + module Code = MakeDeque (struct + type t = instruction + + let name = "code" + + let encoding = + Data_encoding.( + union + [ + case + ~title:"push" + (Tag 0) + Data_encoding.int31 + (function IPush x -> Some x | _ -> None) + (fun x -> IPush x); + case + ~title:"add" + (Tag 1) + Data_encoding.unit + (function IAdd -> Some () | _ -> None) + (fun () -> IAdd); + case + ~title:"store" + (Tag 2) + Data_encoding.string + (function IStore x -> Some x | _ -> None) + (fun x -> IStore x); + ]) + 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 = Halted + + let encoding = + Data_encoding.string_enum + [ + ("Halted", Halted); + ("WaitingForInput", WaitingForInputMessage); + ("Parsing", Parsing); + ("Evaluating", Evaluating); + ] + + let name = "status" + + let string_of_status = function + | Halted -> "Halted" + | WaitingForInputMessage -> "WaitingForInputMessage" + | Parsing -> "Parsing" + | Evaluating -> "Evaluating" + + let pp fmt status = Format.fprintf fmt "%s" (string_of_status status) + end) + + module CurrentLevel = MakeVar (struct + type t = Raw_level.t + + let initial = Raw_level.root + + let encoding = Raw_level.encoding + + let name = "current_level" + + let pp = Raw_level.pp + end) + + module MessageCounter = MakeVar (struct + type t = Z.t + + let initial = Z.(pred zero) + + let encoding = Data_encoding.n + + let name = "message_counter" + + let pp = Z.pp_print + 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) + + type parser_state = ParseInt | ParseVar | SkipLayout + + module LexerState = MakeVar (struct + type t = int * int + + let name = "lexer_buffer" + + let initial = (-1, -1) + + let encoding = Data_encoding.(tup2 int31 int31) + + let pp fmt (start, len) = + Format.fprintf fmt "lexer.(start = %d, len = %d)" start len + end) + + module ParserState = MakeVar (struct + type t = parser_state + + let name = "parser_state" + + let initial = SkipLayout + + let encoding = + Data_encoding.string_enum + [ + ("ParseInt", ParseInt); + ("ParseVar", ParseVar); + ("SkipLayout", SkipLayout); + ] + + let pp fmt = function + | ParseInt -> Format.fprintf fmt "Parsing int" + | ParseVar -> Format.fprintf fmt "Parsing var" + | SkipLayout -> Format.fprintf fmt "Skipping layout" + end) + + module ParsingResult = MakeVar (struct + type t = bool option + + let name = "parsing_result" + + let initial = None + + let encoding = Data_encoding.(option bool) + + let pp fmt = function + | None -> Format.fprintf fmt "n/a" + | Some true -> Format.fprintf fmt "parsing succeeds" + | Some false -> Format.fprintf fmt "parsing fails" + end) + + module EvaluationResult = MakeVar (struct + type t = bool option + + let name = "evaluation_result" + + let initial = None + + let encoding = Data_encoding.(option bool) + + let pp fmt = function + | None -> Format.fprintf fmt "n/a" + | Some true -> Format.fprintf fmt "evaluation succeeds" + | Some false -> Format.fprintf fmt "evaluation fails" + end) + + let pp = + let open Monad.Syntax in + let* status_pp = Status.pp in + let* message_counter_pp = MessageCounter.pp in + let* next_message_pp = NextMessage.pp in + let* parsing_result_pp = ParsingResult.pp in + let* parser_state_pp = ParserState.pp in + let* lexer_state_pp = LexerState.pp in + let* evaluation_result_pp = EvaluationResult.pp in + let* vars_pp = Vars.pp in + return @@ fun fmt () -> + Format.fprintf + fmt + "@[@;%a@;%a@;%a@;%a@;%a@;%a@;%a@;%a@]" + status_pp + () + message_counter_pp + () + next_message_pp + () + parsing_result_pp + () + parser_state_pp + () + lexer_state_pp + () + evaluation_result_pp + () + vars_pp + () + end + + open State + + type state = State.state + + let pp state = + let open Lwt_syntax in + let* _, pp = Monad.run pp state in + match pp with + | None -> return @@ fun fmt _ -> Format.fprintf fmt "" + | Some pp -> return pp + + open Monad + + let initial_state ctxt boot_sector = + let state = Tree.empty ctxt in + let m = + let open Monad.Syntax in + let* () = Boot_sector.set boot_sector in + let* () = Status.set Halted in + return () + in + let open Lwt_syntax in + let* state, _ = run m state in + return state + + let state_hash state = + let m = + let open Monad.Syntax in + let* status = Status.get in + match status with + | Halted -> return State_hash.zero + | _ -> + 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 + + let boot = + let open Monad.Syntax in + let* () = Status.create in + let* () = NextMessage.create in + let* () = Status.set WaitingForInputMessage in + return () + + let result_of ~default m state = + let open Lwt_syntax in + let* _, v = run m state in + match v with None -> return default | Some 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:Tick.initial CurrentTick.get + + let is_input_state_monadic = + let open Monad.Syntax in + let* status = Status.get in + match status with + | WaitingForInputMessage -> + let* level = CurrentLevel.get in + let* counter = MessageCounter.get in + return (Some (level, counter)) + | _ -> return None + + let is_input_state = result_of ~default:None @@ is_input_state_monadic + + let get_status = result_of ~default:WaitingForInputMessage @@ Status.get + + let get_code = result_of ~default:[] @@ Code.to_list + + let get_parsing_result = result_of ~default:None @@ ParsingResult.get + + let get_stack = result_of ~default:[] @@ Stack.to_list + + let get_var state k = (result_of ~default:None @@ Vars.get k) state + + let get_evaluation_result = result_of ~default:None @@ EvaluationResult.get + + let get_is_stuck = result_of ~default:None @@ is_stuck + + let set_input_monadic input = + let open Sc_rollup_PVM_sem 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* last_level = CurrentLevel.get in + let* last_counter = MessageCounter.get in + let update = + let* () = CurrentLevel.set inbox_level in + let* () = MessageCounter.set message_counter in + let* () = NextMessage.set (Some msg) in + return () + in + let does_not_follow = + internal_error "The input message does not follow the previous one." + in + if Raw_level.(equal last_level inbox_level) then + if Z.(equal message_counter (succ last_counter)) then update + else does_not_follow + else if Raw_level.(last_level < inbox_level) then + if Z.(equal message_counter Z.zero) then update else does_not_follow + else does_not_follow + + let set_input input = state_of @@ set_input_monadic input + + let next_char = + let open Monad.Syntax in + LexerState.( + let* start, len = get in + set (start, len + 1)) + + let no_message_to_lex () = + internal_error "lexer: There is no input message to lex" + + let current_char = + let open Monad.Syntax in + let* start, len = LexerState.get in + let* msg = NextMessage.get in + match msg with + | None -> no_message_to_lex () + | Some s -> + if Compare.Int.(start + len < String.length s) then + return (Some s.[start + len]) + else return None + + let lexeme = + let open Monad.Syntax in + let* start, len = LexerState.get in + let* msg = NextMessage.get in + match msg with + | None -> no_message_to_lex () + | Some s -> + let* () = LexerState.set (start + len, 0) in + return (String.sub s start len) + + let push_int_literal = + let open Monad.Syntax in + let* s = lexeme in + match int_of_string_opt s with + | Some x -> Code.inject (IPush x) + | None -> (* By validity of int parsing. *) assert false + + let push_var = + let open Monad.Syntax in + let* s = lexeme in + Code.inject (IStore s) + + let start_parsing : unit t = + let open Monad.Syntax in + let* () = Status.set Parsing in + let* () = ParsingResult.set None in + let* () = ParserState.set SkipLayout in + let* () = LexerState.set (0, 0) in + let* () = Status.set Parsing in + let* () = Code.clear in + return () + + let start_evaluating : unit t = + let open Monad.Syntax in + let* () = EvaluationResult.set None in + let* () = Stack.clear in + let* () = Status.set Evaluating in + return () + + let stop_parsing outcome = + let open Monad.Syntax in + let* () = ParsingResult.set (Some outcome) in + start_evaluating + + let stop_evaluating outcome = + let open Monad.Syntax in + let* () = EvaluationResult.set (Some outcome) in + Status.set WaitingForInputMessage + + let parse : unit t = + let open Monad.Syntax in + let produce_add = + let* _ = lexeme in + let* () = next_char in + let* () = Code.inject IAdd in + return () + in + let produce_int = + let* () = push_int_literal in + let* () = ParserState.set SkipLayout in + return () + in + let produce_var = + let* () = push_var in + let* () = ParserState.set SkipLayout in + return () + in + let is_digit d = Compare.Char.(d >= '0' && d <= '9') in + let is_letter d = Compare.Char.(d >= 'a' && d <= 'z') in + let* parser_state = ParserState.get in + match parser_state with + | ParseInt -> ( + let* char = current_char in + match char with + | Some d when is_digit d -> next_char + | Some '+' -> + let* () = produce_int in + let* () = produce_add in + return () + | Some ' ' -> + let* () = produce_int in + let* () = next_char in + return () + | None -> + let* () = push_int_literal in + stop_parsing true + | _ -> stop_parsing false) + | ParseVar -> ( + let* char = current_char in + match char with + | Some d when is_letter d -> next_char + | Some '+' -> + let* () = produce_var in + let* () = produce_add in + return () + | Some ' ' -> + let* () = produce_var in + let* () = next_char in + return () + | None -> + let* () = push_var in + stop_parsing true + | _ -> stop_parsing false) + | SkipLayout -> ( + let* char = current_char in + match char with + | Some ' ' -> next_char + | Some '+' -> produce_add + | Some d when is_digit d -> + let* _ = lexeme in + let* () = next_char in + let* () = ParserState.set ParseInt in + return () + | Some d when is_letter d -> + let* _ = lexeme in + let* () = next_char in + let* () = ParserState.set ParseVar in + return () + | None -> stop_parsing true + | _ -> stop_parsing false) + + let evaluate = + let open Monad.Syntax in + let* i = Code.pop in + match i with + | None -> stop_evaluating true + | Some (IPush x) -> Stack.push x + | Some (IStore x) -> ( + let* v = Stack.top in + match v with None -> stop_evaluating false | Some v -> Vars.set x v) + | Some IAdd -> ( + let* v = Stack.pop in + match v with + | None -> stop_evaluating false + | Some x -> ( + let* v = Stack.pop in + match v with + | None -> stop_evaluating false + | Some y -> Stack.push (x + y))) + + let reboot = + let open Monad.Syntax in + let* () = Status.set WaitingForInputMessage in + let* () = Stack.clear in + let* () = Code.clear in + return () + + let eval_step = + let open Monad.Syntax in + let* x = is_stuck in + match x with + | Some _ -> reboot + | None -> ( + let* status = Status.get in + match status with + | Halted -> boot + | WaitingForInputMessage -> ( + let* msg = NextMessage.get in + match msg with + | None -> + internal_error + "An input state was not provided an input message." + | Some _ -> start_parsing) + | Parsing -> parse + | Evaluating -> evaluate) + + let ticked m = + let open Monad.Syntax in + let* tick = CurrentTick.get in + let* () = CurrentTick.set (Tick.next tick) in + m + + let eval state = state_of (ticked eval_step) state + + let verify_proof ~input proof = + let open Lwt_syntax in + let transition state = + let* state = + match input with + | None -> eval state + | Some input -> state_of (ticked (set_input_monadic input)) state + in + return (state, ()) + in + let* x = Context.verify_proof proof transition in + match x with Ok _ -> return_true | Error _ -> return_false +end + +module ProtocolImplementation = Make (struct + module Tree = struct + include Context.Tree + + type tree = Context.tree + + type t = Context.t + + type key = string list + + type value = bytes + end + + type tree = Context.tree + + type proof = Context.Proof.tree Context.Proof.t + + let verify_proof = Context.verify_tree_proof + + let kinded_hash_to_state_hash = function + | `Value hash | `Node hash -> + State_hash.hash_bytes [Context_hash.to_bytes hash] + + let proof_start_state proof = + kinded_hash_to_state_hash proof.Context.Proof.before + + let proof_stop_state proof = + kinded_hash_to_state_hash proof.Context.Proof.after + + let proof_encoding = Context.Proof_encoding.V2.Tree32.tree_proof_encoding +end) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli new file mode 100644 index 000000000000..331d29e0265b --- /dev/null +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli @@ -0,0 +1,129 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2021 Nomadic Labs *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +(** This module providess Proof-Generating Virtual Machine (PVM) running + WebAssembly. *) + +open Alpha_context + +module type S = sig + include Sc_rollup_PVM_sem.S + + (** [name] is "wasm_2_0_0". + + WebAssembly is an "evergreen" specification. We aim to track + the latest major version, 2.0 at the time of writing. + *) + val name : string + + (** [parse_boot_sector s] builds a boot sector from its human + writable description. *) + val parse_boot_sector : string -> string option + + (** [pp_boot_sector fmt s] prints a human readable representation of + a boot sector. *) + val pp_boot_sector : Format.formatter -> string -> unit + + (** [pp state] returns a pretty-printer valid for [state]. *) + val pp : state -> (Format.formatter -> unit -> unit) Lwt.t + + (** [get_tick state] returns the current tick of [state]. *) + val get_tick : state -> Sc_rollup.Tick.t Lwt.t + + (** The machine has three possible states: *) + type status = Halted | WaitingForInputMessage | Parsing | Evaluating + + (** [get_status state] returns the machine status in [state]. *) + val get_status : state -> status Lwt.t + + (** The machine has only three instructions. *) + type instruction = + | IPush : int -> instruction + | IAdd : instruction + | IStore : string -> instruction + + (** [equal_instruction i1 i2] is [true] iff [i1] equals [i2]. *) + val equal_instruction : instruction -> instruction -> bool + + (** [pp_instruction fmt i] shows a human readable representation of [i]. *) + val pp_instruction : Format.formatter -> instruction -> unit + + (** [get_parsing_result state] is [Some true] if the current + message is syntactically correct, [Some false] when it + contains a syntax error, and [None] when the machine is + not in parsing state. *) + val get_parsing_result : state -> bool option Lwt.t + + (** [get_code state] returns the current code obtained by parsing + the current input message. *) + val get_code : state -> instruction list Lwt.t + + (** [get_stack state] returns the current stack. *) + val get_stack : state -> int list Lwt.t + + (** [get_var state x] returns the current value of variable [x]. + Returns [None] if [x] does not exist. *) + val get_var : state -> string -> int option Lwt.t + + (** [get_evaluation_result state] returns [Some true] if the current + message evaluation succeeds, [Some false] if it failed, and + [None] if the evaluation has not been done yet. *) + val get_evaluation_result : state -> bool option Lwt.t + + (** [get_is_stuck state] returns [Some err] if some internal error + made the machine fail during the last evaluation step. [None] + if no internal error occurred. When a machine is stuck, it + reboots, waiting for the next message to process. *) + val get_is_stuck : state -> string option Lwt.t +end + +module ProtocolImplementation : S with type context = Context.t + +module type P = sig + module Tree : Context.TREE with type key = string list and type value = bytes + + type tree = Tree.tree + + type proof + + val proof_encoding : proof Data_encoding.t + + val proof_start_state : proof -> Sc_rollup.State_hash.t + + val proof_stop_state : proof -> Sc_rollup.State_hash.t + + val verify_proof : + proof -> + (tree -> (tree * 'a) Lwt.t) -> + ( tree * 'a, + [ `Proof_mismatch of string + | `Stream_too_long of string + | `Stream_too_short of string ] ) + result + Lwt.t +end + +module Make (Context : P) : + S with type context = Context.Tree.t and type state = Context.tree -- GitLab From eb40c9004d7a51b76c615e97a16c9cfe9f4ef3bc Mon Sep 17 00:00:00 2001 From: Hans Hoglund Date: Tue, 17 May 2022 12:21:07 +0000 Subject: [PATCH 2/5] wip --- src/proto_alpha/lib_protocol/sc_rollup_repr.ml | 13 +++++++++++-- src/proto_alpha/lib_protocol/sc_rollup_repr.mli | 2 +- src/proto_alpha/lib_protocol/sc_rollup_wasm.mli | 3 ++- src/proto_alpha/lib_protocol/sc_rollups.ml | 4 ++-- 4 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml index 3a9b343ded22..d77c8dda497a 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml @@ -211,7 +211,7 @@ module Kind = struct - to update [Sc_rollups.kind_of_string] and [encoding]. *) - type t = Example_arith + type t = Example_arith | Wasm_2_0_0 let example_arith_case = Data_encoding.( @@ -222,7 +222,16 @@ module Kind = struct (function Example_arith -> Some ()) (fun () -> Example_arith)) - let encoding = Data_encoding.union ~tag_size:`Uint16 [example_arith_case] + let wasm_2_0_0 = + Data_encoding.( + case + ~title:"Wasm 2.0.0 smart contract rollup kind" + (Tag 0) + unit + (function Wasm_2_0_0 -> Some ()) + (fun () -> Wasm_2_0_0)) + + let encoding = Data_encoding.union ~tag_size:`Uint16 [example_arith_case; wasm_2_0_0_case] let equal x y = match (x, y) with Example_arith, Example_arith -> true diff --git a/src/proto_alpha/lib_protocol/sc_rollup_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_repr.mli index 2f7229e31336..aa44bd58b79f 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.mli @@ -97,7 +97,7 @@ module Kind : sig This list must only be appended for backward compatibility. *) - type t = Example_arith + type t = Example_arith | Wasm_2_0_0 val encoding : t Data_encoding.t diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli index 331d29e0265b..5682591ef90c 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli @@ -34,7 +34,8 @@ module type S = sig (** [name] is "wasm_2_0_0". WebAssembly is an "evergreen" specification. We aim to track - the latest major version, 2.0 at the time of writing. + the latest major version, 2.0 at the time of writing. We + use the minor version number to track changes to our fork. *) val name : string diff --git a/src/proto_alpha/lib_protocol/sc_rollups.ml b/src/proto_alpha/lib_protocol/sc_rollups.ml index 6383f16562ff..c1430ab8c3aa 100644 --- a/src/proto_alpha/lib_protocol/sc_rollups.ml +++ b/src/proto_alpha/lib_protocol/sc_rollups.ml @@ -41,9 +41,9 @@ module PVM = struct type t = (module S) end -let all = [Kind.Example_arith] +let all = [Kind.Example_arith, Kind.Wasm_2_0_0] -let kind_of_string = function "arith" -> Some Kind.Example_arith | _ -> None +let kind_of_string = function "arith" -> Some Kind.Example_arith | "wasm_2_0_0" -> Wasm_2_0_0 | _ -> None let example_arith_pvm = (module Sc_rollup_arith.ProtocolImplementation : PVM.S) -- GitLab From 334252a2b80fbd861afdc6d06a35a7e7379381bc Mon Sep 17 00:00:00 2001 From: Hans Hoglund Date: Tue, 17 May 2022 12:38:02 +0000 Subject: [PATCH 3/5] wip --- src/proto_alpha/lib_protocol/alpha_context.mli | 2 +- src/proto_alpha/lib_protocol/sc_rollup_repr.ml | 17 +++++++++++------ src/proto_alpha/lib_protocol/sc_rollup_wasm.ml | 4 ++++ src/proto_alpha/lib_protocol/sc_rollup_wasm.mli | 5 +++++ src/proto_alpha/lib_protocol/sc_rollups.ml | 9 ++++++--- 5 files changed, 27 insertions(+), 10 deletions(-) diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index 6e8973dd8927..77c2ae155115 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -2477,7 +2477,7 @@ module Sc_rollup : sig type rollup := t module Kind : sig - type t = Example_arith + type t = Example_arith | Wasm_2_0_0 val encoding : t Data_encoding.t end diff --git a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml index d77c8dda497a..af84d6031eff 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml @@ -219,22 +219,27 @@ module Kind = struct ~title:"Example_arith smart contract rollup kind" (Tag 0) unit - (function Example_arith -> Some ()) + (function Example_arith -> Some () | _ -> None) (fun () -> Example_arith)) - let wasm_2_0_0 = + let wasm_2_0_0_case = Data_encoding.( case ~title:"Wasm 2.0.0 smart contract rollup kind" - (Tag 0) + (Tag 1) unit - (function Wasm_2_0_0 -> Some ()) + (function Wasm_2_0_0 -> Some () | _ -> None) (fun () -> Wasm_2_0_0)) let encoding = Data_encoding.union ~tag_size:`Uint16 [example_arith_case; wasm_2_0_0_case] - let equal x y = match (x, y) with Example_arith, Example_arith -> true + let equal x y = match (x, y) with + | Example_arith, Example_arith -> true + | Wasm_2_0_0, Wasm_2_0_0 -> true + | _ -> false let pp fmt kind = - match kind with Example_arith -> Format.fprintf fmt "Example_arith" + match kind with + | Example_arith -> Format.fprintf fmt "Example_arith" + | Wasm_2_0_0 -> Format.fprintf fmt "Wasm_2_0_0" end diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml index 3590243dec30..55e4e155c35b 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml @@ -23,6 +23,8 @@ (* *) (*****************************************************************************) +module V2_0_0 = struct + open Alpha_context open Sc_rollup @@ -995,3 +997,5 @@ module ProtocolImplementation = Make (struct let proof_encoding = Context.Proof_encoding.V2.Tree32.tree_proof_encoding end) + +end diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli index 5682591ef90c..b255c5fe3107 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli @@ -23,11 +23,14 @@ (* *) (*****************************************************************************) +module V2_0_0 : sig + (** This module providess Proof-Generating Virtual Machine (PVM) running WebAssembly. *) open Alpha_context + module type S = sig include Sc_rollup_PVM_sem.S @@ -128,3 +131,5 @@ end module Make (Context : P) : S with type context = Context.Tree.t and type state = Context.tree + +end diff --git a/src/proto_alpha/lib_protocol/sc_rollups.ml b/src/proto_alpha/lib_protocol/sc_rollups.ml index c1430ab8c3aa..f8f3cba07e09 100644 --- a/src/proto_alpha/lib_protocol/sc_rollups.ml +++ b/src/proto_alpha/lib_protocol/sc_rollups.ml @@ -41,13 +41,16 @@ module PVM = struct type t = (module S) end -let all = [Kind.Example_arith, Kind.Wasm_2_0_0] +let all = [Kind.Example_arith; Kind.Wasm_2_0_0] -let kind_of_string = function "arith" -> Some Kind.Example_arith | "wasm_2_0_0" -> Wasm_2_0_0 | _ -> None +let kind_of_string = function "arith" -> Some Kind.Example_arith | "wasm_2_0_0" -> Some Wasm_2_0_0 | _ -> None let example_arith_pvm = (module Sc_rollup_arith.ProtocolImplementation : PVM.S) +let wasm_2_0_0_pvm = (module Sc_rollup_wasm.V2_0_0.ProtocolImplementation : PVM.S) -let of_kind = function Kind.Example_arith -> example_arith_pvm +let of_kind = function + | Kind.Example_arith -> example_arith_pvm + | Kind.Wasm_2_0_0 -> wasm_2_0_0_pvm let kind_of (module M : PVM.S) = match kind_of_string M.name with -- GitLab From e1230be1b17bf7aff9a1a3a428242bc5bf3ee98f Mon Sep 17 00:00:00 2001 From: Hans Hoglund Date: Tue, 17 May 2022 12:40:12 +0000 Subject: [PATCH 4/5] fmt --- .../lib_protocol/sc_rollup_repr.ml | 10 +- .../lib_protocol/sc_rollup_wasm.ml | 1545 +++++++++-------- .../lib_protocol/sc_rollup_wasm.mli | 124 +- src/proto_alpha/lib_protocol/sc_rollups.ml | 13 +- 4 files changed, 849 insertions(+), 843 deletions(-) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml index af84d6031eff..306a670de157 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml @@ -231,15 +231,17 @@ module Kind = struct (function Wasm_2_0_0 -> Some () | _ -> None) (fun () -> Wasm_2_0_0)) - let encoding = Data_encoding.union ~tag_size:`Uint16 [example_arith_case; wasm_2_0_0_case] + let encoding = + Data_encoding.union ~tag_size:`Uint16 [example_arith_case; wasm_2_0_0_case] - let equal x y = match (x, y) with + let equal x y = + match (x, y) with | Example_arith, Example_arith -> true | Wasm_2_0_0, Wasm_2_0_0 -> true | _ -> false let pp fmt kind = match kind with - | Example_arith -> Format.fprintf fmt "Example_arith" - | Wasm_2_0_0 -> Format.fprintf fmt "Wasm_2_0_0" + | Example_arith -> Format.fprintf fmt "Example_arith" + | Wasm_2_0_0 -> Format.fprintf fmt "Wasm_2_0_0" end diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml index 55e4e155c35b..5f44c9c4b09d 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml @@ -24,117 +24,117 @@ (*****************************************************************************) module V2_0_0 = struct + open Alpha_context + open Sc_rollup -open Alpha_context -open Sc_rollup + module type P = sig + module Tree : + Context.TREE with type key = string list and type value = bytes -module type P = sig - module Tree : Context.TREE with type key = string list and type value = bytes + type tree = Tree.tree - type tree = Tree.tree + type proof - type proof + val proof_encoding : proof Data_encoding.t - val proof_encoding : proof Data_encoding.t + val proof_start_state : proof -> State_hash.t - val proof_start_state : proof -> State_hash.t + val proof_stop_state : proof -> State_hash.t - val proof_stop_state : proof -> State_hash.t - - val verify_proof : - proof -> - (tree -> (tree * 'a) Lwt.t) -> - ( tree * 'a, - [ `Proof_mismatch of string - | `Stream_too_long of string - | `Stream_too_short of string ] ) - result - Lwt.t -end + val verify_proof : + proof -> + (tree -> (tree * 'a) Lwt.t) -> + ( tree * 'a, + [ `Proof_mismatch of string + | `Stream_too_long of string + | `Stream_too_short of string ] ) + result + Lwt.t + end -module type S = sig - include Sc_rollup_PVM_sem.S + module type S = sig + include Sc_rollup_PVM_sem.S - val name : string + val name : string - val parse_boot_sector : string -> string option + val parse_boot_sector : string -> string option - val pp_boot_sector : Format.formatter -> string -> unit + val pp_boot_sector : Format.formatter -> string -> unit - val pp : state -> (Format.formatter -> unit -> unit) Lwt.t + val pp : state -> (Format.formatter -> unit -> unit) Lwt.t - val get_tick : state -> Sc_rollup.Tick.t Lwt.t + val get_tick : state -> Sc_rollup.Tick.t Lwt.t - type status = Halted | WaitingForInputMessage | Parsing | Evaluating + type status = Halted | WaitingForInputMessage | Parsing | Evaluating - val get_status : state -> status Lwt.t + val get_status : state -> status Lwt.t - type instruction = - | IPush : int -> instruction - | IAdd : instruction - | IStore : string -> instruction + type instruction = + | IPush : int -> instruction + | IAdd : instruction + | IStore : string -> instruction - val equal_instruction : instruction -> instruction -> bool + val equal_instruction : instruction -> instruction -> bool - val pp_instruction : Format.formatter -> instruction -> unit + val pp_instruction : Format.formatter -> instruction -> unit - val get_parsing_result : state -> bool option Lwt.t + val get_parsing_result : state -> bool option Lwt.t - val get_code : state -> instruction list Lwt.t + val get_code : state -> instruction list Lwt.t - val get_stack : state -> int list Lwt.t + val get_stack : state -> int list Lwt.t - val get_var : state -> string -> int option Lwt.t + val get_var : state -> string -> int option Lwt.t - val get_evaluation_result : state -> bool option Lwt.t + val get_evaluation_result : state -> bool option Lwt.t - val get_is_stuck : state -> string option Lwt.t -end + val get_is_stuck : state -> string option Lwt.t + end -module Make (Context : P) : - S with type context = Context.Tree.t and type state = Context.tree = struct - module Tree = Context.Tree + module Make (Context : P) : + S with type context = Context.Tree.t and type state = Context.tree = struct + module Tree = Context.Tree - type context = Context.Tree.t + type context = Context.Tree.t - type hash = State_hash.t + type hash = State_hash.t - type proof = Context.proof + type proof = Context.proof - let proof_encoding = Context.proof_encoding + let proof_encoding = Context.proof_encoding - let proof_start_state = Context.proof_start_state + let proof_start_state = Context.proof_start_state - let proof_stop_state = Context.proof_stop_state + let proof_stop_state = Context.proof_stop_state - let name = "arith" + let name = "arith" - let parse_boot_sector s = Some s + let parse_boot_sector s = Some s - let pp_boot_sector fmt s = Format.fprintf fmt "%s" s + let pp_boot_sector fmt s = Format.fprintf fmt "%s" s - type tree = Tree.tree + type tree = Tree.tree - type status = Halted | WaitingForInputMessage | Parsing | Evaluating + type status = Halted | WaitingForInputMessage | Parsing | Evaluating - type instruction = - | IPush : int -> instruction - | IAdd : instruction - | IStore : string -> instruction + type instruction = + | IPush : int -> instruction + | IAdd : instruction + | IStore : string -> instruction - let equal_instruction i1 i2 = - match (i1, i2) with - | IPush x, IPush y -> Compare.Int.(x = y) - | IAdd, IAdd -> true - | IStore x, IStore y -> Compare.String.(x = y) - | _, _ -> false + let equal_instruction i1 i2 = + match (i1, i2) with + | IPush x, IPush y -> Compare.Int.(x = y) + | IAdd, IAdd -> true + | IStore x, IStore y -> Compare.String.(x = y) + | _, _ -> false - let pp_instruction fmt = function - | IPush x -> Format.fprintf fmt "push(%d)" x - | IAdd -> Format.fprintf fmt "add" - | IStore x -> Format.fprintf fmt "store(%s)" x + let pp_instruction fmt = function + | IPush x -> Format.fprintf fmt "push(%d)" x + | IAdd -> Format.fprintf fmt "add" + | IStore x -> Format.fprintf fmt "store(%s)" x - (* + (* The machine state is represented using a Merkle tree. @@ -160,842 +160,843 @@ module Make (Context : P) : The outcome of evaluation. *) - module State = struct - type state = tree + module State = struct + type state = tree + + module Monad : sig + type 'a t + + val run : 'a t -> state -> (state * 'a option) Lwt.t + + val is_stuck : string option t + + val internal_error : string -> 'a t + + val return : 'a -> 'a t + + module Syntax : sig + val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t + end + + val remove : Tree.key -> unit t + + val find_value : Tree.key -> 'a Data_encoding.t -> 'a option t + + val children : Tree.key -> 'a Data_encoding.t -> (string * 'a) list t + + val get_value : default:'a -> Tree.key -> 'a Data_encoding.t -> 'a t + + val set_value : Tree.key -> 'a Data_encoding.t -> 'a -> unit t + end = struct + type 'a t = state -> (state * 'a option) Lwt.t + + let return x state = Lwt.return (state, Some 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 + + module Syntax = struct + let ( let* ) = bind + end + + 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 is_stuck tree = + let open Lwt_syntax in + let* v = Tree.find tree internal_error_key in + return (tree, Some (Option.map Bytes.to_string v)) + + let remove key tree = + let open Lwt_syntax in + let* tree = Tree.remove tree key in + return (tree, Some ()) + + 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 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 children key encoding state = + let open Lwt_syntax in + let* children = Tree.list state key in + let rec aux = function + | [] -> return (state, Some []) + | (key, tree) :: children -> ( + let* obytes = Tree.to_value tree in + match obytes with + | None -> internal_error "Invalid children" state + | Some bytes -> ( + let* state, v = decode encoding bytes state in + match v with + | None -> return (state, None) + | Some v -> ( + let* state, l = aux children in + match l with + | None -> return (state, None) + | Some l -> return (state, Some ((key, v) :: l))))) + in + aux children + + let get_value ~default key encoding = + let open Syntax in + let* ov = find_value key encoding in + match ov with None -> return default | Some x -> return x + + 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 - module Monad : sig - type 'a t + open Monad - val run : 'a t -> state -> (state * 'a option) Lwt.t + module MakeVar (P : sig + type t - val is_stuck : string option t + val name : string - val internal_error : string -> 'a t + val initial : t - val return : 'a -> 'a t + val pp : Format.formatter -> t -> unit - module Syntax : sig - val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t - end + val encoding : t Data_encoding.t + end) = + struct + let key = [P.name] - val remove : Tree.key -> unit t + let create = set_value key P.encoding P.initial - val find_value : Tree.key -> 'a Data_encoding.t -> 'a option t + let get = + let open Monad.Syntax in + let* v = find_value key P.encoding in + match v with + | None -> + (* This case should not happen if [create] is properly called. *) + return P.initial + | Some v -> return v - val children : Tree.key -> 'a Data_encoding.t -> (string * 'a) list t + let set = set_value key P.encoding - val get_value : default:'a -> Tree.key -> 'a Data_encoding.t -> 'a t + let pp = + let open Monad.Syntax in + let* v = get in + return @@ fun fmt () -> Format.fprintf fmt "@[%s : %a@]" P.name P.pp v + end - val set_value : Tree.key -> 'a Data_encoding.t -> 'a -> unit t - end = struct - type 'a t = state -> (state * 'a option) Lwt.t + module MakeDict (P : sig + type t - let return x state = Lwt.return (state, Some x) + val name : string - 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 + val pp : Format.formatter -> t -> unit - module Syntax = struct - let ( let* ) = bind - end + val encoding : t Data_encoding.t + end) = + struct + let key k = [P.name; k] - 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 is_stuck tree = - let open Lwt_syntax in - let* v = Tree.find tree internal_error_key in - return (tree, Some (Option.map Bytes.to_string v)) - - let remove key tree = - let open Lwt_syntax in - let* tree = Tree.remove tree key in - return (tree, Some ()) - - 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 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 children key encoding state = - let open Lwt_syntax in - let* children = Tree.list state key in - let rec aux = function - | [] -> return (state, Some []) - | (key, tree) :: children -> ( - let* obytes = Tree.to_value tree in - match obytes with - | None -> internal_error "Invalid children" state - | Some bytes -> ( - let* state, v = decode encoding bytes state in - match v with - | None -> return (state, None) - | Some v -> ( - let* state, l = aux children in - match l with - | None -> return (state, None) - | Some l -> return (state, Some ((key, v) :: l))))) - in - aux children - - let get_value ~default key encoding = - let open Syntax in - let* ov = find_value key encoding in - match ov with None -> return default | Some x -> return x - - 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 + let get k = find_value (key k) P.encoding - open Monad + let set k v = set_value (key k) P.encoding v - module MakeVar (P : sig - type t + let pp = + let open Monad.Syntax in + let* l = children [P.name] P.encoding in + let pp_elem fmt (key, value) = + Format.fprintf fmt "@[%s : %a@]" key P.pp value + in + return @@ fun fmt () -> Format.pp_print_list pp_elem fmt l + end - val name : string + module MakeDeque (P : sig + type t - val initial : t + val name : string - val pp : Format.formatter -> t -> unit + val encoding : t Data_encoding.t + end) = + struct + (* - val encoding : t Data_encoding.t - end) = - struct - let key = [P.name] + A stateful deque. - let create = set_value key P.encoding P.initial + [[head; end[] is the index range for the elements of the deque. - let get = - let open Monad.Syntax in - let* v = find_value key P.encoding in - match v with - | None -> - (* This case should not happen if [create] is properly called. *) - return P.initial - | Some v -> return v + The length of the deque is therefore [end - head]. - let set = set_value key P.encoding + *) - let pp = - let open Monad.Syntax in - let* v = get in - return @@ fun fmt () -> Format.fprintf fmt "@[%s : %a@]" P.name P.pp v - end + let head_key = [P.name; "head"] - module MakeDict (P : sig - type t + let end_key = [P.name; "end"] - val name : string + let get_head = get_value ~default:Z.zero head_key Data_encoding.z - val pp : Format.formatter -> t -> unit + let set_head = set_value head_key Data_encoding.z - val encoding : t Data_encoding.t - end) = - struct - let key k = [P.name; k] + let get_end = get_value ~default:(Z.of_int 0) end_key Data_encoding.z - let get k = find_value (key k) P.encoding + let set_end = set_value end_key Data_encoding.z - let set k v = set_value (key k) P.encoding v + let idx_key idx = [P.name; Z.to_string idx] - let pp = - let open Monad.Syntax in - let* l = children [P.name] P.encoding in - let pp_elem fmt (key, value) = - Format.fprintf fmt "@[%s : %a@]" key P.pp value - in - return @@ fun fmt () -> Format.pp_print_list pp_elem fmt l - end + let top = + let open Monad.Syntax in + let* head_idx = get_head in + let* end_idx = get_end in + let* v = find_value (idx_key head_idx) P.encoding in + if Z.(leq end_idx head_idx) then return None + else + match v with + | None -> (* By invariants of the Deque. *) assert false + | Some x -> return (Some x) + + let push x = + let open Monad.Syntax in + let* head_idx = get_head in + let head_idx' = Z.pred head_idx in + let* () = set_head head_idx' in + set_value (idx_key head_idx') P.encoding x + + let pop = + let open Monad.Syntax in + let* head_idx = get_head in + let* end_idx = get_end in + if Z.(leq end_idx head_idx) then return None + else + let* v = find_value (idx_key head_idx) P.encoding in + match v with + | None -> (* By invariants of the Deque. *) assert false + | Some x -> + let* () = remove (idx_key head_idx) in + let head_idx = Z.succ head_idx in + let* () = set_head head_idx in + return (Some x) + + let inject x = + let open Monad.Syntax in + let* end_idx = get_end in + let end_idx' = Z.succ end_idx in + let* () = set_end end_idx' in + set_value (idx_key end_idx) P.encoding x + + let to_list = + let open Monad.Syntax in + let* head_idx = get_head in + let* end_idx = get_end in + let rec aux l idx = + if Z.(lt idx head_idx) then return l + else + let* v = find_value (idx_key idx) P.encoding in + match v with + | None -> (* By invariants of deque *) assert false + | Some v -> aux (v :: l) (Z.pred idx) + in + aux [] (Z.pred end_idx) + + let clear = remove [P.name] + end - module MakeDeque (P : sig - type t + module CurrentTick = MakeVar (struct + include Tick - val name : string + let name = "tick" + end) - val encoding : t Data_encoding.t - end) = - struct - (* + module Vars = MakeDict (struct + type t = int - A stateful deque. + let name = "vars" - [[head; end[] is the index range for the elements of the deque. + let encoding = Data_encoding.int31 - The length of the deque is therefore [end - head]. + let pp fmt x = Format.fprintf fmt "%d" x + end) - *) + module Stack = MakeDeque (struct + type t = int - let head_key = [P.name; "head"] + let name = "stack" - let end_key = [P.name; "end"] + let encoding = Data_encoding.int31 + end) - let get_head = get_value ~default:Z.zero head_key Data_encoding.z + module Code = MakeDeque (struct + type t = instruction - let set_head = set_value head_key Data_encoding.z + let name = "code" - let get_end = get_value ~default:(Z.of_int 0) end_key Data_encoding.z + let encoding = + Data_encoding.( + union + [ + case + ~title:"push" + (Tag 0) + Data_encoding.int31 + (function IPush x -> Some x | _ -> None) + (fun x -> IPush x); + case + ~title:"add" + (Tag 1) + Data_encoding.unit + (function IAdd -> Some () | _ -> None) + (fun () -> IAdd); + case + ~title:"store" + (Tag 2) + Data_encoding.string + (function IStore x -> Some x | _ -> None) + (fun x -> IStore x); + ]) + end) - let set_end = set_value end_key Data_encoding.z + module Boot_sector = MakeVar (struct + type t = string - let idx_key idx = [P.name; Z.to_string idx] + let name = "boot_sector" - let top = - let open Monad.Syntax in - let* head_idx = get_head in - let* end_idx = get_end in - let* v = find_value (idx_key head_idx) P.encoding in - if Z.(leq end_idx head_idx) then return None - else - match v with - | None -> (* By invariants of the Deque. *) assert false - | Some x -> return (Some x) + let initial = "" - let push x = - let open Monad.Syntax in - let* head_idx = get_head in - let head_idx' = Z.pred head_idx in - let* () = set_head head_idx' in - set_value (idx_key head_idx') P.encoding x + let encoding = Data_encoding.string - let pop = - let open Monad.Syntax in - let* head_idx = get_head in - let* end_idx = get_end in - if Z.(leq end_idx head_idx) then return None - else - let* v = find_value (idx_key head_idx) P.encoding in - match v with - | None -> (* By invariants of the Deque. *) assert false - | Some x -> - let* () = remove (idx_key head_idx) in - let head_idx = Z.succ head_idx in - let* () = set_head head_idx in - return (Some x) - - let inject x = - let open Monad.Syntax in - let* end_idx = get_end in - let end_idx' = Z.succ end_idx in - let* () = set_end end_idx' in - set_value (idx_key end_idx) P.encoding x + let pp fmt s = Format.fprintf fmt "%s" s + end) - let to_list = - let open Monad.Syntax in - let* head_idx = get_head in - let* end_idx = get_end in - let rec aux l idx = - if Z.(lt idx head_idx) then return l - else - let* v = find_value (idx_key idx) P.encoding in - match v with - | None -> (* By invariants of deque *) assert false - | Some v -> aux (v :: l) (Z.pred idx) - in - aux [] (Z.pred end_idx) + module Status = MakeVar (struct + type t = status - let clear = remove [P.name] - end + let initial = Halted - module CurrentTick = MakeVar (struct - include Tick + let encoding = + Data_encoding.string_enum + [ + ("Halted", Halted); + ("WaitingForInput", WaitingForInputMessage); + ("Parsing", Parsing); + ("Evaluating", Evaluating); + ] - let name = "tick" - end) + let name = "status" - module Vars = MakeDict (struct - type t = int + let string_of_status = function + | Halted -> "Halted" + | WaitingForInputMessage -> "WaitingForInputMessage" + | Parsing -> "Parsing" + | Evaluating -> "Evaluating" - let name = "vars" + let pp fmt status = Format.fprintf fmt "%s" (string_of_status status) + end) - let encoding = Data_encoding.int31 + module CurrentLevel = MakeVar (struct + type t = Raw_level.t - let pp fmt x = Format.fprintf fmt "%d" x - end) + let initial = Raw_level.root - module Stack = MakeDeque (struct - type t = int + let encoding = Raw_level.encoding - let name = "stack" + let name = "current_level" - let encoding = Data_encoding.int31 - end) + let pp = Raw_level.pp + end) - module Code = MakeDeque (struct - type t = instruction + module MessageCounter = MakeVar (struct + type t = Z.t - let name = "code" + let initial = Z.(pred zero) - let encoding = - Data_encoding.( - union - [ - case - ~title:"push" - (Tag 0) - Data_encoding.int31 - (function IPush x -> Some x | _ -> None) - (fun x -> IPush x); - case - ~title:"add" - (Tag 1) - Data_encoding.unit - (function IAdd -> Some () | _ -> None) - (fun () -> IAdd); - case - ~title:"store" - (Tag 2) - Data_encoding.string - (function IStore x -> Some x | _ -> None) - (fun x -> IStore x); - ]) - end) + let encoding = Data_encoding.n - module Boot_sector = MakeVar (struct - type t = string + let name = "message_counter" - let name = "boot_sector" + let pp = Z.pp_print + end) - let initial = "" + module NextMessage = MakeVar (struct + type t = string option - let encoding = Data_encoding.string + let initial = None - let pp fmt s = Format.fprintf fmt "%s" s - end) + let encoding = Data_encoding.(option string) - module Status = MakeVar (struct - type t = status + let name = "next_message" - let initial = Halted + let pp fmt = function + | None -> Format.fprintf fmt "None" + | Some s -> Format.fprintf fmt "Some %s" s + end) - let encoding = - Data_encoding.string_enum - [ - ("Halted", Halted); - ("WaitingForInput", WaitingForInputMessage); - ("Parsing", Parsing); - ("Evaluating", Evaluating); - ] + type parser_state = ParseInt | ParseVar | SkipLayout - let name = "status" + module LexerState = MakeVar (struct + type t = int * int - let string_of_status = function - | Halted -> "Halted" - | WaitingForInputMessage -> "WaitingForInputMessage" - | Parsing -> "Parsing" - | Evaluating -> "Evaluating" + let name = "lexer_buffer" - let pp fmt status = Format.fprintf fmt "%s" (string_of_status status) - end) + let initial = (-1, -1) - module CurrentLevel = MakeVar (struct - type t = Raw_level.t + let encoding = Data_encoding.(tup2 int31 int31) - let initial = Raw_level.root + let pp fmt (start, len) = + Format.fprintf fmt "lexer.(start = %d, len = %d)" start len + end) - let encoding = Raw_level.encoding + module ParserState = MakeVar (struct + type t = parser_state - let name = "current_level" + let name = "parser_state" - let pp = Raw_level.pp - end) + let initial = SkipLayout - module MessageCounter = MakeVar (struct - type t = Z.t + let encoding = + Data_encoding.string_enum + [ + ("ParseInt", ParseInt); + ("ParseVar", ParseVar); + ("SkipLayout", SkipLayout); + ] - let initial = Z.(pred zero) + let pp fmt = function + | ParseInt -> Format.fprintf fmt "Parsing int" + | ParseVar -> Format.fprintf fmt "Parsing var" + | SkipLayout -> Format.fprintf fmt "Skipping layout" + end) - let encoding = Data_encoding.n + module ParsingResult = MakeVar (struct + type t = bool option - let name = "message_counter" + let name = "parsing_result" - let pp = Z.pp_print - end) + let initial = None - module NextMessage = MakeVar (struct - type t = string option + let encoding = Data_encoding.(option bool) - let initial = None + let pp fmt = function + | None -> Format.fprintf fmt "n/a" + | Some true -> Format.fprintf fmt "parsing succeeds" + | Some false -> Format.fprintf fmt "parsing fails" + end) - let encoding = Data_encoding.(option string) + module EvaluationResult = MakeVar (struct + type t = bool option - let name = "next_message" + let name = "evaluation_result" - let pp fmt = function - | None -> Format.fprintf fmt "None" - | Some s -> Format.fprintf fmt "Some %s" s - end) + let initial = None - type parser_state = ParseInt | ParseVar | SkipLayout + let encoding = Data_encoding.(option bool) - module LexerState = MakeVar (struct - type t = int * int + let pp fmt = function + | None -> Format.fprintf fmt "n/a" + | Some true -> Format.fprintf fmt "evaluation succeeds" + | Some false -> Format.fprintf fmt "evaluation fails" + end) - let name = "lexer_buffer" + let pp = + let open Monad.Syntax in + let* status_pp = Status.pp in + let* message_counter_pp = MessageCounter.pp in + let* next_message_pp = NextMessage.pp in + let* parsing_result_pp = ParsingResult.pp in + let* parser_state_pp = ParserState.pp in + let* lexer_state_pp = LexerState.pp in + let* evaluation_result_pp = EvaluationResult.pp in + let* vars_pp = Vars.pp in + return @@ fun fmt () -> + Format.fprintf + fmt + "@[@;%a@;%a@;%a@;%a@;%a@;%a@;%a@;%a@]" + status_pp + () + message_counter_pp + () + next_message_pp + () + parsing_result_pp + () + parser_state_pp + () + lexer_state_pp + () + evaluation_result_pp + () + vars_pp + () + end - let initial = (-1, -1) + open State - let encoding = Data_encoding.(tup2 int31 int31) + type state = State.state - let pp fmt (start, len) = - Format.fprintf fmt "lexer.(start = %d, len = %d)" start len - end) + let pp state = + let open Lwt_syntax in + let* _, pp = Monad.run pp state in + match pp with + | None -> return @@ fun fmt _ -> Format.fprintf fmt "" + | Some pp -> return pp - module ParserState = MakeVar (struct - type t = parser_state + open Monad - let name = "parser_state" + let initial_state ctxt boot_sector = + let state = Tree.empty ctxt in + let m = + let open Monad.Syntax in + let* () = Boot_sector.set boot_sector in + let* () = Status.set Halted in + return () + in + let open Lwt_syntax in + let* state, _ = run m state in + return state + + let state_hash state = + let m = + let open Monad.Syntax in + let* status = Status.get in + match status with + | Halted -> return State_hash.zero + | _ -> + 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 - let initial = SkipLayout + let boot = + let open Monad.Syntax in + let* () = Status.create in + let* () = NextMessage.create in + let* () = Status.set WaitingForInputMessage in + return () - let encoding = - Data_encoding.string_enum - [ - ("ParseInt", ParseInt); - ("ParseVar", ParseVar); - ("SkipLayout", SkipLayout); - ] + let result_of ~default m state = + let open Lwt_syntax in + let* _, v = run m state in + match v with None -> return default | Some v -> return v - let pp fmt = function - | ParseInt -> Format.fprintf fmt "Parsing int" - | ParseVar -> Format.fprintf fmt "Parsing var" - | SkipLayout -> Format.fprintf fmt "Skipping layout" - end) + let state_of m state = + let open Lwt_syntax in + let* s, _ = run m state in + return s - module ParsingResult = MakeVar (struct - type t = bool option + let get_tick = result_of ~default:Tick.initial CurrentTick.get - let name = "parsing_result" + let is_input_state_monadic = + let open Monad.Syntax in + let* status = Status.get in + match status with + | WaitingForInputMessage -> + let* level = CurrentLevel.get in + let* counter = MessageCounter.get in + return (Some (level, counter)) + | _ -> return None - let initial = None + let is_input_state = result_of ~default:None @@ is_input_state_monadic - let encoding = Data_encoding.(option bool) + let get_status = result_of ~default:WaitingForInputMessage @@ Status.get - let pp fmt = function - | None -> Format.fprintf fmt "n/a" - | Some true -> Format.fprintf fmt "parsing succeeds" - | Some false -> Format.fprintf fmt "parsing fails" - end) + let get_code = result_of ~default:[] @@ Code.to_list - module EvaluationResult = MakeVar (struct - type t = bool option + let get_parsing_result = result_of ~default:None @@ ParsingResult.get - let name = "evaluation_result" + let get_stack = result_of ~default:[] @@ Stack.to_list - let initial = None + let get_var state k = (result_of ~default:None @@ Vars.get k) state - let encoding = Data_encoding.(option bool) + let get_evaluation_result = result_of ~default:None @@ EvaluationResult.get - let pp fmt = function - | None -> Format.fprintf fmt "n/a" - | Some true -> Format.fprintf fmt "evaluation succeeds" - | Some false -> Format.fprintf fmt "evaluation fails" - end) + let get_is_stuck = result_of ~default:None @@ is_stuck - let pp = + let set_input_monadic input = + let open Sc_rollup_PVM_sem in + let {inbox_level; message_counter; payload} = input in let open Monad.Syntax in - let* status_pp = Status.pp in - let* message_counter_pp = MessageCounter.pp in - let* next_message_pp = NextMessage.pp in - let* parsing_result_pp = ParsingResult.pp in - let* parser_state_pp = ParserState.pp in - let* lexer_state_pp = LexerState.pp in - let* evaluation_result_pp = EvaluationResult.pp in - let* vars_pp = Vars.pp in - return @@ fun fmt () -> - Format.fprintf - fmt - "@[@;%a@;%a@;%a@;%a@;%a@;%a@;%a@;%a@]" - status_pp - () - message_counter_pp - () - next_message_pp - () - parsing_result_pp - () - parser_state_pp - () - lexer_state_pp - () - evaluation_result_pp - () - vars_pp - () - end + let* boot_sector = Boot_sector.get in + let msg = boot_sector ^ payload in + let* last_level = CurrentLevel.get in + let* last_counter = MessageCounter.get in + let update = + let* () = CurrentLevel.set inbox_level in + let* () = MessageCounter.set message_counter in + let* () = NextMessage.set (Some msg) in + return () + in + let does_not_follow = + internal_error "The input message does not follow the previous one." + in + if Raw_level.(equal last_level inbox_level) then + if Z.(equal message_counter (succ last_counter)) then update + else does_not_follow + else if Raw_level.(last_level < inbox_level) then + if Z.(equal message_counter Z.zero) then update else does_not_follow + else does_not_follow - open State + let set_input input = state_of @@ set_input_monadic input - type state = State.state + let next_char = + let open Monad.Syntax in + LexerState.( + let* start, len = get in + set (start, len + 1)) - let pp state = - let open Lwt_syntax in - let* _, pp = Monad.run pp state in - match pp with - | None -> return @@ fun fmt _ -> Format.fprintf fmt "" - | Some pp -> return pp + let no_message_to_lex () = + internal_error "lexer: There is no input message to lex" - open Monad + let current_char = + let open Monad.Syntax in + let* start, len = LexerState.get in + let* msg = NextMessage.get in + match msg with + | None -> no_message_to_lex () + | Some s -> + if Compare.Int.(start + len < String.length s) then + return (Some s.[start + len]) + else return None + + let lexeme = + let open Monad.Syntax in + let* start, len = LexerState.get in + let* msg = NextMessage.get in + match msg with + | None -> no_message_to_lex () + | Some s -> + let* () = LexerState.set (start + len, 0) in + return (String.sub s start len) + + let push_int_literal = + let open Monad.Syntax in + let* s = lexeme in + match int_of_string_opt s with + | Some x -> Code.inject (IPush x) + | None -> (* By validity of int parsing. *) assert false - let initial_state ctxt boot_sector = - let state = Tree.empty ctxt in - let m = + let push_var = let open Monad.Syntax in - let* () = Boot_sector.set boot_sector in - let* () = Status.set Halted in - return () - in - let open Lwt_syntax in - let* state, _ = run m state in - return state + let* s = lexeme in + Code.inject (IStore s) - let state_hash state = - let m = + let start_parsing : unit t = let open Monad.Syntax in - let* status = Status.get in - match status with - | Halted -> return State_hash.zero - | _ -> - 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 - - let boot = - let open Monad.Syntax in - let* () = Status.create in - let* () = NextMessage.create in - let* () = Status.set WaitingForInputMessage in - return () - - let result_of ~default m state = - let open Lwt_syntax in - let* _, v = run m state in - match v with None -> return default | Some 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:Tick.initial CurrentTick.get - - let is_input_state_monadic = - let open Monad.Syntax in - let* status = Status.get in - match status with - | WaitingForInputMessage -> - let* level = CurrentLevel.get in - let* counter = MessageCounter.get in - return (Some (level, counter)) - | _ -> return None - - let is_input_state = result_of ~default:None @@ is_input_state_monadic - - let get_status = result_of ~default:WaitingForInputMessage @@ Status.get - - let get_code = result_of ~default:[] @@ Code.to_list - - let get_parsing_result = result_of ~default:None @@ ParsingResult.get - - let get_stack = result_of ~default:[] @@ Stack.to_list - - let get_var state k = (result_of ~default:None @@ Vars.get k) state - - let get_evaluation_result = result_of ~default:None @@ EvaluationResult.get - - let get_is_stuck = result_of ~default:None @@ is_stuck - - let set_input_monadic input = - let open Sc_rollup_PVM_sem 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* last_level = CurrentLevel.get in - let* last_counter = MessageCounter.get in - let update = - let* () = CurrentLevel.set inbox_level in - let* () = MessageCounter.set message_counter in - let* () = NextMessage.set (Some msg) in - return () - in - let does_not_follow = - internal_error "The input message does not follow the previous one." - in - if Raw_level.(equal last_level inbox_level) then - if Z.(equal message_counter (succ last_counter)) then update - else does_not_follow - else if Raw_level.(last_level < inbox_level) then - if Z.(equal message_counter Z.zero) then update else does_not_follow - else does_not_follow - - let set_input input = state_of @@ set_input_monadic input - - let next_char = - let open Monad.Syntax in - LexerState.( - let* start, len = get in - set (start, len + 1)) - - let no_message_to_lex () = - internal_error "lexer: There is no input message to lex" - - let current_char = - let open Monad.Syntax in - let* start, len = LexerState.get in - let* msg = NextMessage.get in - match msg with - | None -> no_message_to_lex () - | Some s -> - if Compare.Int.(start + len < String.length s) then - return (Some s.[start + len]) - else return None - - let lexeme = - let open Monad.Syntax in - let* start, len = LexerState.get in - let* msg = NextMessage.get in - match msg with - | None -> no_message_to_lex () - | Some s -> - let* () = LexerState.set (start + len, 0) in - return (String.sub s start len) - - let push_int_literal = - let open Monad.Syntax in - let* s = lexeme in - match int_of_string_opt s with - | Some x -> Code.inject (IPush x) - | None -> (* By validity of int parsing. *) assert false - - let push_var = - let open Monad.Syntax in - let* s = lexeme in - Code.inject (IStore s) - - let start_parsing : unit t = - let open Monad.Syntax in - let* () = Status.set Parsing in - let* () = ParsingResult.set None in - let* () = ParserState.set SkipLayout in - let* () = LexerState.set (0, 0) in - let* () = Status.set Parsing in - let* () = Code.clear in - return () - - let start_evaluating : unit t = - let open Monad.Syntax in - let* () = EvaluationResult.set None in - let* () = Stack.clear in - let* () = Status.set Evaluating in - return () - - let stop_parsing outcome = - let open Monad.Syntax in - let* () = ParsingResult.set (Some outcome) in - start_evaluating - - let stop_evaluating outcome = - let open Monad.Syntax in - let* () = EvaluationResult.set (Some outcome) in - Status.set WaitingForInputMessage - - let parse : unit t = - let open Monad.Syntax in - let produce_add = - let* _ = lexeme in - let* () = next_char in - let* () = Code.inject IAdd in - return () - in - let produce_int = - let* () = push_int_literal in + let* () = Status.set Parsing in + let* () = ParsingResult.set None in let* () = ParserState.set SkipLayout in + let* () = LexerState.set (0, 0) in + let* () = Status.set Parsing in + let* () = Code.clear in return () - in - let produce_var = - let* () = push_var in - let* () = ParserState.set SkipLayout in + + let start_evaluating : unit t = + let open Monad.Syntax in + let* () = EvaluationResult.set None in + let* () = Stack.clear in + let* () = Status.set Evaluating in return () - in - let is_digit d = Compare.Char.(d >= '0' && d <= '9') in - let is_letter d = Compare.Char.(d >= 'a' && d <= 'z') in - let* parser_state = ParserState.get in - match parser_state with - | ParseInt -> ( - let* char = current_char in - match char with - | Some d when is_digit d -> next_char - | Some '+' -> - let* () = produce_int in - let* () = produce_add in - return () - | Some ' ' -> - let* () = produce_int in - let* () = next_char in - return () - | None -> - let* () = push_int_literal in - stop_parsing true - | _ -> stop_parsing false) - | ParseVar -> ( - let* char = current_char in - match char with - | Some d when is_letter d -> next_char - | Some '+' -> - let* () = produce_var in - let* () = produce_add in - return () - | Some ' ' -> - let* () = produce_var in - let* () = next_char in - return () - | None -> - let* () = push_var in - stop_parsing true - | _ -> stop_parsing false) - | SkipLayout -> ( - let* char = current_char in - match char with - | Some ' ' -> next_char - | Some '+' -> produce_add - | Some d when is_digit d -> - let* _ = lexeme in - let* () = next_char in - let* () = ParserState.set ParseInt in - return () - | Some d when is_letter d -> - let* _ = lexeme in - let* () = next_char in - let* () = ParserState.set ParseVar in - return () - | None -> stop_parsing true - | _ -> stop_parsing false) - - let evaluate = - let open Monad.Syntax in - let* i = Code.pop in - match i with - | None -> stop_evaluating true - | Some (IPush x) -> Stack.push x - | Some (IStore x) -> ( - let* v = Stack.top in - match v with None -> stop_evaluating false | Some v -> Vars.set x v) - | Some IAdd -> ( - let* v = Stack.pop in - match v with - | None -> stop_evaluating false - | Some x -> ( - let* v = Stack.pop in - match v with - | None -> stop_evaluating false - | Some y -> Stack.push (x + y))) - - let reboot = - let open Monad.Syntax in - let* () = Status.set WaitingForInputMessage in - let* () = Stack.clear in - let* () = Code.clear in - return () - - let eval_step = - let open Monad.Syntax in - let* x = is_stuck in - match x with - | Some _ -> reboot - | None -> ( - let* status = Status.get in - match status with - | Halted -> boot - | WaitingForInputMessage -> ( - let* msg = NextMessage.get in - match msg with - | None -> - internal_error - "An input state was not provided an input message." - | Some _ -> start_parsing) - | Parsing -> parse - | Evaluating -> evaluate) - - let ticked m = - let open Monad.Syntax in - let* tick = CurrentTick.get in - let* () = CurrentTick.set (Tick.next tick) in - m - - let eval state = state_of (ticked eval_step) state - - let verify_proof ~input proof = - let open Lwt_syntax in - let transition state = - let* state = - match input with - | None -> eval state - | Some input -> state_of (ticked (set_input_monadic input)) state + + let stop_parsing outcome = + let open Monad.Syntax in + let* () = ParsingResult.set (Some outcome) in + start_evaluating + + let stop_evaluating outcome = + let open Monad.Syntax in + let* () = EvaluationResult.set (Some outcome) in + Status.set WaitingForInputMessage + + let parse : unit t = + let open Monad.Syntax in + let produce_add = + let* _ = lexeme in + let* () = next_char in + let* () = Code.inject IAdd in + return () in - return (state, ()) - in - let* x = Context.verify_proof proof transition in - match x with Ok _ -> return_true | Error _ -> return_false -end + let produce_int = + let* () = push_int_literal in + let* () = ParserState.set SkipLayout in + return () + in + let produce_var = + let* () = push_var in + let* () = ParserState.set SkipLayout in + return () + in + let is_digit d = Compare.Char.(d >= '0' && d <= '9') in + let is_letter d = Compare.Char.(d >= 'a' && d <= 'z') in + let* parser_state = ParserState.get in + match parser_state with + | ParseInt -> ( + let* char = current_char in + match char with + | Some d when is_digit d -> next_char + | Some '+' -> + let* () = produce_int in + let* () = produce_add in + return () + | Some ' ' -> + let* () = produce_int in + let* () = next_char in + return () + | None -> + let* () = push_int_literal in + stop_parsing true + | _ -> stop_parsing false) + | ParseVar -> ( + let* char = current_char in + match char with + | Some d when is_letter d -> next_char + | Some '+' -> + let* () = produce_var in + let* () = produce_add in + return () + | Some ' ' -> + let* () = produce_var in + let* () = next_char in + return () + | None -> + let* () = push_var in + stop_parsing true + | _ -> stop_parsing false) + | SkipLayout -> ( + let* char = current_char in + match char with + | Some ' ' -> next_char + | Some '+' -> produce_add + | Some d when is_digit d -> + let* _ = lexeme in + let* () = next_char in + let* () = ParserState.set ParseInt in + return () + | Some d when is_letter d -> + let* _ = lexeme in + let* () = next_char in + let* () = ParserState.set ParseVar in + return () + | None -> stop_parsing true + | _ -> stop_parsing false) + + let evaluate = + let open Monad.Syntax in + let* i = Code.pop in + match i with + | None -> stop_evaluating true + | Some (IPush x) -> Stack.push x + | Some (IStore x) -> ( + let* v = Stack.top in + match v with None -> stop_evaluating false | Some v -> Vars.set x v) + | Some IAdd -> ( + let* v = Stack.pop in + match v with + | None -> stop_evaluating false + | Some x -> ( + let* v = Stack.pop in + match v with + | None -> stop_evaluating false + | Some y -> Stack.push (x + y))) + + let reboot = + let open Monad.Syntax in + let* () = Status.set WaitingForInputMessage in + let* () = Stack.clear in + let* () = Code.clear in + return () -module ProtocolImplementation = Make (struct - module Tree = struct - include Context.Tree + let eval_step = + let open Monad.Syntax in + let* x = is_stuck in + match x with + | Some _ -> reboot + | None -> ( + let* status = Status.get in + match status with + | Halted -> boot + | WaitingForInputMessage -> ( + let* msg = NextMessage.get in + match msg with + | None -> + internal_error + "An input state was not provided an input message." + | Some _ -> start_parsing) + | Parsing -> parse + | Evaluating -> evaluate) + + let ticked m = + let open Monad.Syntax in + let* tick = CurrentTick.get in + let* () = CurrentTick.set (Tick.next tick) in + m + + let eval state = state_of (ticked eval_step) state + + let verify_proof ~input proof = + let open Lwt_syntax in + let transition state = + let* state = + match input with + | None -> eval state + | Some input -> state_of (ticked (set_input_monadic input)) state + in + return (state, ()) + in + let* x = Context.verify_proof proof transition in + match x with Ok _ -> return_true | Error _ -> return_false + end - type tree = Context.tree + module ProtocolImplementation = Make (struct + module Tree = struct + include Context.Tree - type t = Context.t + type tree = Context.tree - type key = string list + type t = Context.t - type value = bytes - end + type key = string list - type tree = Context.tree + type value = bytes + end - type proof = Context.Proof.tree Context.Proof.t + type tree = Context.tree - let verify_proof = Context.verify_tree_proof + type proof = Context.Proof.tree Context.Proof.t - let kinded_hash_to_state_hash = function - | `Value hash | `Node hash -> - State_hash.hash_bytes [Context_hash.to_bytes hash] + let verify_proof = Context.verify_tree_proof - let proof_start_state proof = - kinded_hash_to_state_hash proof.Context.Proof.before + let kinded_hash_to_state_hash = function + | `Value hash | `Node hash -> + State_hash.hash_bytes [Context_hash.to_bytes hash] - let proof_stop_state proof = - kinded_hash_to_state_hash proof.Context.Proof.after + let proof_start_state proof = + kinded_hash_to_state_hash proof.Context.Proof.before - let proof_encoding = Context.Proof_encoding.V2.Tree32.tree_proof_encoding -end) + let proof_stop_state proof = + kinded_hash_to_state_hash proof.Context.Proof.after + let proof_encoding = Context.Proof_encoding.V2.Tree32.tree_proof_encoding + end) end diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli index b255c5fe3107..99db99a97550 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.mli @@ -24,112 +24,110 @@ (*****************************************************************************) module V2_0_0 : sig - -(** This module providess Proof-Generating Virtual Machine (PVM) running + (** This module providess Proof-Generating Virtual Machine (PVM) running WebAssembly. *) -open Alpha_context - + open Alpha_context -module type S = sig - include Sc_rollup_PVM_sem.S + module type S = sig + include Sc_rollup_PVM_sem.S - (** [name] is "wasm_2_0_0". + (** [name] is "wasm_2_0_0". WebAssembly is an "evergreen" specification. We aim to track the latest major version, 2.0 at the time of writing. We use the minor version number to track changes to our fork. *) - val name : string + val name : string - (** [parse_boot_sector s] builds a boot sector from its human + (** [parse_boot_sector s] builds a boot sector from its human writable description. *) - val parse_boot_sector : string -> string option + val parse_boot_sector : string -> string option - (** [pp_boot_sector fmt s] prints a human readable representation of + (** [pp_boot_sector fmt s] prints a human readable representation of a boot sector. *) - val pp_boot_sector : Format.formatter -> string -> unit + val pp_boot_sector : Format.formatter -> string -> unit - (** [pp state] returns a pretty-printer valid for [state]. *) - val pp : state -> (Format.formatter -> unit -> unit) Lwt.t + (** [pp state] returns a pretty-printer valid for [state]. *) + val pp : state -> (Format.formatter -> unit -> unit) Lwt.t - (** [get_tick state] returns the current tick of [state]. *) - val get_tick : state -> Sc_rollup.Tick.t Lwt.t + (** [get_tick state] returns the current tick of [state]. *) + val get_tick : state -> Sc_rollup.Tick.t Lwt.t - (** The machine has three possible states: *) - type status = Halted | WaitingForInputMessage | Parsing | Evaluating + (** The machine has three possible states: *) + type status = Halted | WaitingForInputMessage | Parsing | Evaluating - (** [get_status state] returns the machine status in [state]. *) - val get_status : state -> status Lwt.t + (** [get_status state] returns the machine status in [state]. *) + val get_status : state -> status Lwt.t - (** The machine has only three instructions. *) - type instruction = - | IPush : int -> instruction - | IAdd : instruction - | IStore : string -> instruction + (** The machine has only three instructions. *) + type instruction = + | IPush : int -> instruction + | IAdd : instruction + | IStore : string -> instruction - (** [equal_instruction i1 i2] is [true] iff [i1] equals [i2]. *) - val equal_instruction : instruction -> instruction -> bool + (** [equal_instruction i1 i2] is [true] iff [i1] equals [i2]. *) + val equal_instruction : instruction -> instruction -> bool - (** [pp_instruction fmt i] shows a human readable representation of [i]. *) - val pp_instruction : Format.formatter -> instruction -> unit + (** [pp_instruction fmt i] shows a human readable representation of [i]. *) + val pp_instruction : Format.formatter -> instruction -> unit - (** [get_parsing_result state] is [Some true] if the current + (** [get_parsing_result state] is [Some true] if the current message is syntactically correct, [Some false] when it contains a syntax error, and [None] when the machine is not in parsing state. *) - val get_parsing_result : state -> bool option Lwt.t + val get_parsing_result : state -> bool option Lwt.t - (** [get_code state] returns the current code obtained by parsing + (** [get_code state] returns the current code obtained by parsing the current input message. *) - val get_code : state -> instruction list Lwt.t + val get_code : state -> instruction list Lwt.t - (** [get_stack state] returns the current stack. *) - val get_stack : state -> int list Lwt.t + (** [get_stack state] returns the current stack. *) + val get_stack : state -> int list Lwt.t - (** [get_var state x] returns the current value of variable [x]. + (** [get_var state x] returns the current value of variable [x]. Returns [None] if [x] does not exist. *) - val get_var : state -> string -> int option Lwt.t + val get_var : state -> string -> int option Lwt.t - (** [get_evaluation_result state] returns [Some true] if the current + (** [get_evaluation_result state] returns [Some true] if the current message evaluation succeeds, [Some false] if it failed, and [None] if the evaluation has not been done yet. *) - val get_evaluation_result : state -> bool option Lwt.t + val get_evaluation_result : state -> bool option Lwt.t - (** [get_is_stuck state] returns [Some err] if some internal error + (** [get_is_stuck state] returns [Some err] if some internal error made the machine fail during the last evaluation step. [None] if no internal error occurred. When a machine is stuck, it reboots, waiting for the next message to process. *) - val get_is_stuck : state -> string option Lwt.t -end + val get_is_stuck : state -> string option Lwt.t + end -module ProtocolImplementation : S with type context = Context.t + module ProtocolImplementation : S with type context = Context.t -module type P = sig - module Tree : Context.TREE with type key = string list and type value = bytes + module type P = sig + module Tree : + Context.TREE with type key = string list and type value = bytes - type tree = Tree.tree + type tree = Tree.tree - type proof + type proof - val proof_encoding : proof Data_encoding.t + val proof_encoding : proof Data_encoding.t - val proof_start_state : proof -> Sc_rollup.State_hash.t + val proof_start_state : proof -> Sc_rollup.State_hash.t - val proof_stop_state : proof -> Sc_rollup.State_hash.t - - val verify_proof : - proof -> - (tree -> (tree * 'a) Lwt.t) -> - ( tree * 'a, - [ `Proof_mismatch of string - | `Stream_too_long of string - | `Stream_too_short of string ] ) - result - Lwt.t -end + val proof_stop_state : proof -> Sc_rollup.State_hash.t -module Make (Context : P) : - S with type context = Context.Tree.t and type state = Context.tree + val verify_proof : + proof -> + (tree -> (tree * 'a) Lwt.t) -> + ( tree * 'a, + [ `Proof_mismatch of string + | `Stream_too_long of string + | `Stream_too_short of string ] ) + result + Lwt.t + end + module Make (Context : P) : + S with type context = Context.Tree.t and type state = Context.tree end diff --git a/src/proto_alpha/lib_protocol/sc_rollups.ml b/src/proto_alpha/lib_protocol/sc_rollups.ml index f8f3cba07e09..f1e4166e4e6f 100644 --- a/src/proto_alpha/lib_protocol/sc_rollups.ml +++ b/src/proto_alpha/lib_protocol/sc_rollups.ml @@ -43,14 +43,19 @@ end let all = [Kind.Example_arith; Kind.Wasm_2_0_0] -let kind_of_string = function "arith" -> Some Kind.Example_arith | "wasm_2_0_0" -> Some Wasm_2_0_0 | _ -> None +let kind_of_string = function + | "arith" -> Some Kind.Example_arith + | "wasm_2_0_0" -> Some Wasm_2_0_0 + | _ -> None let example_arith_pvm = (module Sc_rollup_arith.ProtocolImplementation : PVM.S) -let wasm_2_0_0_pvm = (module Sc_rollup_wasm.V2_0_0.ProtocolImplementation : PVM.S) + +let wasm_2_0_0_pvm = + (module Sc_rollup_wasm.V2_0_0.ProtocolImplementation : PVM.S) let of_kind = function - | Kind.Example_arith -> example_arith_pvm - | Kind.Wasm_2_0_0 -> wasm_2_0_0_pvm + | Kind.Example_arith -> example_arith_pvm + | Kind.Wasm_2_0_0 -> wasm_2_0_0_pvm let kind_of (module M : PVM.S) = match kind_of_string M.name with -- GitLab From fbc125d91c7eba3faa08b64a75987a0f76641bbf Mon Sep 17 00:00:00 2001 From: Hans Hoglund Date: Wed, 25 May 2022 11:52:02 +0000 Subject: [PATCH 5/5] tmp --- src/proto_alpha/lib_protocol/dune | 5 +++++ src/proto_alpha/lib_protocol/sc_rollup_wasm.ml | 1 + 2 files changed, 6 insertions(+) diff --git a/src/proto_alpha/lib_protocol/dune b/src/proto_alpha/lib_protocol/dune index 77b107fe2f60..4c80a128bf62 100644 --- a/src/proto_alpha/lib_protocol/dune +++ b/src/proto_alpha/lib_protocol/dune @@ -210,6 +210,7 @@ Sc_rollup_operations Sc_rollup_PVM_sem Sc_rollup_arith + Sc_rollup_wasm Sc_rollups Baking Amendment @@ -423,6 +424,7 @@ sc_rollup_operations.ml sc_rollup_operations.mli sc_rollup_PVM_sem.ml sc_rollup_arith.ml sc_rollup_arith.mli + sc_rollup_wasm.ml sc_rollup_wasm.mli sc_rollups.ml sc_rollups.mli baking.ml baking.mli amendment.ml amendment.mli @@ -622,6 +624,7 @@ sc_rollup_operations.ml sc_rollup_operations.mli sc_rollup_PVM_sem.ml sc_rollup_arith.ml sc_rollup_arith.mli + sc_rollup_wasm.ml sc_rollup_wasm.mli sc_rollups.ml sc_rollups.mli baking.ml baking.mli amendment.ml amendment.mli @@ -842,6 +845,7 @@ sc_rollup_operations.ml sc_rollup_operations.mli sc_rollup_PVM_sem.ml sc_rollup_arith.ml sc_rollup_arith.mli + sc_rollup_wasm.ml sc_rollup_wasm.mli sc_rollups.ml sc_rollups.mli baking.ml baking.mli amendment.ml amendment.mli @@ -1057,6 +1061,7 @@ sc_rollup_operations.ml sc_rollup_operations.mli sc_rollup_PVM_sem.ml sc_rollup_arith.ml sc_rollup_arith.mli + sc_rollup_wasm.ml sc_rollup_wasm.mli sc_rollups.ml sc_rollups.mli baking.ml baking.mli amendment.ml amendment.mli diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml index 5f44c9c4b09d..c001895aa53f 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml @@ -983,6 +983,7 @@ module V2_0_0 = struct type tree = Context.tree + (* TODO Tree32 or Tree2 *) type proof = Context.Proof.tree Context.Proof.t let verify_proof = Context.verify_tree_proof -- GitLab