diff --git a/src/proto_alpha/lib_client/client_proto_context.mli b/src/proto_alpha/lib_client/client_proto_context.mli index fa2ca612847d6399e0a3c92442d886f73f5a715a..effd467ea0bfbeef886718c49fff9c108ac1b57f 100644 --- a/src/proto_alpha/lib_client/client_proto_context.mli +++ b/src/proto_alpha/lib_client/client_proto_context.mli @@ -589,7 +589,7 @@ val sc_rollup_originate : ?counter:counter -> source:public_key_hash -> kind:Sc_rollup.Kind.t -> - boot_sector:Sc_rollup.PVM.boot_sector -> + boot_sector:string -> src_pk:public_key -> src_sk:Client_keys.sk_uri -> fee_parameter:Injection.fee_parameter -> diff --git a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL index aa3b2d503b5677322ee0e476089a96b11bc5eead..f247802069871ff71facf89e0d91e3d52f578f36 100644 --- a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL +++ b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL @@ -70,6 +70,7 @@ "Lazy_storage_kind", "Receipt_repr", "Migration_repr", + "Sc_rollup_tick_repr", "Raw_context_intf", "Raw_context", @@ -165,6 +166,7 @@ "Script_interpreter_defs", "Script_interpreter", "Sc_rollup_operations", + "Sc_rollup_PVM_sem", "Sc_rollup_arith", "Sc_rollups", diff --git a/src/proto_alpha/lib_protocol/alpha_context.ml b/src/proto_alpha/lib_protocol/alpha_context.ml index 6647d91934b13fbcd5fa781be53aa92000c80db6..585aea7b0dfac4c6f49dbc5ae2254acf56bf8206 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.ml +++ b/src/proto_alpha/lib_protocol/alpha_context.ml @@ -53,6 +53,7 @@ end module Slot = Slot_repr module Sc_rollup = struct + module Tick = Sc_rollup_tick_repr include Sc_rollup_repr include Sc_rollup_storage module Inbox = Sc_rollup_inbox diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index 72dd3d8e63cabc6273ea9f61a5baa5fa09bd2dab..0b48f657638da683454b71936a632b7b3db2a16f 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -2396,10 +2396,27 @@ end (** See {!Sc_rollup_storage} and {!Sc_rollup_repr}. *) module Sc_rollup : sig - module PVM : sig - type boot_sector + (** See {!Sc_rollup_tick_repr}. *) + module Tick : sig + type t + + val initial : t + + val next : t -> t + + val distance : t -> t -> Z.t + + val of_int : int -> t option + + val to_int : t -> int option + + val encoding : t Data_encoding.t + + val pp : Format.formatter -> t -> unit + + include Compare.S with type t := t - val boot_sector_of_string : string -> boot_sector + module Map : Map.S with type key = t end module Address : S.HASH @@ -2440,7 +2457,7 @@ module Sc_rollup : sig val originate : context -> kind:Kind.t -> - boot_sector:PVM.boot_sector -> + boot_sector:string -> (t * Z.t * context) tzresult Lwt.t val kind : context -> t -> Kind.t option tzresult Lwt.t @@ -2857,7 +2874,7 @@ and _ manager_operation = -> Kind.tx_rollup_withdraw manager_operation | Sc_rollup_originate : { kind : Sc_rollup.Kind.t; - boot_sector : Sc_rollup.PVM.boot_sector; + boot_sector : string; } -> Kind.sc_rollup_originate manager_operation | Sc_rollup_add_messages : { diff --git a/src/proto_alpha/lib_protocol/dune.inc b/src/proto_alpha/lib_protocol/dune.inc index 13b8a2b90b0fe1cafb00db1dfd981f7c1b4de3ad..52d534e0233fad8c58cc59a04d7930c6f9197728 100644 --- a/src/proto_alpha/lib_protocol/dune.inc +++ b/src/proto_alpha/lib_protocol/dune.inc @@ -95,6 +95,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end lazy_storage_kind.mli lazy_storage_kind.ml receipt_repr.mli receipt_repr.ml migration_repr.mli migration_repr.ml + sc_rollup_tick_repr.mli sc_rollup_tick_repr.ml raw_context_intf.ml raw_context.mli raw_context.ml storage_costs.mli storage_costs.ml @@ -179,6 +180,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end script_interpreter_defs.ml script_interpreter.mli script_interpreter.ml sc_rollup_operations.mli sc_rollup_operations.ml + sc_rollup_PVM_sem.ml sc_rollup_arith.mli sc_rollup_arith.ml sc_rollups.mli sc_rollups.ml baking.mli baking.ml @@ -268,6 +270,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end lazy_storage_kind.mli lazy_storage_kind.ml receipt_repr.mli receipt_repr.ml migration_repr.mli migration_repr.ml + sc_rollup_tick_repr.mli sc_rollup_tick_repr.ml raw_context_intf.ml raw_context.mli raw_context.ml storage_costs.mli storage_costs.ml @@ -352,6 +355,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end script_interpreter_defs.ml script_interpreter.mli script_interpreter.ml sc_rollup_operations.mli sc_rollup_operations.ml + sc_rollup_PVM_sem.ml sc_rollup_arith.mli sc_rollup_arith.ml sc_rollups.mli sc_rollups.ml baking.mli baking.ml @@ -441,6 +445,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end lazy_storage_kind.mli lazy_storage_kind.ml receipt_repr.mli receipt_repr.ml migration_repr.mli migration_repr.ml + sc_rollup_tick_repr.mli sc_rollup_tick_repr.ml raw_context_intf.ml raw_context.mli raw_context.ml storage_costs.mli storage_costs.ml @@ -525,6 +530,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end script_interpreter_defs.ml script_interpreter.mli script_interpreter.ml sc_rollup_operations.mli sc_rollup_operations.ml + sc_rollup_PVM_sem.ml sc_rollup_arith.mli sc_rollup_arith.ml sc_rollups.mli sc_rollups.ml baking.mli baking.ml @@ -636,6 +642,7 @@ include Tezos_raw_protocol_alpha.Main Lazy_storage_kind Receipt_repr Migration_repr + Sc_rollup_tick_repr Raw_context_intf Raw_context Storage_costs @@ -720,6 +727,7 @@ include Tezos_raw_protocol_alpha.Main Script_interpreter_defs Script_interpreter Sc_rollup_operations + Sc_rollup_PVM_sem Sc_rollup_arith Sc_rollups Baking @@ -850,6 +858,7 @@ include Tezos_raw_protocol_alpha.Main lazy_storage_kind.mli lazy_storage_kind.ml receipt_repr.mli receipt_repr.ml migration_repr.mli migration_repr.ml + sc_rollup_tick_repr.mli sc_rollup_tick_repr.ml raw_context_intf.ml raw_context.mli raw_context.ml storage_costs.mli storage_costs.ml @@ -934,6 +943,7 @@ include Tezos_raw_protocol_alpha.Main script_interpreter_defs.ml script_interpreter.mli script_interpreter.ml sc_rollup_operations.mli sc_rollup_operations.ml + sc_rollup_PVM_sem.ml sc_rollup_arith.mli sc_rollup_arith.ml sc_rollups.mli sc_rollups.ml baking.mli baking.ml diff --git a/src/proto_alpha/lib_protocol/operation_repr.ml b/src/proto_alpha/lib_protocol/operation_repr.ml index 8d7642089c58a6954b9af0fc3eb366a344a95d8f..468e530e9277c8f7fcd152eb584f299a86b149ab 100644 --- a/src/proto_alpha/lib_protocol/operation_repr.ml +++ b/src/proto_alpha/lib_protocol/operation_repr.ml @@ -341,7 +341,7 @@ and _ manager_operation = -> Kind.tx_rollup_withdraw manager_operation | Sc_rollup_originate : { kind : Sc_rollup_repr.Kind.t; - boot_sector : Sc_rollup_repr.PVM.boot_sector; + boot_sector : string; } -> Kind.sc_rollup_originate manager_operation | Sc_rollup_add_messages : { @@ -847,7 +847,7 @@ module Encoding = struct encoding = obj2 (req "kind" Sc_rollup_repr.Kind.encoding) - (req "boot_sector" Sc_rollup_repr.PVM.boot_sector_encoding); + (req "boot_sector" Data_encoding.string); select = (function | Manager (Sc_rollup_originate _ as op) -> Some op | _ -> None); diff --git a/src/proto_alpha/lib_protocol/operation_repr.mli b/src/proto_alpha/lib_protocol/operation_repr.mli index f9a994e90e1e2db48400273f52458747d9ace62e..e86162b7897980095c60531cb8cdc3f753043a26 100644 --- a/src/proto_alpha/lib_protocol/operation_repr.mli +++ b/src/proto_alpha/lib_protocol/operation_repr.mli @@ -409,7 +409,7 @@ and _ manager_operation = sector). *) | Sc_rollup_originate : { kind : Sc_rollup_repr.Kind.t; - boot_sector : Sc_rollup_repr.PVM.boot_sector; + boot_sector : string; } -> Kind.sc_rollup_originate manager_operation (* [Sc_rollup_add_messages] adds messages to a given rollup's diff --git a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml new file mode 100644 index 0000000000000000000000000000000000000000..067250b4ead5f9583260bbca3ee86bfde14e99bc --- /dev/null +++ b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml @@ -0,0 +1,115 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2021 Nomadic Labs *) +(* Copyright (c) 2022 Trili Tech, *) +(* *) +(* 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 introduces the semantics of Proof-generating Virtual Machines. + + A PVM defines an operational semantics for some computational + model. The specificity of PVMs, in comparison with standard virtual + machines, is their ability to generate and to validate a *compact* + proof that a given atomic execution step turned a given state into + another one. + + In the smart-contract rollups, PVMs are used for two purposes: + + - They allow for the externalization of rollup execution by + completely specifying the operational semantics of a given + rollup. This standardization of the semantics gives a unique and + executable source of truth about the interpretation of + smart-contract rollup inboxes, seen as a transformation of a rollup + state. + + - They allow for the validation or refutation of a claim that the + processing of some messages led to a given new rollup state (given + an actual source of truth about the nature of these messages). + +*) +open Alpha_context + +open Sc_rollup + +module type S = sig + (** + + The state of the PVM denotes a state of the rollup. + + *) + type state + + (** During interactive rejection games, a player may need to + provide a proof that a given execution step is valid. *) + type proof + + val proof_encoding : proof Data_encoding.t + + (** A state is initialized in a given context. *) + type context + + (** A commitment hash characterized the contents of the state. *) + type hash = State_hash.t + + (** [proof_start_state proof] returns the initial state hash of the + [proof] execution step. *) + val proof_start_state : proof -> hash + + (** [proof_stop_state proof] returns the final state hash of the + [proof] execution step. *) + val proof_stop_state : proof -> hash + + (** [state_hash state] returns a compressed representation of [state]. *) + val state_hash : state -> hash Lwt.t + + (** [initial_state context] is the state of the PVM before booting. It must + be such that [state_hash state = Commitment_hash.zero]. Any [context] + should be enough to create an initial state. *) + val initial_state : context -> string -> state Lwt.t + + (** [is_input_state state] returns [Some (level, counter)] if [state] is + waiting for the input message that comes next to the message numbered + [counter] in the inbox of a given [level]. *) + val is_input_state : state -> (Raw_level.t * Z.t) option Lwt.t + + type input = { + inbox_level : Raw_level.t; + message_counter : Z.t; + payload : string; + } + + (** [set_input level n msg state] sets [msg] in [state] as + the next message to be processed. This input message is assumed + to be the number [n] in the inbox messages at the given + [level]. The input message must be the message next to the + previous message processed by the rollup. *) + val set_input : input -> state -> state Lwt.t + + (** [eval s0] returns a state [s1] resulting from the + execution of an atomic step of the rollup at state [s0]. *) + val eval : state -> state Lwt.t + + (** [verify_proof input proof] returns [true] iff the [proof] is valid. + If the state is an input state, [input] is the hash of the input + message externally provided to the evaluation function. *) + val verify_proof : input:input option -> proof -> bool Lwt.t +end diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml index c6b131c0b0976168096181cf1c135203c645879e..299f364362030f83ae59872132fe286e54b1b4e0 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml @@ -23,9 +23,843 @@ (* *) (*****************************************************************************) -let name = "arith" +open Alpha_context +open Sc_rollup -let parse_boot_sector _ = - Some (Alpha_context.Sc_rollup.PVM.boot_sector_of_string "") +module type P = sig + module Tree : Context.TREE with type key = string list and type value = bytes -let pp_boot_sector _fmt _ = () + 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 + + 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_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 = 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 + + let equal_instruction i1 i2 = + match (i1, i2) with + | (IPush x, IPush y) -> Compare.Int.(x = y) + | (IAdd, IAdd) -> true + | (_, _) -> false + + let pp_instruction fmt = function + | IPush x -> Format.fprintf fmt "push(%d)" x + | IAdd -> Format.fprintf fmt "add" + + (* + + 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 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 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 -> ( + match Data_encoding.Binary.of_bytes_opt encoding bytes with + | None -> internal_error "Internal_Error during decoding" state + | Some v -> return (state, Some (Some v))) + + 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 + open Monad.Syntax + + 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* 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 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 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 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); + ]) + 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 | 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); ("SkipLayout", SkipLayout)] + + let pp fmt = function + | ParseInt -> Format.fprintf fmt "Parsing int" + | 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 + return @@ fun fmt () -> + Format.fprintf + fmt + "@[@;%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 + () + 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_evaluation_result = result_of ~default:None @@ EvaluationResult.get + + let get_is_stuck = result_of ~default:None @@ is_stuck + + type input = { + inbox_level : Raw_level.t; + message_counter : Z.t; + payload : string; + } + + let set_input_monadic {inbox_level; message_counter; payload} = + 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 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 is_digit d = Compare.Char.(d >= '0' && d <= '9') 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) + | 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 () + | 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 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_arith.mli b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli index 4162b3598cf86414cd307d49627bfbe4d916bf1f..cb3fc4bfbdea6dd06222639487f0caa14fb6caa3 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli @@ -23,12 +23,119 @@ (* *) (*****************************************************************************) -(** This module provides a temporary toy rollup. *) +(** This module provides a temporary toy rollup to be used as a demo. *) -open Alpha_context.Sc_rollup +(** -val name : string + This rollup is a stack machine equipped with addition. -val parse_boot_sector : string -> PVM.boot_sector option + It processed postfix arithmetic expressions written as sequence of + (space separated) [int] and [+] using the following rules: -val pp_boot_sector : Format.formatter -> PVM.boot_sector -> unit + - a number [x] is interpreted as pushing [x] on the stack ; + + - a symbol [+] pops two integers [x] and [y] and pushes [x + y] on + the stack. + + If a message is not syntactically correct or does not evaluate + correctly, the machine stops its evaluation and waits for the next + message. + + The machine has a boot sector which is a mere string used a prefix + for each message. + + The module implements the {!Sc_rollup_PVM_sem.S} interface to be + used in the smart contract rollup infrastructure. + + The machine exposes extra operations to be used in the rollup node. + +*) +open Alpha_context + +module type S = sig + include Sc_rollup_PVM_sem.S + + (** [name] is "arith". *) + 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 two instructions. *) + type instruction = IPush : int -> instruction | IAdd : 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_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 diff --git a/src/proto_alpha/lib_protocol/sc_rollup_operations.mli b/src/proto_alpha/lib_protocol/sc_rollup_operations.mli index d5c5b2fcfdc099d829667599c172d6516694051e..c050eb81ae61c97f9becc966e9a50ed097ca53c0 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_operations.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_operations.mli @@ -33,5 +33,5 @@ type origination_result = {address : Sc_rollup.Address.t; size : Z.t} val originate : context -> kind:Sc_rollup.Kind.t -> - boot_sector:Sc_rollup.PVM.boot_sector -> + boot_sector:string -> (origination_result * context) tzresult Lwt.t diff --git a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml index ec60c206b4769df5a271e66fa581918865f8dd83..ebebb4eae471aa9b7a5f56f82c8cfde4e772a31d 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml @@ -24,14 +24,6 @@ (* *) (*****************************************************************************) -module PVM = struct - type boot_sector = string - - let boot_sector_encoding = Data_encoding.string - - let boot_sector_of_string s = s -end - module Address = struct let prefix = "scr1" diff --git a/src/proto_alpha/lib_protocol/sc_rollup_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_repr.mli index da1b4c41a589475ea65a0fa692b1094eb8d3e840..f9c49c2b016b98470f74d5f3fed767dab21e8cb4 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.mli @@ -39,14 +39,6 @@ as well as the potentially-disputed operations. *) -module PVM : sig - (** A PVM instance can be initialized by setting a boot sector. *) - type boot_sector - - val boot_sector_encoding : boot_sector Data_encoding.t - - val boot_sector_of_string : string -> boot_sector -end (** A smart-contract rollup has an address starting with "scr1". *) module Address : sig diff --git a/src/proto_alpha/lib_protocol/sc_rollup_storage.ml b/src/proto_alpha/lib_protocol/sc_rollup_storage.ml index 5fe839433a5512a6491048d06e953500b900a7c8..98eb0fb8a2eed0253cda0dacf1abccf0ecb5cf64 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_storage.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_storage.ml @@ -227,9 +227,7 @@ let originate ctxt ~kind ~boot_sector = let addresses_size = 2 * Sc_rollup_repr.Address.size in let stored_kind_size = 2 (* because tag_size of kind encoding is 16bits. *) in let boot_sector_size = - Data_encoding.Binary.length - Sc_rollup_repr.PVM.boot_sector_encoding - boot_sector + Data_encoding.Binary.length Data_encoding.string boot_sector in let origination_size = Constants_storage.sc_rollup_origination_size ctxt in let size = diff --git a/src/proto_alpha/lib_protocol/sc_rollup_storage.mli b/src/proto_alpha/lib_protocol/sc_rollup_storage.mli index 5a04b76350bf96cd4dceadf8a7c5d1d74f4a9dcc..efaab6709ce275f8f8a303667bb2859c098960fe 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_storage.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_storage.mli @@ -151,7 +151,7 @@ type error += val originate : Raw_context.t -> kind:Sc_rollup_repr.Kind.t -> - boot_sector:Sc_rollup_repr.PVM.boot_sector -> + boot_sector:string -> (Sc_rollup_repr.Address.t * Z.t * Raw_context.t) tzresult Lwt.t (** [kind context address] returns [Some kind] iff [address] is an @@ -228,7 +228,7 @@ val withdraw_stake : commitments and {i staking on existing commitments}. The storage of commitments is content-addressable to minimize storage duplication. - Subsequent calls to [refine_stake] and [cement_commitment] must use + Subsequent calls to [refine_stake] and [cement_commitment] must use a [context] with greater level, or behavior is undefined. The first time a commitment hash is staked on, it is assigned a deadline, @@ -277,7 +277,7 @@ val last_cemented_commitment : (** [cement_commitment context rollup commitment] cements the given commitment. - Subsequent calls to [refine_stake] and [cement_commitment] must use + Subsequent calls to [refine_stake] and [cement_commitment] must use a [context] with greater level, or behavior is undefined. For cementing to succeed, the following must hold: diff --git a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml new file mode 100644 index 0000000000000000000000000000000000000000..e16ac07c91347a6f804bf9dcde98a1e07b935bdd --- /dev/null +++ b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml @@ -0,0 +1,55 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 Nomadic Labs *) +(* Copyright (c) 2022 Trili Tech, *) +(* *) +(* 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. *) +(* *) +(*****************************************************************************) + +include Z + +let initial = zero + +let next = succ + +let pp = pp_print + +let encoding = Data_encoding.n + +let distance tick1 tick2 = Z.abs (Z.sub tick1 tick2) + +let of_int x = if Compare.Int.(x < 0) then None else Some (Z.of_int x) + +let to_int x = if Z.fits_int x then Some (Z.to_int x) else None + +let ( <= ) = leq + +let ( < ) = lt + +let ( >= ) = geq + +let ( > ) = gt + +let ( = ) = equal + +let ( <> ) x y = not (x = y) + +module Map = Map.Make (Z) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli new file mode 100644 index 0000000000000000000000000000000000000000..9a91554a65f6dc76aed0a135f490818150674d89 --- /dev/null +++ b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli @@ -0,0 +1,55 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 Nomadic Labs *) +(* Copyright (c) 2022 Trili Tech, *) +(* *) +(* 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 defines [Tick.t], an execution step counter for + smart-contract rollups. *) + +(** A tick is a counter for the execution step of a smart-contract rollup. *) +type t + +(** The initial tick. *) +val initial : t + +(** [next tick] returns the counter successor of [tick]. No overflow can happen. *) +val next : t -> t + +(** [distance t1 t2] is the absolute value of the difference between [t1] and [t2]. *) +val distance : t -> t -> Z.t + +(** [of_int x] returns [Some tick] for the rollup [x]-th execution + step if [x] is non-negative. Returns [None] otherwise. *) +val of_int : int -> t option + +(** [to_int tick] converts the [tick] into an integer. *) +val to_int : t -> int option + +val encoding : t Data_encoding.t + +val pp : Format.formatter -> t -> unit + +include Compare.S with type t := t + +module Map : Map.S with type key = t diff --git a/src/proto_alpha/lib_protocol/sc_rollups.ml b/src/proto_alpha/lib_protocol/sc_rollups.ml index ef115a9b95fd271fbde94cca81939d34ceb70f4d..6383f16562ff895d8da4f1b288f0465c9c94c97b 100644 --- a/src/proto_alpha/lib_protocol/sc_rollups.ml +++ b/src/proto_alpha/lib_protocol/sc_rollups.ml @@ -26,7 +26,7 @@ open Alpha_context.Sc_rollup module PVM = struct - type boot_sector = Alpha_context.Sc_rollup.PVM.boot_sector + type boot_sector = string module type S = sig val name : string @@ -34,6 +34,8 @@ module PVM = struct val parse_boot_sector : string -> boot_sector option val pp_boot_sector : Format.formatter -> boot_sector -> unit + + include Sc_rollup_PVM_sem.S end type t = (module S) @@ -43,7 +45,7 @@ let all = [Kind.Example_arith] let kind_of_string = function "arith" -> Some Kind.Example_arith | _ -> None -let example_arith_pvm = (module Sc_rollup_arith : PVM.S) +let example_arith_pvm = (module Sc_rollup_arith.ProtocolImplementation : PVM.S) let of_kind = function Kind.Example_arith -> example_arith_pvm diff --git a/src/proto_alpha/lib_protocol/sc_rollups.mli b/src/proto_alpha/lib_protocol/sc_rollups.mli index 0c530f15e2519ac68a73d01d4bf84ab927db3ac1..dc74b289ea0183ef6c337bdf778db4c1ac6d0d34 100644 --- a/src/proto_alpha/lib_protocol/sc_rollups.mli +++ b/src/proto_alpha/lib_protocol/sc_rollups.mli @@ -27,7 +27,7 @@ open Alpha_context.Sc_rollup module PVM : sig - type boot_sector = Alpha_context.Sc_rollup.PVM.boot_sector + type boot_sector = string module type S = sig val name : string @@ -35,6 +35,8 @@ module PVM : sig val parse_boot_sector : string -> boot_sector option val pp_boot_sector : Format.formatter -> boot_sector -> unit + + include Sc_rollup_PVM_sem.S end type t = (module S) diff --git a/src/proto_alpha/lib_protocol/storage.ml b/src/proto_alpha/lib_protocol/storage.ml index 4d52e2e945c10edbd637b346a19370bd27dd2c49..d9b03f7b74bd9db038c1b00725432c258ed1dc1c 100644 --- a/src/proto_alpha/lib_protocol/storage.ml +++ b/src/proto_alpha/lib_protocol/storage.ml @@ -1549,9 +1549,9 @@ module Sc_rollup = struct let name = ["boot_sector"] end) (struct - type t = Sc_rollup_repr.PVM.boot_sector + type t = string - let encoding = Sc_rollup_repr.PVM.boot_sector_encoding + let encoding = Data_encoding.string end) module Initial_level = diff --git a/src/proto_alpha/lib_protocol/storage.mli b/src/proto_alpha/lib_protocol/storage.mli index e4829e067aca9c10f18f6f9d7a6a000e354eed85..85cbaa74bf7927702e302c5e956b13f586252371 100644 --- a/src/proto_alpha/lib_protocol/storage.mli +++ b/src/proto_alpha/lib_protocol/storage.mli @@ -720,7 +720,7 @@ module Sc_rollup : sig module Boot_sector : Indexed_data_storage with type key = Sc_rollup_repr.t - and type value = Sc_rollup_repr.PVM.boot_sector + and type value = string and type t := Raw_context.t module Initial_level : diff --git a/src/proto_alpha/lib_protocol/test/helpers/op.mli b/src/proto_alpha/lib_protocol/test/helpers/op.mli index 7b7e3cbb78af17ea3d903bb6464f85bb0fcb637b..b4aa981b5e57df610e72acd4003c533018c334bf 100644 --- a/src/proto_alpha/lib_protocol/test/helpers/op.mli +++ b/src/proto_alpha/lib_protocol/test/helpers/op.mli @@ -249,7 +249,7 @@ val sc_rollup_origination : Context.t -> Contract.t -> Sc_rollup.Kind.t -> - Sc_rollup.PVM.boot_sector -> + string -> packed_operation tzresult Lwt.t (** [tx_rollup_commit ctxt source tx_rollup commitment] Commits to a tx diff --git a/src/proto_alpha/lib_protocol/test/integration/operations/test_sc_rollup.ml b/src/proto_alpha/lib_protocol/test/integration/operations/test_sc_rollup.ml index 9183c97091241aa38f3c5b511a4f62da46af762b..1e25f86abfd6a52215fc2f25e62a5b9abc0320bb 100644 --- a/src/proto_alpha/lib_protocol/test/integration/operations/test_sc_rollup.ml +++ b/src/proto_alpha/lib_protocol/test/integration/operations/test_sc_rollup.ml @@ -49,7 +49,7 @@ let test_disable_feature_flag () = in Incremental.begin_construction b >>=? fun i -> let kind = Sc_rollup.Kind.Example_arith in - let boot_sector = Sc_rollup.PVM.boot_sector_of_string "" in + let boot_sector = "" in Op.sc_rollup_origination (I i) contract kind boot_sector >>=? fun op -> let expect_failure = function | Environment.Ecoproto_error (Apply.Sc_rollup_feature_disabled as e) :: _ -> diff --git a/src/proto_alpha/lib_protocol/test/pbt/dune b/src/proto_alpha/lib_protocol/test/pbt/dune index 908952ffecbc21c566741eb01339f9ac8de4c90a..dcdd85f2d2060ae5b7a36b20106a02a9c7685873 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/dune +++ b/src/proto_alpha/lib_protocol/test/pbt/dune @@ -8,6 +8,7 @@ test_tez_repr test_tx_rollup_l2_encoding test_tx_rollup_l2_withdraw_storage + test_sc_rollup_tick_repr test_carbonated_map) (libraries tezos-base tezos-micheline diff --git a/src/proto_alpha/lib_protocol/test/pbt/test_sc_rollup_tick_repr.ml b/src/proto_alpha/lib_protocol/test/pbt/test_sc_rollup_tick_repr.ml new file mode 100644 index 0000000000000000000000000000000000000000..b8a2c84b358cc0c6677d8b4c7a8da17bd695fe15 --- /dev/null +++ b/src/proto_alpha/lib_protocol/test/pbt/test_sc_rollup_tick_repr.ml @@ -0,0 +1,96 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 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. *) +(* *) +(*****************************************************************************) + +(** Testing + ------- + Component: Protocol Library + Invocation: dune exec \ + src/proto_alpha/lib_protocol/test/pbt/test_sc_rollup_tick_repr.exe + Subject: Operations in Tick_repr +*) + +open Protocol.Alpha_context.Sc_rollup +open QCheck + +(** A generator for ticks *) +let tick : Tick.t QCheck.arbitrary = + QCheck.( + Gen.(make (Option.value ~default:Tick.initial <$> map Tick.of_int nat))) + +(** For all x, x = initial \/ x > initial. *) +let test_initial_is_bottom = + QCheck.Test.make ~name:"x = initial \\/ x > initial" tick @@ fun x -> + Tick.(x = initial || x > initial) + +(** For all x, next x > x. *) +let test_next_is_monotonic = + QCheck.Test.make ~name:"next x > x" tick @@ fun x -> Tick.(next x > x) + +(** distance is indeed a distance. *) +let test_distance_identity_of_indiscernibles = + QCheck.Test.make ~name:"distance is a distance (identity)" (pair tick tick) + @@ fun (x, y) -> + (Z.(equal (Tick.distance x y) zero) && Tick.(x = y)) + || Z.(not (equal (Tick.distance x y) zero)) + +let test_distance_symmetry = + QCheck.Test.make ~name:"distance is a distance (symmetry)" (pair tick tick) + @@ fun (x, y) -> Z.(equal (Tick.distance x y) (Tick.distance y x)) + +let test_distance_triangle_inequality = + QCheck.Test.make + ~name:"distance is a distance (triangle inequality)" + (triple tick tick tick) + @@ fun (x, y, z) -> + Tick.(Z.(geq (distance x y + distance y z) (distance x z))) + +(** [of_int x = Some t] iff [x >= 0] *) +let test_of_int = + QCheck.Test.make ~name:"of_int only accepts natural numbers" int @@ fun x -> + match Tick.of_int x with None -> x < 0 | Some _ -> x >= 0 + +(** [of_int (to_int x) = Some x]. *) +let test_of_int_to_int = + QCheck.Test.make ~name:"to_int o of_int = identity" tick @@ fun x -> + Tick.( + match to_int x with + | None -> (* by the tick generator definition. *) assert false + | Some i -> ( match of_int i with Some y -> y = x | None -> false)) + +let tests = + [ + test_next_is_monotonic; + test_initial_is_bottom; + test_distance_identity_of_indiscernibles; + test_distance_symmetry; + test_distance_triangle_inequality; + test_of_int; + test_of_int_to_int; + ] + +let () = + Alcotest.run + "Tick_repr" + [("Tick_repr", Lib_test.Qcheck_helpers.qcheck_wrap tests)] diff --git a/src/proto_alpha/lib_protocol/test/unit/main.ml b/src/proto_alpha/lib_protocol/test/unit/main.ml index 2e82aca0a7d103f4d934baa45e6845cd00189e9d..fc85a60e2c0d85ea961e8398e5a4012f36f4d195 100644 --- a/src/proto_alpha/lib_protocol/test/unit/main.ml +++ b/src/proto_alpha/lib_protocol/test/unit/main.ml @@ -72,5 +72,6 @@ let () = Unit_test.spec "tx rollup l2" Test_tx_rollup_l2.tests; Unit_test.spec "tx rollup l2 apply" Test_tx_rollup_l2_apply.tests; Unit_test.spec "liquidity baking" Test_liquidity_baking_repr.tests; + Unit_test.spec "sc rollup arith" Test_sc_rollup_arith.tests; ] |> Lwt_main.run diff --git a/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_arith.ml new file mode 100644 index 0000000000000000000000000000000000000000..2cec6ec1aca998de9d3399979d97bcc46c56a774 --- /dev/null +++ b/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_arith.ml @@ -0,0 +1,204 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 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. *) +(* *) +(*****************************************************************************) + +(** Testing + ------- + Component: Protocol (saturated arithmetic) + Invocation: dune exec src/proto_alpha/lib_protocol/test/unit/main.exe \ + -- test "^\[Unit\] sc rollup arith$" + Subject: Basic testing of the arithmetic rollup example +*) + +open Protocol +open Sc_rollup_arith.ProtocolImplementation +open Alpha_context + +let create_context () = + Context.init 1 >>=? fun (block, _) -> return block.context + +let setup boot_sector f = + create_context () >>=? fun ctxt -> + initial_state ctxt boot_sector >>= fun state -> f state + +let pre_boot boot_sector f = + parse_boot_sector boot_sector |> function + | None -> failwith "Invalid boot sector" + | Some boot_sector -> setup boot_sector @@ f + +let test_preboot () = + [""; "1"; "1 2 +"] + |> List.iter_es (fun boot_sector -> + pre_boot boot_sector @@ fun _state -> return ()) + +let boot boot_sector f = pre_boot boot_sector @@ fun state -> eval state >>= f + +let test_boot () = + boot "" @@ fun state -> + is_input_state state >>= function + | Some _ -> return () + | _ -> failwith "After booting, the machine must be waiting for input." + +let test_input_message () = + boot "" @@ fun state -> + let input = + { + inbox_level = Raw_level.root; + message_counter = Z.zero; + payload = "MESSAGE"; + } + in + set_input input state >>= fun state -> + eval state >>= fun state -> + is_input_state state >>= function + | Some _ -> + failwith + "After receiving a message, the rollup must not be waiting for input." + | None -> return () + +let go ~max_steps target_status state = + let rec aux i state = + pp state >>= fun pp -> + Format.eprintf "%a" pp () ; + if i > max_steps then + failwith "Maximum number of steps reached before target status." + else + get_status state >>= fun current_status -> + if target_status = current_status then return state + else eval state >>= aux (i + 1) + in + aux 0 state + +let test_parsing_message ~valid (source, expected_code) = + boot "" @@ fun state -> + let input = + {inbox_level = Raw_level.root; message_counter = Z.zero; payload = source} + in + set_input input state >>= fun state -> + eval state >>= fun state -> + go ~max_steps:10000 Evaluating state >>=? fun state -> + get_parsing_result state >>= fun result -> + Assert.equal + ~loc:__LOC__ + (Option.equal Bool.equal) + "Unexpected parsing resutlt" + (fun fmt r -> + Format.fprintf + fmt + (match r with + | None -> "No parsing running" + | Some true -> "Syntax correct" + | Some false -> "Syntax error")) + (Some valid) + result + >>=? fun () -> + if valid then + get_code state >>= fun code -> + Assert.equal + ~loc:__LOC__ + (List.equal equal_instruction) + "The parsed code is not what we expected: " + (Format.pp_print_list pp_instruction) + expected_code + code + else return () + +let syntactically_valid_messages = + List.map + (fun nums -> + ( String.concat " " (List.map string_of_int nums), + List.map (fun x -> IPush x) nums )) + [[0]; [42]; [373]; [0; 1]; [0; 123; 42; 73; 34; 13; 31]] + @ [ + ("1 2 +", [IPush 1; IPush 2; IAdd]); + ( "1 2 3 + + 3 +", + [IPush 1; IPush 2; IPush 3; IAdd; IAdd; IPush 3; IAdd] ); + ("1 2+", [IPush 1; IPush 2; IAdd]); + ("1 2 3++3+", [IPush 1; IPush 2; IPush 3; IAdd; IAdd; IPush 3; IAdd]); + ("", []); + ] + +let syntactically_invalid_messages = + List.map (fun s -> (s, [])) ["a"; " a"; " a "; "---"; "12 +++ --"] + +let test_parsing_messages () = + List.iter_es (test_parsing_message ~valid:true) syntactically_valid_messages + >>=? fun () -> + List.iter_es + (test_parsing_message ~valid:false) + syntactically_invalid_messages + +let test_evaluation_message ~valid (boot_sector, source, expected_stack) = + boot boot_sector @@ fun state -> + let input = + {inbox_level = Raw_level.root; message_counter = Z.zero; payload = source} + in + set_input input state >>= fun state -> + eval state >>= fun state -> + go ~max_steps:10000 WaitingForInputMessage state >>=? fun state -> + if valid then + get_stack state >>= fun stack -> + Assert.equal + ~loc:__LOC__ + (List.equal Compare.Int.equal) + "The stack is not what we expected: " + Format.(pp_print_list (fun fmt -> fprintf fmt "%d;@;")) + expected_stack + stack + else + get_evaluation_result state >>= function + | Some true -> failwith "This code should lead to an evaluation error." + | None -> failwith "We should have reached the evaluation end." + | Some false -> return () + +let valid_messages = + [ + ("", "0", [0]); + ("", "1 2", [2; 1]); + ("", "1 2 +", [3]); + ("", "1 2 + 3 +", [6]); + ("", "1 2 + 3 + 1 1 + +", [8]); + ("0 ", "", [0]); + ("1 ", "2", [2; 1]); + ("1 2 ", "+", [3]); + ("1 2 + ", "3 +", [6]); + ("1 2 + ", "3 + 1 1 + +", [8]); + ] + +let invalid_messages = + List.map (fun s -> ("", s, [])) ["+"; "1 +"; "1 1 + +"; "1 1 + 1 1 + + +"] + +let test_evaluation_messages () = + List.iter_es (test_evaluation_message ~valid:true) valid_messages + >>=? fun () -> + List.iter_es (test_evaluation_message ~valid:false) invalid_messages + +let tests = + [ + Tztest.tztest "PreBoot" `Quick test_preboot; + Tztest.tztest "Boot" `Quick test_boot; + Tztest.tztest "Input message" `Quick test_input_message; + Tztest.tztest "Parsing message" `Quick test_parsing_messages; + Tztest.tztest "Evaluating message" `Quick test_evaluation_messages; + ] diff --git a/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_storage.ml b/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_storage.ml index 429157f666a87f4db62571aa1ca450f35c9c27e9..c7e50d6b9f2d5b433b752e877bddd7a08cf7445a 100644 --- a/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_storage.ml +++ b/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_storage.ml @@ -48,10 +48,7 @@ let new_context () = let new_sc_rollup ctxt = let+ (rollup, _size, ctxt) = - Sc_rollup_storage.originate - ctxt - ~kind:Example_arith - ~boot_sector:(Sc_rollup_repr.PVM.boot_sector_of_string "") + Sc_rollup_storage.originate ctxt ~kind:Example_arith ~boot_sector:"" in (rollup, ctxt)