diff --git a/src/proto_alpha/lib_client/client_proto_context.mli b/src/proto_alpha/lib_client/client_proto_context.mli index 1d1895ad6f7130e2e8623313cf2c8d3b3aa43f05..5a7f5ad63bfaf800b4571e29713479c210742721 100644 --- a/src/proto_alpha/lib_client/client_proto_context.mli +++ b/src/proto_alpha/lib_client/client_proto_context.mli @@ -423,7 +423,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:[`Compressed | `Verifiable | `Full] Sc_rollup.PVM.state -> src_pk:public_key -> src_sk:Client_keys.sk_uri -> fee_parameter:Injection.fee_parameter -> diff --git a/src/proto_alpha/lib_client/operation_result.ml b/src/proto_alpha/lib_client/operation_result.ml index 6bcf9302da4031163d6b575345a77e203c93f830..18721361a4ae15ee78f9117b12af76c58dd9b794 100644 --- a/src/proto_alpha/lib_client/operation_result.ml +++ b/src/proto_alpha/lib_client/operation_result.ml @@ -181,7 +181,7 @@ let pp_manager_operation_content (type kind) source internal pp_result ppf "@[Originate smart contract rollup of kind %s with boot sector \ '%a'%a@]" R.name - R.pp_boot_sector + Sc_rollup.PVM.pp boot_sector pp_result result) ; diff --git a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL index 773866de6a4d4fefd6a3ca2ee0c090a80e1f27e6..f59b57b4c11bb4857f4ccad1496003e8e2efe627 100644 --- a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL +++ b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL @@ -13,8 +13,9 @@ "Blinded_public_key_hash", "Block_payload_hash", "Origination_nonce", - + "Tick_repr", "Sc_rollup_repr", + "Game_repr", "Slot_repr", "Tez_repr", "Period_repr", diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index 4f64a8755d2f14a0fb22c750eb34146761e7469a..b2a15b2fd3594951c86c5e574f357d3216e9459f 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -1903,11 +1903,7 @@ end (** See {!Sc_rollup_storage} and {!Sc_rollup_repr}. *) module Sc_rollup : sig - module PVM : sig - type boot_sector - - val boot_sector_of_string : string -> boot_sector - end + module PVM : Sc_rollup_repr.TPVM module Address : S.HASH @@ -1922,7 +1918,7 @@ module Sc_rollup : sig val originate : context -> kind:Kind.t -> - boot_sector:PVM.boot_sector -> + boot_sector:[`Full | `Verifiable | `Compressed] PVM.state -> (context * t * Z.t) tzresult Lwt.t val kind : context -> t -> Kind.t option tzresult Lwt.t @@ -2107,7 +2103,7 @@ and _ manager_operation = | Tx_rollup_origination : Kind.tx_rollup_origination manager_operation | Sc_rollup_originate : { kind : Sc_rollup.Kind.t; - boot_sector : Sc_rollup.PVM.boot_sector; + boot_sector : [`Compressed | `Verifiable | `Full] Sc_rollup.PVM.state; } -> Kind.sc_rollup_originate manager_operation diff --git a/src/proto_alpha/lib_protocol/dune.inc b/src/proto_alpha/lib_protocol/dune.inc index 42b61fb17400668a960b222231ca183dc95cfd84..2324101a81788db0ac31da74e576e6e6a40a779b 100644 --- a/src/proto_alpha/lib_protocol/dune.inc +++ b/src/proto_alpha/lib_protocol/dune.inc @@ -39,7 +39,9 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end blinded_public_key_hash.mli blinded_public_key_hash.ml block_payload_hash.mli block_payload_hash.ml origination_nonce.mli origination_nonce.ml + tick_repr.mli tick_repr.ml sc_rollup_repr.mli sc_rollup_repr.ml + game_repr.mli game_repr.ml slot_repr.mli slot_repr.ml tez_repr.mli tez_repr.ml period_repr.mli period_repr.ml @@ -176,7 +178,9 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end blinded_public_key_hash.mli blinded_public_key_hash.ml block_payload_hash.mli block_payload_hash.ml origination_nonce.mli origination_nonce.ml + tick_repr.mli tick_repr.ml sc_rollup_repr.mli sc_rollup_repr.ml + game_repr.mli game_repr.ml slot_repr.mli slot_repr.ml tez_repr.mli tez_repr.ml period_repr.mli period_repr.ml @@ -313,7 +317,9 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end blinded_public_key_hash.mli blinded_public_key_hash.ml block_payload_hash.mli block_payload_hash.ml origination_nonce.mli origination_nonce.ml + tick_repr.mli tick_repr.ml sc_rollup_repr.mli sc_rollup_repr.ml + game_repr.mli game_repr.ml slot_repr.mli slot_repr.ml tez_repr.mli tez_repr.ml period_repr.mli period_repr.ml @@ -472,7 +478,9 @@ include Tezos_raw_protocol_alpha.Main Blinded_public_key_hash Block_payload_hash Origination_nonce + Tick_repr Sc_rollup_repr + Game_repr Slot_repr Tez_repr Period_repr @@ -650,7 +658,9 @@ include Tezos_raw_protocol_alpha.Main blinded_public_key_hash.mli blinded_public_key_hash.ml block_payload_hash.mli block_payload_hash.ml origination_nonce.mli origination_nonce.ml + tick_repr.mli tick_repr.ml sc_rollup_repr.mli sc_rollup_repr.ml + game_repr.mli game_repr.ml slot_repr.mli slot_repr.ml tez_repr.mli tez_repr.ml period_repr.mli period_repr.ml diff --git a/src/proto_alpha/lib_protocol/game_repr.ml b/src/proto_alpha/lib_protocol/game_repr.ml new file mode 100644 index 0000000000000000000000000000000000000000..b2edc3278fb820e714b3bf6b3f6a0ec852617434 --- /dev/null +++ b/src/proto_alpha/lib_protocol/game_repr.ml @@ -0,0 +1,510 @@ +(*****************************************************************************) +(* *) +(* 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. *) +(* *) +(*****************************************************************************) + +open Compare.Int +open Sc_rollup_repr + +let repeat n f = List.init ~when_negative_length:[] n f + +module Make (P : TPVM) = struct + module PVM = P + + module Section_repr = struct + type 'k section = { + section_start_state : 'k PVM.state; + section_start_at : PVM.tick; + section_stop_state : 'k PVM.state; + section_stop_at : PVM.tick; + } + + and 'k dissection = 'k section Tick_repr.Map.t + + let section_encoding = + let open Data_encoding in + conv + (fun { + section_start_state; + section_start_at; + section_stop_state; + section_stop_at; + } -> + ( section_start_state, + section_start_at, + section_stop_state, + section_stop_at )) + (fun ( section_start_state, + section_start_at, + section_stop_state, + section_stop_at ) -> + { + section_start_state; + section_start_at; + section_stop_state; + section_stop_at; + }) + (obj4 + (req "section_start_state" PVM.encoding) + (req "section_start_at" Tick_repr.encoding) + (req "section_stop_state" PVM.encoding) + (req "section_stop_at" Tick_repr.encoding)) + + let dissection_encoding = + let open Data_encoding in + let open Tick_repr in + option + @@ conv + (fun map -> List.of_seq @@ Map.to_seq map) + (fun list -> Map.of_seq @@ List.to_seq list) + (list @@ tup2 encoding section_encoding) + + let find_section section (dissection : _ dissection) = + let open Tick_repr in + Option.bind + (Map.find section.section_start_at dissection) + (fun {section_start_at; section_stop_at; _} -> + if + section_start_at = section.section_start_at + && section_stop_at = section.section_stop_at + then Some section + else None) + + let pp_of_section ppf (s : _ section) = + Format.fprintf + ppf + "( %a ) -- [%d] \n ->\n ( %a ) -- [%d]\n " + PVM.pp + s.section_start_state + (s.section_start_at :> int) + PVM.pp + s.section_stop_state + (s.section_stop_at :> int) + + let pp_of_dissection ppf d = + let open Tick_repr in + let list = List.of_seq @@ Map.to_seq d in + Format.pp_print_list + ~pp_sep:(fun ppf () -> Format.pp_print_string ppf ";\n\n") + (fun ppf (key, b) -> + Format.fprintf ppf "key = %a \n val = %a\n" pp key pp_of_section b) + ppf + list + + let pp_optional_dissection d = + Format.pp_print_option + ~none:(fun ppf () -> + Format.pp_print_text ppf "no dissection at the moment") + pp_of_dissection + d + + let valid_section ({section_start_at; section_stop_at; _} : _ section) = + (section_stop_at :> int) > (section_start_at :> int) + + exception Dissection_error of string + + let valid_dissection section dissection = + let open Tick_repr in + let aux section dissection = + Map.fold + (fun _ v acc -> + if acc = v.section_start_at && valid_section v then + v.section_stop_at + else raise (Dissection_error "invalid dissection")) + dissection + section.section_start_at + in + try section.section_stop_at = aux section dissection with _ -> false + + let dissection_of_section history (branching : int) (section : _ section) = + if Tick_repr.(next section.section_start_at = section.section_stop_at) + then None + else + let start = (section.section_start_at :> int) in + let stop = (section.section_stop_at :> int) in + let len = stop - start in + let branching = min len branching in + let bucket = len / branching in + let reminder = len mod branching in + let rec aux index branch rem map = + if index = branch then map + else + let start_at = start + (bucket * index) + min rem index in + let stop_at = + start + (bucket * (index + 1)) + min rem (index + 1) + in + let section_start_at = Tick_repr.make start_at + and section_stop_at = Tick_repr.make stop_at in + let section = + { + section_start_at; + section_start_state = PVM.state_at history section_start_at; + section_stop_at; + section_stop_state = PVM.state_at history section_stop_at; + } + in + let new_map = + Tick_repr.Map.add section.section_start_at section map + in + aux (index + 1) branching rem new_map + in + + let (dissection : _ dissection) = + aux 0 branching reminder Tick_repr.Map.empty + in + Some dissection + end + + type player = Committer | Refuter + + let pp_of_player ppf player = + Format.fprintf + ppf + (match player with Committer -> "committer" | Refuter -> "refuter") + + let player_encoding = + let open Data_encoding in + union + ~tag_size:`Uint8 + [ + case + ~title:"Commiter" + (Tag 0) + string + (function Committer -> Some "committer" | _ -> None) + (fun _ -> Committer); + case + ~title:"Refuter" + (Tag 1) + string + (function Refuter -> Some "refuter" | _ -> None) + (fun _ -> Refuter); + ] + + let opponent = function Committer -> Refuter | Refuter -> Committer + + type t = { + turn : player; + start_state : [`Compressed | `Full | `Verifiable] PVM.state; + start_at : PVM.tick; + player_stop_state : [`Compressed | `Full | `Verifiable] PVM.state; + opponent_stop_state : [`Compressed | `Full | `Verifiable] PVM.state; + stop_at : PVM.tick; + current_dissection : + [`Compressed | `Full | `Verifiable] Section_repr.dissection option; + } + + let encoding = + let open Data_encoding in + conv + (fun { + turn; + start_state; + start_at; + player_stop_state; + opponent_stop_state; + stop_at; + current_dissection; + } -> + ( turn, + start_state, + start_at, + player_stop_state, + opponent_stop_state, + stop_at, + current_dissection )) + (fun ( turn, + start_state, + start_at, + player_stop_state, + opponent_stop_state, + stop_at, + current_dissection ) -> + { + turn; + start_state; + start_at; + player_stop_state; + opponent_stop_state; + stop_at; + current_dissection; + }) + (obj7 + (req "turn" player_encoding) + (req "start_state" PVM.encoding) + (req "start_at" Tick_repr.encoding) + (req "player_stop_state" PVM.encoding) + (req "oponent_stop_state" PVM.encoding) + (req "stop_at" Tick_repr.encoding) + (req "current_dissection" Section_repr.dissection_encoding)) + + type conflict_search_step = + | Refine of { + stop_state : [`Compressed | `Full | `Verifiable] PVM.state; + next_dissection : + [`Compressed | `Full | `Verifiable] Section_repr.dissection; + } + | Conclude : { + start_state : ([`Compressed | `Full | `Verifiable] as 'a) PVM.state; + stop_state : [`Compressed | `Full | `Verifiable] PVM.state; + } + -> conflict_search_step + + type move = + | ConflictInside of { + choice : [`Compressed | `Full | `Verifiable] Section_repr.section; + conflict_search_step : conflict_search_step; + } + + type commit = + | Commit of [`Compressed | `Full | `Verifiable] Section_repr.section + + type refutation = RefuteByConflict of conflict_search_step + + type reason = InvalidMove | ConflictResolved + + let pp_of_reason ppf reason = + Format.fprintf + ppf + "%s" + (match reason with + | InvalidMove -> "invalid move" + | ConflictResolved -> "conflict resolved") + + type outcome = {winner : player option; reason : reason} + + let pp_of_winner winner = + Format.pp_print_option + ~none:(fun ppf () -> Format.pp_print_text ppf "no winner") + pp_of_player + winner + + let pp_of_outcome ppf {winner; reason} = + Format.fprintf + ppf + "%a because of %a" + pp_of_winner + winner + pp_of_reason + reason + + type state = Over of outcome | Ongoing of t + + let pp_of_game ppf g = + Format.fprintf + ppf + "%a @ %d -> %a / %a @ %d [%a] %s playing" + PVM.pp + g.start_state + (g.start_at :> int) + PVM.pp + g.player_stop_state + PVM.pp + g.opponent_stop_state + (g.stop_at :> int) + Section_repr.pp_optional_dissection + g.current_dissection + (match g.turn with Committer -> "committer" | Refuter -> "refuter") + + let pp_of_move ppf = function + | ConflictInside + {choice; conflict_search_step = Refine {next_dissection; stop_state}} -> + Format.fprintf + ppf + "conflict is inside %a, should end with %a, new dissection = %a" + Section_repr.pp_of_section + choice + PVM.pp + stop_state + Section_repr.pp_of_dissection + next_dissection + | ConflictInside + {choice; conflict_search_step = Conclude {start_state; stop_state}} -> + Format.fprintf + ppf + "atomic conflict found inside %a, we can verify that it starts with \ + %a and should end with %a" + Section_repr.pp_of_section + choice + PVM.pp + start_state + PVM.pp + stop_state + + let conflict_found (game : t) = + Compare.Int.((game.stop_at :> int) - (game.start_at :> int) = 1) + + let stop_state = function + | Refine {stop_state; _} -> stop_state + | Conclude {stop_state; _} -> stop_state + + let initial (Commit commit) (refutation : conflict_search_step) = + let game = + { + start_state = commit.section_start_state; + start_at = commit.section_start_at; + opponent_stop_state = commit.section_stop_state; + stop_at = commit.section_stop_at; + player_stop_state = stop_state refutation; + current_dissection = None; + turn = Refuter; + } + in + let choice = commit in + let move = ConflictInside {choice; conflict_search_step = refutation} in + (game, move) + + let resolve_conflict (game : t) verifiable_start_state = + let open PVM in + assert (conflict_found game) ; + let player = game.turn in + let over winner = {winner; reason = ConflictResolved} in + match eval ~failures:[] game.start_at verifiable_start_state with + | stop_state -> ( + let player_state_valid = + Internal_for_tests.equal_state stop_state game.player_stop_state + in + let opponent_state_valid = + Internal_for_tests.equal_state stop_state game.opponent_stop_state + in + match (player_state_valid, opponent_state_valid) with + | (true, true) -> over @@ Some Committer + | (true, false) -> over @@ Some player + | (false, true) -> over @@ Some (opponent player) + | (false, false) -> over @@ None) + + let apply_choice ~(game : t) ~(choice : _ Section_repr.section) + chosen_stop_state = + Option.bind + (match game.current_dissection with + | Some dissection -> + Section_repr.find_section choice dissection + (* TODO faster binary search in the list if we have binary tree.*) + | None -> + if + PVM.Internal_for_tests.equal_state + choice.section_start_state + game.start_state + then Some choice + else None) + @@ fun ({ + section_start_state; + section_start_at; + section_stop_state; + section_stop_at; + } : + _ Section_repr.section) -> + if PVM.Internal_for_tests.equal_state chosen_stop_state section_stop_state + then None + else + Some + { + game with + start_state = section_start_state; + start_at = section_start_at; + opponent_stop_state = section_stop_state; + player_stop_state = chosen_stop_state; + stop_at = section_stop_at; + } + + let apply_dissection ~(game : t) (next_dissection : _ Section_repr.dissection) + = + let current_section : _ Section_repr.section = + { + section_start_state = game.start_state; + section_start_at = game.start_at; + section_stop_state = game.opponent_stop_state; + section_stop_at = game.stop_at; + } + in + if Section_repr.valid_dissection current_section next_dissection then + Some {game with current_dissection = Some next_dissection} + else None + + let verifiable_representation vstate state = + if PVM.Internal_for_tests.equal_state vstate state then Some () else None + + let play game (ConflictInside {choice; conflict_search_step}) = + let player = game.turn in + + let apply_move () = + match conflict_search_step with + | Refine {next_dissection; stop_state} -> + Option.bind (apply_choice ~game ~choice stop_state) @@ fun game -> + Option.bind (apply_dissection ~game next_dissection) @@ fun game -> + Some (Ongoing game) + | Conclude {start_state; stop_state} -> + Option.bind (apply_choice ~game ~choice stop_state) @@ fun game -> + Option.bind (verifiable_representation start_state game.start_state) + @@ fun () -> + if conflict_found game then + Some (Over (resolve_conflict game start_state)) + else None + in + match apply_move () with + | None -> Over {winner = Some (opponent player); reason = InvalidMove} + | Some state -> state + + type ('from, 'initial) client = { + initial : 'from -> 'initial; + next_move : + [`Compressed | `Full | `Verifiable] Section_repr.dissection -> move; + } + + let run ~start_at + ~(start_state : [`Compressed | `Verifiable | `Full] PVM.state) ~committer + ~refuter = + let (Commit commit) = committer.initial (start_at, start_state) in + let (RefuteByConflict refutation) = + refuter.initial (start_state, Commit commit) + in + let outcome = + let rec loop game move = + match play game move with + | Over outcome -> outcome + | Ongoing game -> + let game = {game with turn = opponent game.turn} in + let move = + match game.turn with + | Committer -> + let nm = + committer.next_move + (Option.value + ~default:Tick_repr.Map.empty + game.current_dissection) + in + nm + | Refuter -> + refuter.next_move + (Option.value + ~default:Tick_repr.Map.empty + game.current_dissection) + in + loop game move + in + let (game, move) = initial (Commit commit) refutation in + loop game move + in + outcome +end diff --git a/src/proto_alpha/lib_protocol/game_repr.mli b/src/proto_alpha/lib_protocol/game_repr.mli new file mode 100644 index 0000000000000000000000000000000000000000..ba0aa41d68a7b4b002bf51253ffbe96212561e93 --- /dev/null +++ b/src/proto_alpha/lib_protocol/game_repr.mli @@ -0,0 +1,295 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2021 Nomadic Labs and *) +(* 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 creates a refutation game for Optimistic rollup. + It is in fact a functor that takes a PVM module and produce a game. + + Expected properties + =================== + + Honest-committer-wins: + - If a committer has posted a valid commit and has a perfect PVM at hand, + there is a winning strategy which consists in choosing the first section + of the current dissection and in producing a regular dissection until the + conflict is reached. + + Honest-refuter-wins: + - If a refuter has detected an invalid commit and has a perfect PVM at hand, + the same strategy is also winning. + + Here "winning strategy" means that the player actually wins (a draw is not + enough). + + + Important invariants + ==================== + + - The committer and the refuter agree on the first state of the current + section and disagree on its final state. If they agree on both then whoever plays loses by InvalidMove. + + Remarks + ======= + + There are several subtle cornercases: + + - If the refuter and the committer both post only invalid states, the + game may end in a conflict state where both are wrong. By convention, + we decide that these games have no winner. + + - If the refuter and the committer both post only states, the + game never has any conflicts. By convention, + we decide that in this case the commiter winds by InvalidMove. + + - If the refuter and the committer both post valid and invalid states, + all outcomes are possible. This means that if a committer wins a + game we have no guarantee that she has posted a valid commit. + + +*) + +val repeat : int -> (int -> 'a) -> ('a list, 'b list) result + +module Make : functor (P : Sc_rollup_repr.TPVM) -> sig + module PVM : + Sc_rollup_repr.TPVM + with type 'a state = 'a P.state + and type history = P.history + + (** This submodule introduces sections and dissections and the functions that build them +*) + module Section_repr : sig + (** a section has a start and end tick as well as a start and end state. + The game will compare such sections and dissagree on them.*) + type 'k section = { + section_start_state : 'k P.state; + section_start_at : Tick_repr.t; + section_stop_state : 'k P.state; + section_stop_at : Tick_repr.t; + } + + (**a dissection is a split of a section in several smaller sections. it is defined as a map + based on start_at (which are increasing) rather than a list.*) + and 'k dissection = 'k section Tick_repr.Map.t + + val section_encoding : + [`Compressed | `Full | `Verifiable] section Data_encoding.t + + val dissection_encoding : + [`Compressed | `Full | `Verifiable] dissection option Data_encoding.t + + val find_section : 'a section -> 'a dissection -> 'a section option + + val pp_of_section : + Format.formatter -> [`Compressed | `Full | `Verifiable] section -> unit + + val pp_of_dissection : + Format.formatter -> [`Compressed | `Full | `Verifiable] dissection -> unit + + val pp_optional_dissection : + Format.formatter -> + [`Compressed | `Full | `Verifiable] dissection option -> + unit + + (** a section is valid if its star_at tick is smaller than it stop_at tick.*) + val valid_section : 'a section -> bool + + exception Dissection_error of string + + (** + + A dissection is valid if it is composed of a list of contiguous + sections that covers a given [section]. + + In practice, we also want sections to be balanced in terms of gas + they consume to avoid strategies that slowdown convergence. + + the function valid_dissection checks if a dissection is valid and, if so, + it verifies that it is a dissection of the given section. + + *) + val valid_dissection : 'a section -> 'a dissection -> bool + + (** This function takes a section and an integer branching and creates a dissection with branching number of pieces that + are (roughly) equal and whose states come from the history. + Assume that length of the initial section is len and len mod branching = r. We have the following invariants: + - if branching >len then we make branching = len (split the section into one tick sections) + - valid_disection section (dissection_of_section history branching section)=true + - The first r pieces are one tick longer than the rest (the alternative would have been for the last piece to be a lot longer) + *) + val dissection_of_section : + PVM.history -> + int -> + 'a section -> + [`Compressed | `Full | `Verifiable] dissection option + end + + type player = Committer | Refuter + + val pp_of_player : Format.formatter -> player -> unit + + val player_encoding : player Data_encoding.t + + val opponent : player -> player + + (** this is the type (state) of a game at a certain moment.It indicates the following: + - whose turn it is, + - where does it start and where does it stop + - the agreed starting state and the disagreed stop state, + _ the current dissection that teh player should choose from.*) + type t = { + turn : player; + start_state : [`Compressed | `Full | `Verifiable] P.state; + start_at : Tick_repr.t; + player_stop_state : [`Compressed | `Full | `Verifiable] P.state; + opponent_stop_state : [`Compressed | `Full | `Verifiable] P.state; + stop_at : Tick_repr.t; + current_dissection : + [`Compressed | `Full | `Verifiable] Section_repr.dissection option; + } + + val encoding : t Data_encoding.t + + (** a conflict_search_step can either be a refining of an existing section or a concluded + step.*) + type conflict_search_step = + | Refine of { + stop_state : [`Compressed | `Full | `Verifiable] P.state; + next_dissection : + [`Compressed | `Full | `Verifiable] Section_repr.dissection; + } + | Conclude : { + start_state : [`Compressed | `Full | `Verifiable] P.state; + stop_state : [`Compressed | `Full | `Verifiable] P.state; + } + -> conflict_search_step + + (** a move consists of a choice of a section and a conflict_search step. +Note that there is some overlap of the info in a move.*) + type move = + | ConflictInside of { + choice : [`Compressed | `Full | `Verifiable] Section_repr.section; + conflict_search_step : conflict_search_step; + } + + (** the commiter commits a section *) + type commit = + | Commit of [`Compressed | `Full | `Verifiable] Section_repr.section + + (** the refuter refutes a conflict_search_step*) + type refutation = RefuteByConflict of conflict_search_step + + type reason = InvalidMove | ConflictResolved + + val pp_of_reason : Format.formatter -> reason -> unit + + (** the outcome of a finished game gives the winner as well as the reason for winning*) + type outcome = {winner : player option; reason : reason} + + val pp_of_winner : Format.formatter -> player option -> unit + + val pp_of_outcome : Format.formatter -> outcome -> unit + + (** a game can be over witha given outcome or Ongoing with a given game state*) + type state = Over of outcome | Ongoing of t + + val pp_of_game : Format.formatter -> t -> unit + + val pp_of_move : Format.formatter -> move -> unit + + (** [confict_found game] is [true] iff the [game]'s section is + one tick long. *) + val conflict_found : t -> bool + + (** this function extracts the stop state of a conflict_search_step*) + val stop_state : + conflict_search_step -> [`Compressed | `Full | `Verifiable] P.state + + (** + + The initial game state from the commit and the refutation. + + The first player to play is the refuter. + + *) + val initial : commit -> conflict_search_step -> t * move + + (** + + Assuming a [game] where the current section is one tick long, + [resolve_conflict game] determines the [game] outcome. + + *) + val resolve_conflict : t -> [> `Verifiable] P.state -> outcome + + (** [apply_choice turn game choice chosen_stop_state] returns [Some + game'] state where the [choice] of the [turn]'s player is applied + to [game] and justified by [chosen_stop_state]. + + If the [choice] is invalid, this function returns [None]. *) + val apply_choice : + game:t -> + choice:[`Compressed | `Full | `Verifiable] Section_repr.section -> + [`Compressed | `Full | `Verifiable] P.state -> + t option + + (** [apply_dissection game next_dissection] returns [Some game'] + where the [current_dissection] is the [next_dissection] if + it is valid. Otherwise, this function returns [None]. *) + val apply_dissection : + game:t -> + [`Compressed | `Full | `Verifiable] Section_repr.dissection -> + t option + + val verifiable_representation : 'a P.state -> 'b P.state -> unit option + + (** [playe game move] returns the state of the [game] after that + [move] has been applied, if [move] is valid. Otherwise, this + function returns an game over due to InvalidMove. *) + val play : t -> move -> state + + (** a client is a strategy for a player. It consists of an initial move and a function that + picks the next move once the oponent gives ou a dissection. + In practice + - the commuter will be a ((tick * _ state) * commit) client + - the refuter will be a ((_ state * commit) * refutation) client *) + + type ('from, 'initial) client = { + initial : 'from -> 'initial; + next_move : + [`Compressed | `Full | `Verifiable] Section_repr.dissection -> move; + } + + (** this is the function that runs a game. + It receives a starting tick and a starting state as well as commiter and refuter clients and + outputs the outcome of the refutation game.*) + + val run : + start_at:'a -> + start_state:[`Compressed | `Full | `Verifiable] P.state -> + committer:('a * [`Compressed | `Full | `Verifiable] P.state, commit) client -> + refuter: + ([`Compressed | `Full | `Verifiable] P.state * commit, refutation) client -> + outcome +end diff --git a/src/proto_alpha/lib_protocol/operation_repr.ml b/src/proto_alpha/lib_protocol/operation_repr.ml index 15a222a675603600c02a889be11bfe551b0ddcc7..e0f2b93f74f6084894d074a5171f3d696dc6cb31 100644 --- a/src/proto_alpha/lib_protocol/operation_repr.ml +++ b/src/proto_alpha/lib_protocol/operation_repr.ml @@ -264,7 +264,7 @@ and _ manager_operation = | Tx_rollup_origination : Kind.tx_rollup_origination manager_operation | Sc_rollup_originate : { kind : Sc_rollup_repr.Kind.t; - boot_sector : Sc_rollup_repr.PVM.boot_sector; + boot_sector : [`Compressed | `Verifiable | `Full] Sc_rollup_repr.PVM.state; } -> Kind.sc_rollup_originate manager_operation @@ -503,7 +503,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" Sc_rollup_repr.PVM.encoding); 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 dd279466c4d527949db9fa5587a453e01e1eda82..5f62c2f98d9d6d4697fd929c3dd260f7b5585da8 100644 --- a/src/proto_alpha/lib_protocol/operation_repr.mli +++ b/src/proto_alpha/lib_protocol/operation_repr.mli @@ -242,7 +242,7 @@ and _ manager_operation = | Tx_rollup_origination : Kind.tx_rollup_origination manager_operation | Sc_rollup_originate : { kind : Sc_rollup_repr.Kind.t; - boot_sector : Sc_rollup_repr.PVM.boot_sector; + boot_sector : [`Compressed | `Verifiable | `Full] Sc_rollup_repr.PVM.state; } -> Kind.sc_rollup_originate manager_operation diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml index c6b131c0b0976168096181cf1c135203c645879e..60a14a26ed0b246fc46cc8ae363582a488278ea7 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml @@ -22,10 +22,8 @@ (* DEALINGS IN THE SOFTWARE. *) (* *) (*****************************************************************************) +open Alpha_context.Sc_rollup let name = "arith" -let parse_boot_sector _ = - Some (Alpha_context.Sc_rollup.PVM.boot_sector_of_string "") - -let pp_boot_sector _fmt _ = () +let parse_boot_sector (_ : string) = Some PVM.Internal_for_tests.initial_state diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli index 4162b3598cf86414cd307d49627bfbe4d916bf1f..b1733450ef5abf8dc2dec3e4b0771bafaaafa59e 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli @@ -29,6 +29,5 @@ open Alpha_context.Sc_rollup val name : string -val parse_boot_sector : string -> PVM.boot_sector option - -val pp_boot_sector : Format.formatter -> PVM.boot_sector -> unit +val parse_boot_sector : + string -> [`Compressed | `Full | `Verifiable] PVM.state option diff --git a/src/proto_alpha/lib_protocol/sc_rollup_operations.mli b/src/proto_alpha/lib_protocol/sc_rollup_operations.mli index c8f31e0637066e9d9cd708ad7a3bb58b9332b198..61002e23e3ac0aaa31291392c6cb962ccc3c229c 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:[`Compressed | `Verifiable | `Full] Sc_rollup.PVM.state -> (context * origination_result) 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 3abbbbc164ede1441a646c56e1720d89247c8a0c..87c978698b3d2d08d9a70572d40c6f14def12334 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.ml @@ -23,13 +23,155 @@ (* *) (*****************************************************************************) -module PVM = struct - type boot_sector = string +exception TickNotFound of Tick_repr.t - let boot_sector_encoding = Data_encoding.string +module type TPVM = sig + type _ state - let boot_sector_of_string s = s + (** + + The state of the PVM represents a concrete execution state of the + underlying machine. Let us write [concrete_of state] to denote + the underlying concrete state of some PVM [state]. + + This state is probably not implemented exactly as in the + underlying machine because it must be useful for proof generation + and proof validation. + + In particular, a state can be a lossy compression of the concrete + machine state, typically a hash of this state. This is useful to + transmit a short fingerprint of this state to the layer 1. + + A state can also be *verifiable* which means that it exposes + enough structure to validate an execution step of the machine. + + A state must finally be *serializable* as it must be transmitted + from rollup participants to the layer 1. + + *) + + module Internal_for_tests : sig + (** The following three functions are for testing purposes. *) + + val initial_state : [`Compressed | `Verifiable | `Full] state + + val random_state : + int -> + [`Compressed | `Verifiable | `Full] state -> + [`Compressed | `Verifiable | `Full] state + + (** [equal_state s1 s2] is [true] iff [concrete_of_state s1] + is equal to [concrete_of_state s2]. *) + val equal_state : _ state -> _ state -> bool + end + + (** The history of an execution. *) + type history + + val empty_history : history + + (** We want to navigate into the history using a trace counter. *) + type tick = Tick_repr.t + + val encoding : [`Compressed | `Verifiable | `Full] state Data_encoding.t + + val remember : + history -> tick -> [`Compressed | `Verifiable | `Full] state -> history + + val compress : _ state -> [`Compressed] state + + val verifiable_state_at : + history -> tick -> [`Compressed | `Verifiable | `Full] state + + (** [state_at p tick] returns a full representation of [concrete_of + state] at the given trace counter [tick]. *) + val state_at : history -> tick -> [`Compressed | `Verifiable | `Full] state + + val pp : Format.formatter -> [`Compressed | `Verifiable | `Full] state -> unit + + (** [eval failures tick state] executes the machine at [tick] + assuming a given machine [state]. The function returns the state + at the [next tick]. + + [failures] is here for testing purpose: an error is intentionally + inserted for ticks in [failures]. + *) + val eval : + failures:tick list -> tick -> ([> `Verifiable] as 'a) state -> 'a state + + (** [execute_until failures tick state pred] applies [eval] + starting from a [tick] and a [state] and returns the first + [tick] and [state] where [pred tick state] is [true], or + diverges if such a configuration does not exist. *) + val execute_until : + failures:tick list -> + tick -> + ([> `Verifiable] as 'a) state -> + (tick -> 'a state -> bool) -> + tick * 'a state +end + +module PVM : TPVM with type _ state = string = struct + type _ state = string + + module Internal_for_tests = struct + let initial_state = "init" + + let random_state _ (st : _ state) = st + + let equal_state = String.equal + end + + type tick = Tick_repr.t + + type history = string Tick_repr.Map.t + + let encoding = Data_encoding.string + + let remember history (tick : tick) state = + Tick_repr.Map.add tick state history + + let pp = Format.pp_print_string + + let empty_history = Tick_repr.Map.empty + + let eval ~failures (tick : Tick_repr.t) state = + if List.mem ~equal:Tick_repr.( = ) tick failures then "" else state + + let execute_until ~failures tick state pred = + let rec loop state tick = + if pred tick state then (tick, state) + else + let state = eval ~failures tick state in + loop state (Tick_repr.next tick) + in + loop state tick + + let state_at history tick = + let open Tick_repr in + let (lower, ostate, _) = Tick_repr.Map.split tick history in + match ostate with + | Some state -> state + | None -> + let (tick0, state0) = + Option.value + ~default:(Tick_repr.make 0, Internal_for_tests.initial_state) + (Tick_repr.Map.max_binding lower) + in + snd + (execute_until ~failures:[] tick0 state0 (fun tick' _ -> tick' = tick)) + + let verifiable_state_at = state_at + + let compress x = x end +(* 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 df68d4559e6f64010490353a978a6fb4b3593ad7..70844ab2b088dbf85eb5d1c5605f5b067f258ad0 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_repr.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_repr.mli @@ -38,15 +38,95 @@ 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 +exception TickNotFound of Tick_repr.t - val boot_sector_of_string : string -> boot_sector +module type TPVM = sig + type _ state + + (** + + The state of the PVM represents a concrete execution state of the + underlying machine. Let us write [concrete_of state] to denote + the underlying concrete state of some PVM [state]. + + This state is probably not implemented exactly as in the + underlying machine because it must be useful for proof generation + and proof validation. + + In particular, a state can be a lossy compression of the concrete + machine state, typically a hash of this state. This is useful to + transmit a short fingerprint of this state to the layer 1. + + A state can also be *verifiable* which means that it exposes + enough structure to validate an execution step of the machine. + + A state must finally be *serializable* as it must be transmitted + from rollup participants to the layer 1. + + *) + module Internal_for_tests : sig + (** The following three functions are for testing purposes. *) + val initial_state : [`Compressed | `Verifiable | `Full] state + + val random_state : + int -> + [`Compressed | `Verifiable | `Full] state -> + [`Compressed | `Verifiable | `Full] state + + (** [equal_state s1 s2] is [true] iff [concrete_of_state s1] + is equal to [concrete_of_state s2]. *) + val equal_state : _ state -> _ state -> bool + end + + (** The history of an execution. *) + type history + + val empty_history : history + + (** We want to navigate into the history using a trace counter. *) + type tick = Tick_repr.t + + val encoding : [`Compressed | `Verifiable | `Full] state Data_encoding.t + + val remember : + history -> tick -> [`Compressed | `Verifiable | `Full] state -> history + + val compress : _ state -> [`Compressed] state + + val verifiable_state_at : + history -> tick -> [`Compressed | `Verifiable | `Full] state + + (** [state_at p tick] returns a full representation of [concrete_of + state] at the given trace counter [tick]. *) + val state_at : history -> tick -> [`Compressed | `Verifiable | `Full] state + + val pp : Format.formatter -> [`Compressed | `Verifiable | `Full] state -> unit + + (** [eval failures tick state] executes the machine at [tick] + assuming a given machine [state]. The function returns the state + at the [next tick]. + + [failures] is here for testing purpose: an error is intentionally + inserted for ticks in [failures]. + *) + val eval : + failures:tick list -> tick -> ([> `Verifiable] as 'a) state -> 'a state + + (** [execute_until failures tick state pred] applies [eval] + starting from a [tick] and a [state] and returns the first + [tick] and [state] where [pred tick state] is [true], or + diverges if such a configuration does not exist. *) + val execute_until : + failures:tick list -> + tick -> + ([> `Verifiable] as 'a) state -> + (tick -> 'a state -> bool) -> + tick * 'a state end +module PVM : TPVM + (** A smart-contract rollup has an address starting with "scr1". *) module Address : sig include S.HASH diff --git a/src/proto_alpha/lib_protocol/sc_rollup_storage.ml b/src/proto_alpha/lib_protocol/sc_rollup_storage.ml index c9500266b5b184729574e57a39a437acd9d1a68a..eb44a5b898729d2a0080c00c6756fe4e99cd701d 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_storage.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_storage.ml @@ -31,9 +31,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 Sc_rollup_repr.PVM.encoding 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 3086e14cf1928fe4aa5f9da6e6bfbcdb88f73cf4..656661408d0ac61e1c1d03dee8542c10fd712e7a 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_storage.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_storage.mli @@ -33,7 +33,7 @@ val originate : Raw_context.t -> kind:Sc_rollup_repr.Kind.t -> - boot_sector:Sc_rollup_repr.PVM.boot_sector -> + boot_sector:[`Compressed | `Verifiable | `Full] Sc_rollup_repr.PVM.state -> (Raw_context.t * Sc_rollup_repr.Address.t * Z.t) tzresult Lwt.t (** [kind context address] returns [Some kind] iff [address] is an diff --git a/src/proto_alpha/lib_protocol/sc_rollups.ml b/src/proto_alpha/lib_protocol/sc_rollups.ml index ef115a9b95fd271fbde94cca81939d34ceb70f4d..98816ee5b08048c405ded88d29d39df968d9499c 100644 --- a/src/proto_alpha/lib_protocol/sc_rollups.ml +++ b/src/proto_alpha/lib_protocol/sc_rollups.ml @@ -26,14 +26,11 @@ open Alpha_context.Sc_rollup module PVM = struct - type boot_sector = Alpha_context.Sc_rollup.PVM.boot_sector - module type S = sig val name : string - val parse_boot_sector : string -> boot_sector option - - val pp_boot_sector : Format.formatter -> boot_sector -> unit + val parse_boot_sector : + string -> [`Compressed | `Full | `Verifiable] PVM.state option end type t = (module S) @@ -43,7 +40,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 PVM.S) = (module Sc_rollup_arith) 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..40ccda7654b3b952e5544e6b375859bf5eb723da 100644 --- a/src/proto_alpha/lib_protocol/sc_rollups.mli +++ b/src/proto_alpha/lib_protocol/sc_rollups.mli @@ -27,14 +27,11 @@ open Alpha_context.Sc_rollup module PVM : sig - type boot_sector = Alpha_context.Sc_rollup.PVM.boot_sector - module type S = sig val name : string - val parse_boot_sector : string -> boot_sector option - - val pp_boot_sector : Format.formatter -> boot_sector -> unit + val parse_boot_sector : + string -> [`Compressed | `Full | `Verifiable] PVM.state option end type t = (module S) diff --git a/src/proto_alpha/lib_protocol/storage.ml b/src/proto_alpha/lib_protocol/storage.ml index 26e832f5c819c5ee5bad8b7693ceca99a52c91a6..562a3e430097f77d1ee6eda4d17e30f0673da397 100644 --- a/src/proto_alpha/lib_protocol/storage.ml +++ b/src/proto_alpha/lib_protocol/storage.ml @@ -1682,8 +1682,8 @@ module Sc_rollup = struct let name = ["boot_sector"] end) (struct - type t = Sc_rollup_repr.PVM.boot_sector + type t = [`Compressed | `Verifiable | `Full] Sc_rollup_repr.PVM.state - let encoding = Sc_rollup_repr.PVM.boot_sector_encoding + let encoding = Sc_rollup_repr.PVM.encoding end) end diff --git a/src/proto_alpha/lib_protocol/storage.mli b/src/proto_alpha/lib_protocol/storage.mli index f5e3334e6d563136b6cc398c181968573e90a64b..29926aa6852dc21b9f2eb90b02d1e4a6c193921a 100644 --- a/src/proto_alpha/lib_protocol/storage.mli +++ b/src/proto_alpha/lib_protocol/storage.mli @@ -722,6 +722,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 = + [`Full | `Verifiable | `Compressed] Sc_rollup_repr.PVM.state and type t := Raw_context.t end diff --git a/src/proto_alpha/lib_protocol/test/helpers/op.mli b/src/proto_alpha/lib_protocol/test/helpers/op.mli index fc460753cf28814b3314da389d8383f14f770e74..90935afec7609af804774ee4d8d377006c308aa5 100644 --- a/src/proto_alpha/lib_protocol/test/helpers/op.mli +++ b/src/proto_alpha/lib_protocol/test/helpers/op.mli @@ -214,5 +214,5 @@ val sc_rollup_origination : Context.t -> Contract.t -> Sc_rollup.Kind.t -> - Sc_rollup.PVM.boot_sector -> + [`Compressed | `Verifiable | `Full] Sc_rollup.PVM.state -> packed_operation tzresult Lwt.t 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..f9c70e893ec1c4cbada08ba85d21f62a167fe226 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 = Sc_rollup.PVM.Internal_for_tests.initial_state 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 159a94a6ff656497b596698c12c6cf5d14af96d7..d9740a86f838dcfaa0d289fe30711da1749fdf86 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/dune +++ b/src/proto_alpha/lib_protocol/test/pbt/dune @@ -1,6 +1,7 @@ (tests (package tezos-protocol-alpha-tests) (names liquidity_baking_pbt + refutation_game_pbt saturation_fuzzing test_gas_properties test_sampler diff --git a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml new file mode 100644 index 0000000000000000000000000000000000000000..f5e74dbf30256f09d114ce7fd80e61201ccad609 --- /dev/null +++ b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml @@ -0,0 +1,1496 @@ +(*****************************************************************************) +(* *) +(* 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. *) +(* *) +(*****************************************************************************) + +(** Testing + ------- + Component: Protocol Library + Invocation: dune exec \ + src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.exe + Subject: SCORU refutation game +*) +open Protocol + +open Game_repr + +exception TickNotFound of Tick_repr.t + +open Lib_test.Qcheck_helpers + +(** +Helpers +*) +let option_get = function + | Some a -> a + | None -> raise (Invalid_argument "option is None") + +(** this is avery simple PVM whose state is an integer and who can count up to a certin target.*) +module MakeCountingPVM (P : sig + val target : int +end) : Sc_rollup_repr.TPVM with type _ state = int = struct + type _ state = int + + let compress x = x + + module Internal_for_tests = struct + let initial_state = 0 + + let random_state _ _ = Random.bits () + + let equal_state = ( = ) + end + + let pp ppf = Format.fprintf ppf "%d" + + type tick = Tick_repr.t + + type history = {states : int Tick_repr.Map.t; tick : tick} + + let encoding = Data_encoding.int16 + + let remember history tick state = + {history with states = Tick_repr.Map.add tick state history.states} + + let eval ~failures (tick : Tick_repr.t) state = + if state >= P.target then state + else if List.mem ~equal:Tick_repr.( = ) tick failures then state + else state + 1 + + let execute_until ~failures tick state pred = + let rec loop state tick = + if pred tick state then (tick, state) + else + let state = eval ~failures tick state in + loop state (Tick_repr.next tick) + in + loop state tick + + let state_at history tick = + let (lower, ostate, _) = Tick_repr.Map.split tick history.states in + match ostate with + | Some state -> state + | None -> + let (tick0, state0) = + match Tick_repr.Map.max_binding lower with + | Some s -> s + | None -> (Tick_repr.make 0, 0) + in + snd + (execute_until ~failures:[] tick0 state0 (fun tick' _ -> tick' = tick)) + + let verifiable_state_at = state_at + + let empty_history = {states = Tick_repr.Map.empty; tick = Tick_repr.make 0} +end + +let operation state number = + Digest.bytes @@ Bytes.of_string @@ state ^ string_of_int number + +(** this is a simple "random PVM" its state is a pair (state, prog) whee state is a string and +prog is a list of integers representing the a program. evaluation just consumes the head of program +and modifies state by concatenating the head of the program to the existing state and hashing the result. +It is initiated with an initialprgram that creates the initial state. *) +module MakeRandomPVM (P : sig + val initial_prog : int list +end) : Sc_rollup_repr.TPVM with type _ state = string * int list = struct + type _ state = string * int list + + let compress x = x + + module Internal_for_tests = struct + let initial_state = ("hello", P.initial_prog) + + let random_state length ((_, program) : _ state) = + let remaining_program = TzList.drop_n length program in + let (stop_state : _ state) = + (operation "" (Random.bits ()), remaining_program) + in + stop_state + + let equal_state = ( = ) + end + + let pp ppf (st, li) = + Format.fprintf ppf "%s@ %a" st (Format.pp_print_list Format.pp_print_int) li + + type history = { + states : [`Compressed | `Verifiable | `Full] state Tick_repr.Map.t; + tick : Tick_repr.t; + } + + let encoding = + let open Data_encoding in + conv + (fun (value, list) -> (value, list)) + (fun (value, list) -> (value, list)) + (tup2 string (list int16)) + + let remember history tick state = + {history with states = Tick_repr.Map.add tick state history.states} + + let eval ~failures (tick : Tick_repr.t) ((hash, continuation) as state) = + match continuation with + | [] -> state + | h :: tl -> + if List.mem ~equal:( = ) tick failures then (hash, tl) + else (operation hash h, tl) + + let execute_until ~failures tick state pred = + let rec loop state tick = + if pred tick state || snd state = [] then (tick, state) + else + let state = eval ~failures tick state in + loop state (Tick_repr.next tick) + in + loop state tick + + let state_at history tick = + let (lower, ostate, _) = Tick_repr.Map.split tick history.states in + match ostate with + | Some state -> state + | None -> + let (tick0, state0) = + match Tick_repr.Map.max_binding lower with + | Some (t, s) -> (t, s) + | None -> (Tick_repr.make 0, Internal_for_tests.initial_state) + in + snd + (execute_until ~failures:[] tick0 state0 (fun tick' _ -> tick' = tick)) + + let verifiable_state_at = state_at + + let empty_history = {states = Tick_repr.Map.empty; tick = Tick_repr.make 0} + + type tick = Tick_repr.t +end + +(** This is a mor ecomplicated PVM introducing a subset of +Michelson instructions. the eval functions pretty much like the +evaluation of a smart contract.*) +module MerkelizedMichelson = struct + (** + + We assume the existence of some cryptographic hashing + function. Notice that such function is relatively slow. + Therefore, the interpreter should compute hashes only when + strictly required. + + *) + module Hash : sig + type t + + (** This function will more likely be of type [Bytes.t -> t]. *) + val hash : 'a -> t + + (** [combine hs] returns a hash for hash list [hs]. *) + val combine : t list -> t + + (** The size in bytes of the serialization of an hash. *) + val size : int + + val to_string : t -> string + end = struct + type t = Digest.t + + let hash x = Digest.bytes (Marshal.to_bytes x []) + + let to_string x = String.sub (Digest.to_hex x) 0 8 + + let rec combine = function + | [] -> assert false + | [h] -> h + | h :: hs -> hash (h, combine hs) + + let size = 16 + end + + (** + + We need a notion of [Taint] to mark specific parts of values to + understand if they have been useful for a given execution step. + + *) + module Taint : sig + type t + + val transparent : t + + val of_tick : Tick_repr.t -> t + + val fresh : unit -> t + + val to_string : t -> string + end = struct + type t = int + + let transparent = -1 + + let fresh = + let r = ref (-1) in + fun () -> + decr r ; + !r + + let of_tick (t : Tick_repr.t) = (t :> int) + + let to_string = string_of_int + end + + (** + + The following type constructor is used at each level of the + values manipulated by the merkelizing interpreter. + + Hopefully, the introduction of such a type constructor will be + the major change in the existing Michelson interpreter. + + Indeed, to recover the standard Michelson interpreter, one can + simply use the type constructor ['a id = 'a] instead of ['a + merkelized]. + + *) + type 'a merkelized = { + value : 'a option; (** A merkelized value can be absent. *) + repr : 'a repr; (** A dynamic representation of ['a]'s type. *) + mutable hash : Hash.t option; + (** A value of type ['a merkelized] is actually "premerkelized" + as the hashes are only computed on demand by a (recursive) + modification of the [hash] field. *) + mutable mark : Taint.t; + (** A [mark] represents a taintstamp with respect to the + execution witnessing that the value has been observed at some + point of the execution. + + We must maintain the invariant that the mark of subvalues are + older than [mark]. *) + size : int; + (** + + We need to maintain the size of merkelized values because we + must be able to transmit them in a layer-1 operation (which + has a limited size). + + What we call "size" in this context is not the size of the + complete merkelized value but simply the size of the serialization + of the toplevel structure of the merkelized value. + + Typically, for an inhabitant of an algebraic data type, + this size is typically the size of the data constructor plus + the size of the hashes of its components. + + In the real implementation, we will probably need to transmit + serialized values instead of hashes for small values. + + *) + } + + and 'a v = 'a merkelized + + and ('a, 's) cell = 'a v * 's v + + and ('s, 'f) cont = + | KHalt : ('f, 'f) cont + | KCons : ('s, 't) instr v * ('t, 'f) cont v -> ('s, 'f) cont + + (** + + A small subset of Michelson. + + *) + and ('s, 'u) instr = + | Halt : ('f, 'f) instr + | Push : 'a v * (('a, 's) cell, 'f) instr v -> ('s, 'f) instr + | Succ : ((int, 's) cell, 'u) instr v -> ((int, 's) cell, 'u) instr + | Mul : + ((int, 's) cell, 'f) instr v + -> ((int, (int, 's) cell) cell, 'f) instr + | Dec : ((int, 's) cell, 'f) instr v -> ((int, 's) cell, 'f) instr + | CmpNZ : ((bool, 's) cell, 'f) instr v -> ((int, 's) cell, 'f) instr + | Loop : + ('s, (bool, 's) cell) instr v * ('s, 'f) instr v + -> ((bool, 's) cell, 'f) instr + | Dup : (('a, ('a, 's) cell) cell, 'f) instr v -> (('a, 's) cell, 'f) instr + | Swap : + (('b, ('a, 's) cell) cell, 'f) instr v + -> (('a, ('b, 's) cell) cell, 'f) instr + | Drop : ('s, 'f) instr v -> (('a, 's) cell, 'f) instr + | Dip : + ('s, 't) instr v * (('a, 't) cell, 'f) instr v + -> (('a, 's) cell, 'f) instr + + and _ repr = + | Int : int repr + | Bool : bool repr + | Unit : unit repr + | Cell : 'a repr * 'b repr -> ('a, 'b) cell repr + | Instr : 'i repr * 'o repr -> ('i, 'o) instr repr + | Cont : 'a repr * 'b repr -> ('a, 'b) cont repr + + (** To simplify testing, we assume that a program has no argument + and always produces an integer. *) + type program = (unit, (int, unit) cell) instr v + + let hash_of v = Option.value ~default:(Hash.hash "Empty_hash") v.hash + + let rec pp_of_repr : type a. Format.formatter -> a repr -> unit = + fun ppf repr -> + match repr with + | Cell (ity, oty) -> + Format.fprintf ppf "(%a, %a)" pp_of_repr ity pp_of_repr oty + | Cont (ity, oty) -> + Format.fprintf ppf "(%a ~> %a)" pp_of_repr ity pp_of_repr oty + | Instr _ -> Format.pp_print_string ppf "instr" + | Int -> Format.pp_print_string ppf "int" + | Bool -> Format.pp_print_string ppf "bool" + | Unit -> Format.pp_print_string ppf "unit" + + let rec pp_of_value : type a. Format.formatter -> a repr -> a -> unit = + fun ppf repr x -> + match repr with + | Cell (_ity, _oty) -> + Format.fprintf ppf "(%a, %a)" show (fst x) show (snd x) + | Cont _ -> pp_of_cont ppf x + | Instr _ -> pp_of_instr ppf x + | Int -> Format.pp_print_int ppf x + | Bool -> Format.pp_print_bool ppf x + | Unit -> Format.pp_print_string ppf "()" + + and pp_of_instr : type a s. Format.formatter -> (a, s) instr -> unit = + fun ppf instr -> + match instr with + | Halt -> Format.pp_print_string ppf "halt" + | Push (x, i) -> Format.fprintf ppf "push %a ; %a" show x show i + | Succ i -> Format.fprintf ppf "succ ; %a" show i + | Mul i -> Format.fprintf ppf "mul ; %a" show i + | Dec i -> Format.fprintf ppf "dec ; %a" show i + | CmpNZ i -> Format.fprintf ppf "cmpnz ; %a" show i + | Loop (body, the_exit) -> + Format.fprintf ppf "loop { %a } ; %a" show body show the_exit + | Dup i -> Format.fprintf ppf "dup ; %a" show i + | Swap i -> Format.fprintf ppf "swap ; %a" show i + | Drop i -> Format.fprintf ppf "drop ; %a" show i + | Dip (body, and_then) -> + Format.fprintf ppf "dip { %a } ; %a" show body show and_then + + and pp_of_cont : type s f. Format.formatter -> (s, f) cont -> unit = + fun ppf s -> + match s with + | KHalt -> Format.pp_print_string ppf "khalt" + | KCons (i, k) -> Format.fprintf ppf "%a : %a" show i show k + + and verbose = false + + and show : type a. Format.formatter -> a v -> unit = + fun ppf v -> + if verbose then + Format.fprintf + ppf + "([%s | %s ]%a : %a)" + (Taint.to_string v.mark) + (Option.fold ~none:"?" ~some:Hash.to_string v.hash) + (Format.pp_print_option + ~none:(fun ppf _ -> Format.pp_print_string ppf "") + (fun ppf x -> pp_of_value ppf v.repr x)) + v.value + pp_of_repr + v.repr + else + Format.fprintf + ppf + "([%a]%a)" + (Format.pp_print_option + ~none:(fun ppf _ -> Format.pp_print_string ppf "?") + (fun ppf x -> Format.pp_print_string ppf (Hash.to_string x))) + v.hash + (Format.pp_print_option + ~none:(fun ppf _ -> Format.pp_print_string ppf "") + (fun ppf x -> pp_of_value ppf v.repr x)) + v.value + + let get ~taint left_space v = + if taint <> Taint.transparent then v.mark <- taint ; + left_space := !left_space - v.size ; + if !left_space < 0 then + raise (Invalid_argument "This operation consumes too much space") ; + option_get v.value + + let merke ~taint repr value size = + {hash = None; value = Some value; repr; size; mark = taint} + + let push ~taint x i = + match i.repr with + | Instr (Cell (_, s), f) -> + merke ~taint (Instr (s, f)) (Push (x, i)) (24 + (2 * Hash.size)) + + let halt ~taint f = merke ~taint (Instr (f, f)) Halt (8 + Hash.size) + + let succ ~taint i = merke ~taint i.repr (Succ i) (24 + Hash.size) + + let mul ~taint i = + match i.repr with + | Instr (s, f) -> + merke ~taint (Instr (Cell (Int, s), f)) (Mul i) (24 + Hash.size) + + let dec ~taint i = merke ~taint i.repr (Dec i) (24 + i.size) + + let cmpnz ~taint i = + match i.repr with + | Instr (Cell (_, s), f) -> + merke ~taint (Instr (Cell (Int, s), f)) (CmpNZ i) (24 + Hash.size) + + let dup ~taint i = + match i.repr with + | Instr (Cell (_, Cell (a, s)), f) -> + merke ~taint (Instr (Cell (a, s), f)) (Dup i) (24 + Hash.size) + + let swap ~taint i = + match i.repr with + | Instr (Cell (b, Cell (a, s)), f) -> + merke ~taint (Instr (Cell (a, Cell (b, s)), f)) (Swap i) (24 + Hash.size) + + let drop ~taint ty i = + match i.repr with + | Instr (s, f) -> + merke ~taint (Instr (Cell (ty, s), f)) (Drop i) (24 + Hash.size) + + let loop ~taint body the_exit = + match (body.repr, the_exit.repr) with + | (Instr (_, i), Instr (_, f)) -> + merke + ~taint + (Instr (i, f)) + (Loop (body, the_exit)) + (24 + (2 * Hash.size)) + + let dip ~taint body and_then = + match (and_then.repr, body.repr) with + | (Instr (Cell (a, _), f), Instr (s', _)) -> + merke + ~taint + (Instr (Cell (a, s'), f)) + (Dip (body, and_then)) + (24 + (2 * Hash.size)) + + let lint ~taint x = merke ~taint Int x 8 + + let lbool ~taint x = merke ~taint Bool x 8 + + let khalt ~taint f = merke ~taint (Cont (f, f)) KHalt 8 + + let kcons ~taint (type s t f) (i : (s, t) instr v) (cont : (t, f) cont v) : + (s, f) cont v = + match i.repr with + | Instr (ity, _) -> ( + match cont.repr with + | Cont (_, oty) -> + merke + ~taint + (Cont (ity, oty)) + (KCons (i, cont)) + (i.size + cont.size + 24)) + + let cell ~taint x v = + merke ~taint (Cell (x.repr, v.repr)) (x, v) (x.size + v.size + 24) + + let empty_stack ~taint = merke ~taint Unit () 8 + + (** [merkelize v] computes the hashes in [v]. *) + let rec merkelize : type a. a v -> unit = + let open Hash in + fun v -> + match v.hash with + | Some _ -> () + | None -> + let hash = + match (v.repr, v.value) with + | (Cell _, Some x) -> + let (a, b) = x in + merkelize a ; + merkelize b ; + assert (v.hash = None) ; + (* No recursive values allowed. *) + combine [hash_of a; hash_of b] + | (Instr _, Some i) -> hash_instr i + | (Cont _, Some k) -> hash_cont k + | (Int, Some i) -> hash i + | (Bool, Some i) -> hash i + | (Unit, Some ()) -> hash () + | (_, None) -> assert false + in + v.hash <- Some hash + + and hash_cont : type s f. (s, f) cont -> Hash.t = function + | KHalt -> Hash.hash "KHalt" + | KCons (i, cont) -> + merkelize i ; + merkelize cont ; + Hash.(combine [hash "KCons"; hash_of i; hash_of cont]) + + and hash_instr : type s f. (s, f) instr -> Hash.t = function + | Halt -> Hash.hash ["Halt"] + | Push (x, i) -> + merkelize x ; + merkelize i ; + Hash.(combine [hash "Push"; hash_of x; hash_of i]) + | Succ i -> + merkelize i ; + Hash.(combine [hash "Succ"; hash_of i]) + | Mul i -> + merkelize i ; + Hash.(combine [hash "Mul"; hash_of i]) + | Dec i -> + merkelize i ; + Hash.(combine [hash "Dec"; hash_of i]) + | CmpNZ i -> + merkelize i ; + Hash.(combine [hash "CmpNZ"; hash_of i]) + | Loop (body, the_exit) -> + merkelize body ; + merkelize the_exit ; + Hash.(combine [hash "Loop"; hash_of body; hash_of the_exit]) + | Dup i -> + merkelize i ; + Hash.(combine [hash "Dup"; hash_of i]) + | Swap i -> + merkelize i ; + Hash.(combine [hash "Swap"; hash_of i]) + | Drop i -> + merkelize i ; + Hash.(combine [hash "Drop"; hash_of i]) + | Dip (body, and_then) -> + merkelize body ; + merkelize and_then ; + Hash.(combine [hash "Dip"; hash_of body; hash_of and_then]) + + (** [useful_part ~taint v] returns the (toplevel) parts of [v] + that have been marked with [taint]. + + We assume that the root of [v] has been marked with [taint]. + Otherwise, the result is undefined. + *) + let useful_part ~taint v = + let rec aux : type a. a v -> a v = + fun v -> + if v.mark <> taint then {v with value = None} + else + match (v.repr, v.value) with + | (Cell _, Some x) -> {v with value = Some (aux (fst x), aux (snd x))} + | (Cont _, Some (KCons (i, k))) -> + {v with value = Some (KCons (aux i, aux k))} + | (Cont _, Some KHalt) -> v + | (Instr _, Some i) -> + let value = + match i with + | Push (x, i) -> Push (aux x, aux i) + | Halt -> Halt + | Succ i -> Succ (aux i) + | Mul i -> Mul (aux i) + | Dec i -> Dec (aux i) + | CmpNZ i -> CmpNZ (aux i) + | Loop (body, the_exit) -> Loop (aux body, aux the_exit) + | Dup i -> Dup (aux i) + | Swap i -> Swap (aux i) + | Drop i -> Drop (aux i) + | Dip (body, and_then) -> Dip (aux body, aux and_then) + in + {v with value = Some value} + | (Int, _) -> v + | (Bool, _) -> v + | (Unit, _) -> v + | (_, None) -> v + in + aux v +end + +module MakeMPVM (Code : sig + val program : MerkelizedMichelson.program +end) = +struct + open MerkelizedMichelson + + (** + + The state of the Merkelized interpreter for Michelson is + made of merkelized pair of a stack of type ['s] and a + continuation expecting a stack of this type. + + ['f] represents the type of the final stack. + + Both ['s] and ['f] are existentially quantified but can + be recovered thanks to their dynamic representation held + by the [repr] field of the merkelized value. + + *) + type _ state = State : ('s, ('s, 'f) cont) cell v -> _ state + + let pp ppf (State cell) = show ppf cell + + let merkelize_state (State s) = + merkelize s ; + State s + + (** This function "compresses" the state representation by dropping the + value. This should reduce the size of the serialization. However, if + the value is shorter than the hash, we should probably keep the value + and recompute the hash on the other side of the pipe. *) + let compress (State s) = State {s with value = None} + + module Internal_for_tests = struct + let initial_state = + let taint = Taint.transparent in + let stack = empty_stack ~taint in + let cont = kcons ~taint Code.program (khalt ~taint (Cell (Int, Unit))) in + merkelize_state (State (cell ~taint stack cont)) + + let equal_state : _ state -> _ state -> bool = + fun (State s1) (State s2) -> + match (s1.hash, s2.hash) with + | (Some h1, Some h2) -> h1 = h2 + | (_, _) -> assert false + + let random_state _ _ = + let taint = Taint.transparent in + let s = cell ~taint (empty_stack ~taint) (khalt ~taint Unit) in + compress (merkelize_state (State s)) + end + + (** The encoding is not really the main point here, I made arathe silly one (that only produces the initial state) + to move forward. *) + let encoding : _ state Data_encoding.t = + Data_encoding.conv + (fun x -> match x with State _ -> 3) + (fun _ -> compress Internal_for_tests.initial_state) + Data_encoding.int16 + + let random_state _ _ = + let taint = Taint.transparent in + let s = cell ~taint (empty_stack ~taint) (khalt ~taint Unit) in + compress (merkelize_state (State s)) + + (** + + [step_instr ~taint i k stack] implements a single execution step. + + This interpreter is close the current Michelson interpreter + except on the following points: + + - There is no recursive call to immediately evaluate the next + instruction. + + - Values are deconstructed through [get] which taints them to + determine their useful parts. As said earlier, replacing + [get] with the identity should recover the current Michelson + interpreter. + + - This interpreter checks that the useful part of the state + remains compatible with the size limit of its serialization. + + *) + let step_instr : + type s t f. + taint:Taint.t -> + int ref -> + (s, t) instr v -> + (t, f) cont v -> + s v -> + [`Compressed | `Verifiable | `Full] state = + fun ~taint left_space i cont s -> + let return s = State s in + match get ~taint left_space i with + | Halt -> return (cell ~taint s cont) + | Push (x, i) -> + return (cell ~taint (cell ~taint x s) (kcons ~taint i cont)) + | Succ i -> ( + match get ~taint left_space s with + | (x, s) -> + let x = get ~taint left_space x in + return + (cell + ~taint + (cell ~taint (lint ~taint (x + 1)) s) + (kcons ~taint i cont))) + | Mul i -> ( + match get ~taint left_space s with + | (x, s) -> ( + match get ~taint left_space s with + | (y, s) -> + let x = get ~taint left_space x in + let y = get ~taint left_space y in + return + (cell + ~taint + (cell ~taint (lint ~taint (x * y)) s) + (kcons ~taint i cont)))) + | Dec i -> ( + match get ~taint left_space s with + | (x, s) -> + let x = get ~taint left_space x in + return + (cell + ~taint + (cell ~taint (lint ~taint (x - 1)) s) + (kcons ~taint i cont))) + | CmpNZ i -> ( + match get ~taint left_space s with + | (x, s) -> + let x = get ~taint left_space x in + return + (cell + ~taint + (cell ~taint (lbool ~taint (x <> 0)) s) + (kcons ~taint i cont))) + | Loop (body, the_exit) -> ( + match get ~taint left_space s with + | (b, s) -> + if get ~taint left_space b then + return (cell ~taint s (kcons ~taint body (kcons ~taint i cont))) + else return (cell ~taint s (kcons ~taint the_exit cont))) + | Dup i -> ( + match get ~taint left_space s with + | (x, _) -> return (cell ~taint (cell ~taint x s) (kcons ~taint i cont)) + ) + | Swap i -> ( + match get ~taint left_space s with + | (x, s) -> ( + match get ~taint left_space s with + | (y, s) -> + return + (cell + ~taint + (cell ~taint y (cell ~taint x s)) + (kcons ~taint i cont)))) + | Drop i -> ( + match get ~taint left_space s with + | (_, s) -> return (cell ~taint s (kcons ~taint i cont))) + | Dip (body, and_then) -> ( + match get ~taint left_space s with + | (x, s) -> + let cont = + kcons ~taint body (kcons ~taint (push ~taint x and_then) cont) + in + return (cell ~taint s cont)) + + let step_cont : + type s f. + taint:Taint.t -> + int ref -> + (s, f) cont v -> + s v -> + [`Compressed | `Verifiable | `Full] state = + fun ~taint left_space cont s -> + match get ~taint left_space cont with + | KHalt -> State (cell ~taint s cont) + | KCons (i, cont) -> step_instr ~taint left_space i cont s + + (** + + The history contains at most K snapshots of the state + where K is the number of section in the previous dissection. + + Hence, if the initial section of the game has N ticks, at + the step I, we have (N / K^I) execution steps to replay. + This looks reasonable. + + *) + + type history = [`Compressed | `Verifiable | `Full] state Tick_repr.Map.t + + let empty_history : history = Tick_repr.Map.empty + + let remember history (tick : Tick_repr.t) state = + Tick_repr.Map.add tick state history + + type tick = Tick_repr.t + + let forward_eval history tick = + match Tick_repr.Map.split tick history with + | (lower, None, _) -> Tick_repr.Map.max_binding lower + | (_, Some state, _) -> Some (tick, state) + + let eval_to : + taint:Taint.t -> + history -> + tick -> + [`Compressed | `Verifiable | `Full] state = + fun ~taint history target_tick -> + let (tick0, state0) = + Option.value ~default:(Tick_repr.make 0, Internal_for_tests.initial_state) + @@ forward_eval history target_tick + in + let rec go tick state = + if tick = target_tick then state + else + let (State s) = state in + let left_space = ref (16 * 1024) in + let (v, cont) = get ~taint left_space s in + let state' = step_cont ~taint left_space cont v in + go (Tick_repr.next tick) state' + in + go tick0 state0 + + let state_at : history -> tick -> [`Compressed | `Verifiable | `Full] state = + fun history tick -> + let taint = Taint.of_tick tick in + merkelize_state @@ eval_to ~taint history tick + + let verifiable_state_at : + history -> tick -> [`Compressed | `Verifiable | `Full] state = + fun history tick -> + let (State s0) = state_at history tick in + let taint = Taint.of_tick tick in + let left_space = ref (16 * 1024) in + let (v, cont) = get ~taint left_space s0 in + let _ = step_cont ~taint left_space cont v in + State (useful_part ~taint s0) + + let eval : + failures:tick list -> tick -> ([> `Verifiable] as 'a) state -> 'a state = + fun ~failures tick (State s) -> + if List.mem ~equal:Tick_repr.( = ) tick failures then + (* In this case, a failure is a stuttering. *) + State s + else + let taint = Taint.of_tick tick in + let left_space = ref (16 * 1024) in + let (v, cont) = get ~taint left_space s in + merkelize_state (step_cont ~taint left_space cont v) + + let rec execute_until : + failures:tick list -> + tick -> + ([> `Verifiable] as 'a) state -> + (tick -> 'a state -> bool) -> + tick * 'a state = + fun ~failures tick state pred -> + if pred tick state then (tick, merkelize_state state) + else + let state = eval ~failures tick state in + execute_until ~failures (Tick_repr.next tick) state pred +end + +module Push = struct + open MerkelizedMichelson + + let program = + let taint = Taint.transparent in + push ~taint (lint ~taint 1) (halt ~taint (Cell (Int, Unit))) +end + +module Fact20 = struct + open MerkelizedMichelson + + let program : program = + let taint = Taint.transparent in + + push ~taint (lint ~taint 20) + @@ push ~taint (lint ~taint 1) + @@ dup ~taint @@ cmpnz ~taint + @@ dip ~taint (swap ~taint (halt ~taint (Cell (Int, Cell (Int, Unit))))) + @@ loop + ~taint + (dup ~taint + @@ dip + ~taint + (swap ~taint (halt ~taint (Cell (Int, Cell (Int, Unit))))) + @@ mul ~taint @@ swap ~taint @@ dec ~taint @@ dup ~taint + @@ cmpnz + ~taint + (halt ~taint (Cell (Bool, Cell (Int, Cell (Int, Unit)))))) + @@ drop ~taint Int (halt ~taint (Cell (Int, Unit))) +end + +(** This module introduces some testing strategies for a game created from a PVM +*) +module Strategies (P : Sc_rollup_repr.TPVM) = struct + module Game = Game_repr.Make (P) + open Game + open PVM + + (** this eception is needed for a small that alows a "fold-with break" +*) + exception + Section of [`Compressed | `Verifiable | `Full] Game.Section_repr.section + + let random_tick ?(from = 0) () = Tick_repr.make (from + Random.int 31) + + (** this picks a random section between start_at and stop_at. The states + are determined by the random_state function.*) + let random_section (start_at : Tick_repr.t) start_state + (stop_at : Tick_repr.t) = + let x = min 10000 (abs (Tick_repr.distance start_at stop_at)) in + let length = 1 + try Random.int x with _ -> 0 in + let stop_at = (start_at :> int) + length in + + ({ + section_start_at = start_at; + section_start_state = start_state; + section_stop_at = Tick_repr.make stop_at; + section_stop_state = Internal_for_tests.random_state length start_state; + } + : _ Section_repr.section) + + (** this picks a random dissection of a given section. + The sections involved are random and their states have no connection with the initial section.*) + let random_dissection + (gsection : [`Compressed | `Verifiable | `Full] Section_repr.section) = + let open Tick_repr in + let rec aux dissection start_at start_state = + if start_at = gsection.section_stop_at then dissection + else + let section = + random_section start_at start_state gsection.section_stop_at + in + if + section.section_start_at = gsection.section_start_at + && section.section_stop_at = gsection.section_stop_at + then aux dissection start_at start_state + else + aux + (Map.add section.section_start_at section dissection) + section.section_stop_at + section.section_stop_state + in + if distance gsection.section_stop_at gsection.section_start_at > 1 then + Some + (aux Map.empty gsection.section_start_at gsection.section_start_state) + else None + + (** this function assmbles a random decision from a given dissection. + It first picks a random section from the dissection and modifies randomly its states. + If the length of this section is one tick the returns a conclusion with the given modified states. + If the length is longer it creates a random decision and outputs a Refine decisoon with this dissection.*) + let random_decision d = + let open Section_repr in + let open Tick_repr.Map in + let cardinal = cardinal d in + let x = Random.int cardinal in + (* Section_repr.pp_of_dissection Format.std_formatter d; *) + let (_, section) = + try + fold + (fun _ s (n, _) -> if n = x then raise (Section s) else (n + 1, None)) + d + (0, None) + with Section sec -> (0, Some sec) + in + let section = + match section with None -> raise Not_found | Some section -> section + in + let section_start_at = section.section_start_at in + let section_stop_at = section.section_stop_at in + let section_start_state = + Internal_for_tests.random_state 0 section.section_start_state + in + let section_stop_state = + Internal_for_tests.random_state + ((section_stop_at :> int) - (section_start_at :> int)) + section.section_start_state + in + + let next_dissection = random_dissection section in + let section = + { + section_start_state; + section_start_at; + section_stop_state; + section_stop_at; + } + in + let conflict_search_step = + match next_dissection with + | None -> + Conclude + { + start_state = section.section_start_state; + stop_state = section.section_stop_state; + } + | Some next_dissection -> + Refine {stop_state = section.section_stop_state; next_dissection} + in + ConflictInside {choice = section; conflict_search_step} + + (** technical params for machine directed strategies, branching is the number of pieces for a dissection +failing level*) + type parameters = { + branching : int; + failing_level : int; + max_failure : int option; + } + + type checkpoint = Tick_repr.t -> bool + + (** there are two kinds of strategies, random and machine dirrected by a params and a checkpoint*) + type strategy = Random | MachineDirected of parameters * checkpoint + + (**checks that the stop state of a section conflicts with the one in the history.*) + let conflicting_section (history : PVM.history) + (section : _ Section_repr.section) = + not + (Internal_for_tests.equal_state + section.section_stop_state + (state_at history section.section_stop_at)) + + (** updates the history*) + let remember_section history + (section : [`Compressed | `Verifiable | `Full] Section_repr.section) = + let history = + PVM.remember history section.section_start_at section.section_start_state + in + PVM.remember history section.section_stop_at section.section_stop_state + + (** Finds the section (if it exists) is a dissection that conflicts with the history. + This is where the trick with the exception appears*) + let find_conflict history dissection = + try + Tick_repr.Map.fold + (fun _ v _ -> + if conflicting_section history v then raise (Section v) else None) + dissection + None + with Section section -> Some section + + (** [next_move history branching dissection] + If finds the next move based on a dissection and history. + It finds the first section of dissection that conflicts with the history. + If the section has length one tick it returns a move with a Conclude conflict_search_step. + If the section is longer it creates a new dissection with branching many pieces, updates the history based on + this dissection and returns a move with a Refine type conflict_search_step. + *) + let next_move history branching dissection = + let section = + find_conflict history dissection |> function + | None -> raise (TickNotFound (Tick_repr.make 0)) + | Some s -> s + in + let next_dissection = + Section_repr.dissection_of_section history branching section + in + let (conflict_search_step, history) = + match next_dissection with + | None -> + let stop_state = + state_at history (Tick_repr.next section.section_start_at) + in + ( Conclude + { + start_state = + PVM.(verifiable_state_at history section.section_start_at); + stop_state; + }, + empty_history ) + | Some next_dissection -> + let stop_state = state_at history section.section_stop_at in + let history = + Tick_repr.Map.fold + (fun _ v acc -> remember_section acc v) + next_dissection + empty_history + in + (Refine {stop_state; next_dissection}, history) + in + (ConflictInside {choice = section; conflict_search_step}, history) + + (** helper function that generates an array of failing_level many ticks between start and stop*) + let generate_failures failing_level (section_start_at : Tick_repr.t) + (section_stop_at : Tick_repr.t) max_failure = + let d = Tick_repr.distance section_stop_at section_stop_at in + let d = match max_failure with None -> d | Some x -> x in + if failing_level > 0 then + let s = + repeat failing_level (fun _ -> + let s = (section_start_at :> int) + Random.int (max d 1) in + Tick_repr.make s) + in + Result.value ~default:[] s + else [] + + (** this is an outomatic commuter client. It generates a "perfect" client for the commuter unless +given some positive failing level when it "forgets" to evaluate the ticks on the autmatically generated failure list.*) + let machine_directed_committer {branching; failing_level; max_failure} pred = + let history = ref PVM.empty_history in + let initial ((section_start_at : Tick_repr.t), section_start_state) : commit + = + let section_stop_at = + Tick_repr.make ((section_start_at :> int) + Random.int 2) + in + let failures = + generate_failures + failing_level + section_start_at + section_stop_at + max_failure + in + let (section_stop_at, section_stop_state) = + PVM.execute_until ~failures section_start_at section_start_state + @@ fun tick _ -> pred tick + in + history := PVM.remember !history section_start_at section_start_state ; + history := PVM.remember !history section_stop_at section_stop_state ; + Commit + { + section_start_state; + section_start_at; + section_stop_state; + section_stop_at; + } + in + let next_move dissection = + let (move, history') = next_move !history branching dissection in + history := history' ; + move + in + + ({initial; next_move} : _ client) + + (** this is an outomatic refuter client. It generates a "perfect" client for the commuter unless +given some positive failing level when it "forgets" to evaluate the ticks on the autmatically generated failure list.*) + let machine_directed_refuter {branching; failing_level; max_failure} = + let history = ref PVM.empty_history in + let initial (section_start_state, Commit section) : refutation = + let ({section_start_at; section_stop_at; _} : _ Section_repr.section) = + section + in + let failures = + generate_failures + failing_level + section_start_at + section_stop_at + max_failure + in + let (_stop_at, section_stop_state) = + PVM.execute_until ~failures section_start_at section_start_state + @@ fun tick _ -> tick >= section_stop_at + in + history := PVM.remember !history section_start_at section_start_state ; + history := PVM.remember !history section_stop_at section_stop_state ; + let next_dissection = + Section_repr.dissection_of_section + !history + branching + {section with section_stop_state} + in + let conflict_search_step = + match next_dissection with + | None -> + Conclude + { + start_state = verifiable_state_at !history section_start_at; + stop_state = section_stop_state; + } + | Some next_dissection -> + Refine {stop_state = section_stop_state; next_dissection} + in + RefuteByConflict conflict_search_step + in + let next_move dissection = + let (move, history') = next_move !history branching dissection in + history := history' ; + move + in + ({initial; next_move} : _ client) + + (** This builds a commiter client from a strategy. + If the strategy is MachineDirected it uses the above constructions. + if the strategy is random then it usesa random section for the initial commitments + and the random decision for the next move.*) + let committer_from_strategy : strategy -> _ client = function + | Random -> + { + initial = + (fun ((section_start_at : Tick_repr.t), start_state) -> + let section_stop_at = + random_tick ~from:(section_start_at :> int) () + in + let section = + random_section section_start_at start_state section_stop_at + in + Commit section); + next_move = random_decision; + } + | MachineDirected (parameters, checkpoint) -> + machine_directed_committer parameters checkpoint + + (** This builds a refuter client from a strategy. + If the strategy is MachineDirected it uses the above constructions. + If the strategy is random then it uses a randomdissection + of the commited section for the initial refutation + and the random decision for the next move.*) + let refuter_from_strategy : strategy -> _ client = function + | Random -> + { + initial = + (fun ( (start_state : [`Compressed | `Verifiable | `Full] state), + Commit section ) -> + let conflict_search_step = + let next_dissection = random_dissection section in + match next_dissection with + | None -> + Conclude + { + start_state; + stop_state = + Internal_for_tests.random_state 1 start_state; + } + | Some next_dissection -> + let (_, section) = + Option.value + ~default:(Tick_repr.make 0, section) + (Tick_repr.Map.max_binding next_dissection) + in + Refine + {stop_state = section.section_stop_state; next_dissection} + in + RefuteByConflict conflict_search_step); + next_move = random_decision; + } + | MachineDirected (parameters, _) -> machine_directed_refuter parameters + + (** [test_strategies committer_strategy refuter_strategy expectation] + runs a game based oin the two given strategies and checks that the resulting + outcome fits the expectations. *) + let test_strategies committer_strategy refuter_strategy expectation = + let start_state = PVM.Internal_for_tests.initial_state in + let committer = committer_from_strategy committer_strategy in + let refuter = refuter_from_strategy refuter_strategy in + let outcome = + run ~start_at:(Tick_repr.make 0) ~start_state ~committer ~refuter + in + expectation outcome + + (** This is a commuter client having a perfect strategy*) + let perfect_committer = + MachineDirected + ( {failing_level = 0; branching = 2; max_failure = None}, + fun tick -> (tick :> int) >= 20 + Random.int 100 ) + (** This is a refuter client having a perfect strategy*) + + let perfect_refuter = + MachineDirected + ( {failing_level = 0; branching = 2; max_failure = None}, + fun _ -> assert false ) + + (** This is a commuter client having a strategy that forgets a tick*) + let failing_committer max_failure = + MachineDirected + ( {failing_level = 1; branching = 2; max_failure}, + fun tick -> + let s = match max_failure with None -> 20 | Some x -> x in + (tick :> int) >= s ) + + (** This is a commuter client having a strategy that forgets a tick*) + let failing_refuter max_failure = + MachineDirected + ({failing_level = 1; branching = 2; max_failure}, fun _ -> assert false) + + (** the possible expectation functions *) + let commiter_wins = function + | {winner = Some Committer; _} -> true + | _ -> false + + let refuter_wins = function {winner = Some Refuter; _} -> true | _ -> false + + let all_win (_ : outcome) = true +end + +(** the following are the possible combinations of strategies*) +let perfect_perfect (module P : Sc_rollup_repr.TPVM) _max_failure = + let module R = Strategies (P) in + R.test_strategies R.perfect_committer R.perfect_refuter R.commiter_wins + +let random_random (module P : Sc_rollup_repr.TPVM) _max_failure = + let module S = Strategies (P) in + S.test_strategies Random Random S.all_win + +let random_perfect (module P : Sc_rollup_repr.TPVM) _max_failure = + let module S = Strategies (P) in + S.test_strategies Random S.perfect_refuter S.refuter_wins + +let perfect_random (module P : Sc_rollup_repr.TPVM) _max_failure = + let module S = Strategies (P) in + S.test_strategies S.perfect_committer Random S.commiter_wins + +let failing_perfect (module P : Sc_rollup_repr.TPVM) max_failure = + let module S = Strategies (P) in + S.test_strategies + (S.failing_committer max_failure) + S.perfect_refuter + S.refuter_wins + +let perfect_failing (module P : Sc_rollup_repr.TPVM) max_failure = + let module S = Strategies (P) in + S.test_strategies + S.perfect_committer + (S.failing_refuter max_failure) + S.commiter_wins + +(** this assembles a test from a RandomPVM and a function that choses the type of strategies *) +let testing_randomPVM (f : (module Sc_rollup_repr.TPVM) -> int option -> bool) + name = + QCheck.Test.make + ~name + (QCheck.list_of_size QCheck.Gen.small_int (QCheck.int_range 0 100)) + (fun initial_prog -> + QCheck.assume (initial_prog <> []) ; + f + (module MakeRandomPVM (struct + let initial_prog = initial_prog + end)) + (Some (List.length initial_prog))) + +(** this assembles a test from a CountingPVM and a function that choses the type of strategies *) +let testing_countPVM (f : (module Sc_rollup_repr.TPVM) -> int option -> bool) + name = + QCheck.Test.make ~name QCheck.small_int (fun target -> + QCheck.assume (target > 0) ; + f + (module MakeCountingPVM (struct + let target = target + end)) + (Some target)) + +(** this assembles a test from a MichelsonPVM and a function that choses the type of strategies *) + +let testing_mich (f : (module Sc_rollup_repr.TPVM) -> int option -> bool) name = + QCheck.Test.make ~name QCheck.small_int (fun _ -> + f (module MakeMPVM (Fact20)) (Some 20)) + +let test_random_dissection (module P : Sc_rollup_repr.TPVM) start_at length + branching = + let open P in + let module S = Strategies (P) in + let state = Internal_for_tests.initial_state in + let stop_at = start_at + length in + + let section = + S.Game.Section_repr. + { + section_start_at = Tick_repr.make start_at; + section_start_state = state; + section_stop_at = Tick_repr.make stop_at; + section_stop_state = Internal_for_tests.random_state length state; + } + in + let option_dissection = + S.Game.Section_repr.dissection_of_section empty_history branching section + in + let dissection = + match option_dissection with + | None -> raise (Invalid_argument "no dissection") + | Some x -> x + in + S.Game.Section_repr.valid_dissection section dissection + +let testDissection = + [ + QCheck.Test.make + ~name:"randomVPN" + (QCheck.quad + (QCheck.list_of_size QCheck.Gen.small_int (QCheck.int_range 0 100)) + QCheck.small_int + QCheck.small_int + QCheck.small_int) + (fun (initial_prog, start_at, length, branching) -> + QCheck.assume + (start_at >= 0 && length > 1 + && List.length initial_prog > start_at + length + && 1 < branching) ; + let module P = MakeRandomPVM (struct + let initial_prog = initial_prog + end) in + test_random_dissection (module P) start_at length branching); + QCheck.Test.make + ~name:"count" + (QCheck.quad + QCheck.small_int + QCheck.small_int + QCheck.small_int + QCheck.small_int) + (fun (target, start_at, length, branching) -> + QCheck.assume (start_at >= 0 && length > 1 && 1 < branching) ; + let module P = MakeCountingPVM (struct + let target = target + end) in + test_random_dissection (module P) start_at length branching); + QCheck.Test.make + ~name:"Mich" + (QCheck.triple QCheck.small_int QCheck.small_int QCheck.small_int) + (fun (start_at, length, branching) -> + QCheck.assume (start_at >= 0 && length > 1 && 1 < branching) ; + let module P = MakeMPVM (Fact20) in + test_random_dissection (module P) start_at length branching); + ] + +let () = + Alcotest.run + "Refutation Game" + [ + ("Dissection tests", qcheck_wrap testDissection); + ( "RandomPVM", + qcheck_wrap + [ + testing_randomPVM perfect_perfect "perfect-perfect"; + testing_randomPVM random_random "random-random"; + testing_randomPVM random_perfect "random-perfect"; + testing_randomPVM perfect_random "perfect-random"; + testing_randomPVM failing_perfect "failing_perfect"; + testing_randomPVM perfect_failing "perfect-failing"; + ] ); + ( "CountingPVM", + qcheck_wrap + [ + testing_countPVM perfect_perfect "perfect-perfect"; + testing_countPVM random_random "random-random"; + testing_countPVM random_perfect "random-perfect"; + testing_countPVM perfect_random "perfect-random"; + testing_countPVM failing_perfect "failing_perfect"; + testing_countPVM perfect_failing "perfect-failing"; + ] ); + ( "Fact20PVM", + qcheck_wrap + [ + testing_mich perfect_perfect "perfect-perfect"; + testing_mich random_random "random-random"; + testing_mich random_perfect "random-perfect"; + testing_mich perfect_random "perfect-random"; + testing_mich failing_perfect "failing_perfect"; + testing_mich perfect_failing "perfect-failing"; + ] ); + ] + +(* +let test_machine (module M : PVM) = + let module PCG = MakeGame (M) in + let module S = Strategies (PCG) in + S.test () + + +let () = + test_machine + (module RandomPVM (struct + let initial_prog = + QCheck.Gen.generate1 + (QCheck.Gen.list_size + QCheck.Gen.small_int + (QCheck.Gen.int_range 0 100)) + end)) *) diff --git a/src/proto_alpha/lib_protocol/tick_repr.ml b/src/proto_alpha/lib_protocol/tick_repr.ml new file mode 100644 index 0000000000000000000000000000000000000000..da1a79ac7f7d0bc0cc26a0fd36952938198ada90 --- /dev/null +++ b/src/proto_alpha/lib_protocol/tick_repr.ml @@ -0,0 +1,43 @@ +(*****************************************************************************) +(* *) +(* 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. *) +(* *) +(*****************************************************************************) + +type t = int + +let encoding = Data_encoding.int16 + +let pp ppf tick = Format.fprintf ppf "%d" tick + +let make x = + assert (Compare.Int.(x >= 0)) ; + x + +let next = succ + +let distance tick1 tick2 = abs (tick1 - tick2) + +let ( = ) = Compare.Int.( = ) + +module Map = Map.Make (Compare.Int) diff --git a/src/proto_alpha/lib_protocol/tick_repr.mli b/src/proto_alpha/lib_protocol/tick_repr.mli new file mode 100644 index 0000000000000000000000000000000000000000..ec0a0e9388d04c09e6f23701959144b5872200d9 --- /dev/null +++ b/src/proto_alpha/lib_protocol/tick_repr.mli @@ -0,0 +1,49 @@ +(*****************************************************************************) +(* *) +(* 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, a representation of the rollup operations *) + +type t = private int + +val encoding : t Data_encoding.t + +val pp : Format.formatter -> t -> unit + +(** Creates a tick from an integer. + This function fails when the integer is negative *) +val make : int -> t + +(** the next tick +*) +val next : t -> t + +(** The absolute value of the ifference between two ticks*) +val distance : t -> t -> int + +(** Tick.t equality *) +val ( = ) : t -> t -> bool + +module Map : Map.S with type key = t diff --git a/tezos-sc-rollup-client-alpha b/tezos-sc-rollup-client-alpha new file mode 100755 index 0000000000000000000000000000000000000000..89e67129593f59c68bbc3d3a865cb0c14a016b2a Binary files /dev/null and b/tezos-sc-rollup-client-alpha differ diff --git a/tezt/_regressions/sc_rollup_node_configuration.out b/tezt/_regressions/sc_rollup_node_configuration.out index 2552370d372ce33ebb87bedce1e408328c76b3bc..16baefd7255655369e7545c397f61f643c98dbb9 100644 --- a/tezt/_regressions/sc_rollup_node_configuration.out +++ b/tezt/_regressions/sc_rollup_node_configuration.out @@ -1,2 +1,2 @@ tezt/_regressions/sc_rollup_node_configuration.out -{"sc-rollup-address":"scr1FMbLCKVD19Lx9WYqsiHfyt2VMne55espu","rpc-port":17384} +{"sc-rollup-address":"scr1TUxGx5BxBxw4xfGEMuGtD7D5fUp6RWeGx","rpc-port":17384} diff --git a/tezt/_regressions/sc_rollup_origination.out b/tezt/_regressions/sc_rollup_origination.out index f331e57cf65fd7dad2548b66cab910eb994a69d7..7a2b2946e31a552d322c70b60bcee911ce05503f 100644 --- a/tezt/_regressions/sc_rollup_origination.out +++ b/tezt/_regressions/sc_rollup_origination.out @@ -1,2 +1,2 @@ tezt/_regressions/sc_rollup_origination.out -scr1FMbLCKVD19Lx9WYqsiHfyt2VMne55espu +scr1TUxGx5BxBxw4xfGEMuGtD7D5fUp6RWeGx