diff --git a/manifest/main.ml b/manifest/main.ml index e19d40ecb193592e7d35e4c7524f4fe2facd31a0..a38f70621f62e5c0f5b2e8d417c9cd6906fc39e9 100644 --- a/manifest/main.ml +++ b/manifest/main.ml @@ -3211,7 +3211,7 @@ end = struct type t = {main : target; embedded : target} let make_tests ?test_helpers ?parameters ?plugin ?client ?benchmark - ?benchmark_type_inference ~main ~name () = + ?benchmark_type_inference ?sc_rollup ~main ~name () = let name_dash = Name.name_dash name in let number = Name.number name in let path = Name.base_path name in @@ -3369,6 +3369,7 @@ end = struct octez_benchmark; benchmark |> if_some |> open_; benchmark_type_inference |> if_some |> open_; + sc_rollup |> if_some |> if_ N.(number >= 015) |> open_; ] in let _unit = @@ -4623,6 +4624,7 @@ module Protocol = Protocol ?client ?benchmark:(Option.bind benchmark Fun.id) ?benchmark_type_inference + ?sc_rollup ~main ~name () diff --git a/opam/tezos-protocol-alpha-tests.opam b/opam/tezos-protocol-alpha-tests.opam index d31e14fc17963c1c9c629c57bb9aa4e3ed68bb50..23930c85fbb2aaf45df8369b2b8edd27b608d18a 100644 --- a/opam/tezos-protocol-alpha-tests.opam +++ b/opam/tezos-protocol-alpha-tests.opam @@ -25,6 +25,7 @@ depends: [ "tezos-context" {with-test} "tezos-test-helpers" {with-test} "alcotest" { with-test & >= "1.5.0" } + "tezos-sc-rollup-alpha" {with-test} "tezos-client-base" {with-test} "tezos-protocol-environment" {with-test} "tezos-stdlib-unix" {with-test} diff --git a/src/lib_test/qcheck2_helpers.ml b/src/lib_test/qcheck2_helpers.ml index d78ca281a5e4d4cc6dbdab05027da7d83dad3a69..37b222bdd7d604c8e8174bef487bbbfd80fe1336 100644 --- a/src/lib_test/qcheck2_helpers.ml +++ b/src/lib_test/qcheck2_helpers.ml @@ -44,6 +44,10 @@ let qcheck_make_result ?count ?print ?pp_error ?check ~name in QCheck2.Test.make ~name ?print ?count gen (fun x -> f x |> check) +let qcheck_make_lwt ?count ?print ~extract ~name ~(gen : 'a QCheck2.Gen.t) + (f : 'a -> bool Lwt.t) = + QCheck2.Test.make ~name ?print ?count gen (fun x -> extract (f x)) + let qcheck_eq ?pp ?cmp ?eq expected actual = let pass = match (eq, cmp) with diff --git a/src/lib_test/qcheck2_helpers.mli b/src/lib_test/qcheck2_helpers.mli index 05f411e6c8a71bd9caa81b32ccfdb45ab8e3e5bd..353ff36fad73fbe00c0a7af58a0a5b61fc263a28 100644 --- a/src/lib_test/qcheck2_helpers.mli +++ b/src/lib_test/qcheck2_helpers.mli @@ -46,6 +46,19 @@ val qcheck_make_result : ('a -> (bool, 'b) result) -> QCheck2.Test.t +(** [qcheck_make_lwt ?print ?count ~extract ~name ~gen f] is a wrapper + around {!QCheck2.Test.make} where [f] returns a [bool Lwt.t]. + [extract] needs to be provided to extract the [bool] from [Lwt], e.g. + [Lwt_main.run]. *) +val qcheck_make_lwt : + ?count:int -> + ?print:'a QCheck2.Print.t -> + extract:(bool Lwt.t -> bool) -> + name:string -> + gen:'a QCheck2.Gen.t -> + ('a -> bool Lwt.t) -> + QCheck2.Test.t + (** [qcheck_eq_tests ~eq ~gen ~eq_name] returns three tests of [eq]: reflexivity, symmetry, and transitivity. diff --git a/src/proto_alpha/bin_sc_rollup_node/refutation_game.ml b/src/proto_alpha/bin_sc_rollup_node/refutation_game.ml index a837a2186b561f84caf03d740cd8a67a6888db64..45b4c1d7a070059d9569bb196021b6cb0f313c70 100644 --- a/src/proto_alpha/bin_sc_rollup_node/refutation_game.ml +++ b/src/proto_alpha/bin_sc_rollup_node/refutation_game.ml @@ -136,48 +136,24 @@ module Make (PVM : Pvm.S) : S with module PVM = PVM = struct r let new_dissection node_ctxt store last_level ok our_view = - let open Lwt_result_syntax in + let state_hash_from_tick tick = + let open Lwt_result_syntax in + let* r = Interpreter.state_of_tick node_ctxt store tick last_level in + return (Option.map snd r) + in let start_hash, start_tick = ok in - let our_state, stop_tick = our_view in + let start_chunk = {state_hash = Some start_hash; tick = start_tick} in + let start_hash, start_tick = our_view in + let our_stop_chunk = {state_hash = start_hash; tick = start_tick} in let Node_context.{protocol_constants; _} = node_ctxt in - let max_number_of_sections = - Z.of_int - protocol_constants.parametric.sc_rollup.number_of_sections_in_dissection - in - let trace_length = Z.succ (Sc_rollup.Tick.distance stop_tick start_tick) in - let number_of_sections = Z.min max_number_of_sections trace_length in - let rem = Z.(rem trace_length number_of_sections) in - let first_section_length, section_length = - if Z.Compare.(trace_length < max_number_of_sections) then - (* In this case, every section is of length one. *) - Z.(one, one) - else - let section_length = - Z.(max one (div trace_length number_of_sections)) - in - if Z.Compare.(section_length = Z.one) && not Z.Compare.(rem = Z.zero) - then - (* If we put [section_length] in this situation, we will most likely - have a very long last section. *) - (rem, section_length) - else (section_length, section_length) - in - (* [k] is the number of sections in [rev_dissection]. *) - let rec make rev_dissection k tick = - if Z.(equal k (pred number_of_sections)) then - return - @@ List.rev - ({state_hash = our_state; tick = stop_tick} :: rev_dissection) - else - let* r = Interpreter.state_of_tick node_ctxt store tick last_level in - let state_hash = Option.map snd r in - let next_tick = Sc_rollup.Tick.jump tick section_length in - make ({state_hash; tick} :: rev_dissection) (Z.succ k) next_tick + let default_number_of_sections = + protocol_constants.parametric.sc_rollup.number_of_sections_in_dissection in - make - [{state_hash = Some start_hash; tick = start_tick}] - Z.one - (Sc_rollup.Tick.jump start_tick first_section_length) + Game_helpers.new_dissection + ~start_chunk + ~our_stop_chunk + ~default_number_of_sections + ~state_hash_from_tick (** [generate_from_dissection node_ctxt store game] traverses the current [game.dissection] and returns a move which diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index 4491ff61a680d166e044a26abd5ba18ba44d4413..3150f31907004f5c72161159dab6810939e5e7f1 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -3339,6 +3339,8 @@ module Sc_rollup : sig type dissection_chunk = {state_hash : State_hash.t option; tick : Tick.t} + val pp_dissection_chunk : Format.formatter -> dissection_chunk -> unit + type t = { turn : player; inbox_snapshot : Inbox.history_proof; @@ -3348,6 +3350,8 @@ module Sc_rollup : sig default_number_of_sections : int; } + val pp_dissection : Format.formatter -> dissection_chunk list -> unit + val pp : Format.formatter -> t -> unit module Index : sig @@ -3371,7 +3375,7 @@ module Sc_rollup : sig val pp_refutation : Format.formatter -> refutation -> unit type invalid_move = - | Dissection_choice_not_found of Sc_rollup_tick_repr.t + | Dissection_choice_not_found of Tick.t | Dissection_number_of_sections_mismatch of {expected : Z.t; given : Z.t} | Dissection_invalid_number_of_sections of Z.t | Dissection_start_hash_mismatch of { @@ -3380,15 +3384,15 @@ module Sc_rollup : sig } | Dissection_stop_hash_mismatch of State_hash.t option | Dissection_edge_ticks_mismatch of { - dissection_start_tick : Sc_rollup_tick_repr.t; - dissection_stop_tick : Sc_rollup_tick_repr.t; - chunk_start_tick : Sc_rollup_tick_repr.t; - chunk_stop_tick : Sc_rollup_tick_repr.t; + dissection_start_tick : Tick.t; + dissection_stop_tick : Tick.t; + chunk_start_tick : Tick.t; + chunk_stop_tick : Tick.t; } | Dissection_ticks_not_increasing | Dissection_invalid_distribution | Dissection_invalid_successive_states_shape - | Proof_unpexpected_section_size of Z.t + | Proof_unexpected_section_size of Z.t | Proof_start_state_hash_mismatch of { start_state_hash : State_hash.t option; start_proof : State_hash.t; @@ -3399,6 +3403,8 @@ module Sc_rollup : sig } | Proof_invalid of string + val pp_invalid_move : Format.formatter -> invalid_move -> unit + type reason = Conflict_resolved | Invalid_move of invalid_move | Timeout val pp_reason : Format.formatter -> reason -> unit diff --git a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml index 8c079025826c971cef779d13369c94571653ef75..dcaca8ad3e5a841ee56b681f8f5082db0db162a7 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml @@ -28,12 +28,26 @@ open Sc_rollup_repr type player = Alice | Bob -type dissection_chunk = { - state_hash : State_hash.t option; - tick : Sc_rollup_tick_repr.t; -} - module V1 = struct + type dissection_chunk = { + state_hash : State_hash.t option; + tick : Sc_rollup_tick_repr.t; + } + + let pp_state_hash = + let open Format in + pp_print_option ~none:(fun ppf () -> fprintf ppf "None") State_hash.pp + + let pp_dissection_chunk ppf {state_hash; tick} = + let open Format in + fprintf + ppf + "State hash:%a@ Tick: %a" + pp_state_hash + state_hash + Sc_rollup_tick_repr.pp + tick + type t = { turn : player; inbox_snapshot : Sc_rollup_inbox_repr.history_proof; @@ -157,11 +171,11 @@ module V1 = struct (fun ppf {state_hash; tick} -> Format.fprintf ppf - " %a @ %a" - (Format.pp_print_option State_hash.pp) - state_hash + "%a: %a" Sc_rollup_tick_repr.pp - tick) + tick + pp_state_hash + state_hash) ppf d @@ -361,7 +375,7 @@ type invalid_move = | Dissection_ticks_not_increasing | Dissection_invalid_distribution | Dissection_invalid_successive_states_shape - | Proof_unpexpected_section_size of Z.t + | Proof_unexpected_section_size of Z.t | Proof_start_state_hash_mismatch of { start_state_hash : State_hash.t option; start_proof : State_hash.t; @@ -441,7 +455,7 @@ let pp_invalid_move fmt = fmt "Maximum tick increment in a section cannot be more than half total \ dissection length" - | Proof_unpexpected_section_size n -> + | Proof_unexpected_section_size n -> Format.fprintf fmt "dist should be equal to 1 in a proof, but got %a" @@ -575,14 +589,13 @@ let invalid_move_encoding = | Dissection_invalid_successive_states_shape -> Some () | _ -> None) (fun () -> Dissection_invalid_successive_states_shape); case - ~title:"sc_rollup_proof_unpexpected_section_size" + ~title:"sc_rollup_proof_unexpected_section_size" (Tag 9) (obj2 - (req "kind" (constant "proof_unpexpected_section_size")) + (req "kind" (constant "proof_unexpected_section_size")) (req "value" n)) - (function - | Proof_unpexpected_section_size n -> Some ((), n) | _ -> None) - (fun ((), n) -> Proof_unpexpected_section_size n); + (function Proof_unexpected_section_size n -> Some ((), n) | _ -> None) + (fun ((), n) -> Proof_unexpected_section_size n); case ~title:"sc_rollup_proof_start_state_hash_mismatch" (Tag 10) @@ -798,7 +811,7 @@ let check_dissection ~default_number_of_sections ~start_chunk ~stop_chunk let check_proof_start_stop ~start_chunk ~stop_chunk proof = let open Lwt_result_syntax in let dist = Sc_rollup_tick_repr.distance start_chunk.tick stop_chunk.tick in - let* () = check Z.(equal dist one) (Proof_unpexpected_section_size dist) in + let* () = check Z.(equal dist one) (Proof_unexpected_section_size dist) in let start_proof = Sc_rollup_proof_repr.start proof in let stop_proof = Sc_rollup_proof_repr.stop proof in let* () = diff --git a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli index 0f21b768222c86fb3caa368fdce469295926de4e..e661acdab27ba6b3207749287bb6491ddfdd4fcc 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli @@ -129,14 +129,16 @@ open Sc_rollup_repr represent the first and second player in the pair respectively. *) type player = Alice | Bob -(** A dissection chunk is made of a state hash (that could be [None], see +module V1 : sig + (** A dissection chunk is made of a state hash (that could be [None], see invariants below), and a tick count. *) -type dissection_chunk = { - state_hash : State_hash.t option; - tick : Sc_rollup_tick_repr.t; -} + type dissection_chunk = { + state_hash : State_hash.t option; + tick : Sc_rollup_tick_repr.t; + } + + val pp_dissection_chunk : Format.formatter -> dissection_chunk -> unit -module V1 : sig (** A game state is characterized by: - [turn], the player that must provide the next move. @@ -202,7 +204,10 @@ end (** Versioning, see {!Sc_rollup_data_version_sig.S} for more information. *) include Sc_rollup_data_version_sig.S with type t = V1.t -include module type of V1 with type t = V1.t +include + module type of V1 + with type dissection_chunk = V1.dissection_chunk + and type t = V1.t module Index : sig type t = private {alice : Staker.t; bob : Staker.t} @@ -312,7 +317,7 @@ type invalid_move = | Dissection_invalid_successive_states_shape (** A dissection cannot have a section with no state hash after another section with some state hash. *) - | Proof_unpexpected_section_size of Z.t + | Proof_unexpected_section_size of Z.t (** Invalid proof step because there is more than one tick. *) | Proof_start_state_hash_mismatch of { start_state_hash : State_hash.t option; diff --git a/src/proto_alpha/lib_protocol/test/pbt/dune b/src/proto_alpha/lib_protocol/test/pbt/dune index 8a661a531a3b96691bdd2b43d0f2273992c3452c..e8b9f5aa221c591ef52cda47f89768e1cb068b60 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/dune +++ b/src/proto_alpha/lib_protocol/test/pbt/dune @@ -27,7 +27,8 @@ qcheck-alcotest tezos-benchmark tezos-benchmark-alpha - tezos-benchmark-type-inference-alpha) + tezos-benchmark-type-inference-alpha + tezos-sc-rollup-alpha) (flags (:standard) -open Tezos_base.TzPervasives @@ -37,7 +38,8 @@ -open Tezos_protocol_alpha -open Tezos_alpha_test_helpers -open Tezos_benchmark_alpha - -open Tezos_benchmark_type_inference_alpha)) + -open Tezos_benchmark_type_inference_alpha + -open Tezos_sc_rollup_alpha)) (rule (alias runtest) diff --git a/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml index 73cd8732acd829e3eee1bd67ba6551bab49e8e3b..c17037904cdb6fb1391d1a79cd2da34521b323f1 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml @@ -35,66 +35,171 @@ open Protocol open Alpha_context open Sc_rollup -open Lwt_syntax open Lib_test.Qcheck2_helpers -(** +(** {2 Utils} *) - Helpers +let qcheck_make_lwt = + Lib_test.Qcheck2_helpers.qcheck_make_lwt ~extract:Lwt_main.run -*) - -let hash_state state number = - Digest.bytes @@ Bytes.of_string @@ state ^ string_of_int number - -type dummy_proof = { - start : State_hash.t; - stop : State_hash.t option; - valid : bool; -} +let tick_to_int_exn ?(__LOC__ = __LOC__) t = + WithExceptions.Option.get ~loc:__LOC__ (Tick.to_int t) -module Tick_map = Map.Make (Sc_rollup_tick_repr) +let tick_of_int_exn ?(__LOC__ = __LOC__) n = + WithExceptions.Option.get ~loc:__LOC__ (Tick.of_int n) -let dummy_proof_encoding : dummy_proof Data_encoding.t = - let open Data_encoding in - conv - (fun {start; stop; valid} -> (start, stop, valid)) - (fun (start, stop, valid) -> {start; stop; valid}) - (obj3 - (req "start" State_hash.encoding) - (req "stop" (option State_hash.encoding)) - (req "valid" bool)) +let list_assoc ?(__LOC__ = __LOC__) key list = + match List.assoc ~equal:( = ) key list with + | Some value -> value + | None -> + QCheck2.Test.fail_reportf "list_assoc failed when called at %s" __LOC__ -let proof_start_state proof = proof.start +let print_dissection_chunk = Format.asprintf "%a" Game.pp_dissection_chunk -let proof_stop_state proof = proof.stop +let print_dissection = Format.asprintf "%a" Game.pp_dissection -let number_of_ticks_exn n = - match Number_of_ticks.of_int32 n with - | Some x -> x - | None -> Stdlib.failwith "Bad Number_of_ticks" - -let get_comm pred inbox_level ticks state = - Commitment. - { - predecessor = pred; - inbox_level = Raw_level.of_int32_exn inbox_level; - number_of_ticks = number_of_ticks_exn ticks; - compressed_state = state; - } +let print_our_states _ = "" +let expect_invalid_move expected = function + | Error (Game.Invalid_move reason) -> + if reason = expected then true + else + let pp = Game.pp_invalid_move in + QCheck2.Test.fail_reportf + "@[Expected reason: %a@;Actual reason: %a@]" + pp + expected + pp + reason + | _ -> false + +let initial_of_dissection dissection = + List.hd dissection |> WithExceptions.Option.get ~loc:__LOC__ + +(** Modify the last section of a dissection. *) +let rec modify_stop f dissection = + match dissection with + | [] -> assert false + | [chunk] -> [f chunk] + | x :: xs -> + let xs = modify_stop f xs in + x :: xs + +(** Modify the first section of a dissection. *) +let modify_start f dissection = + match dissection with + | chunk :: xs -> f chunk :: xs + | [] -> (* The dissection can not be empty. *) assert false + +(** Checks that the [dissection] is valid regarding the function + {!Sc_rollup_game_repr.check_dissection}. *) +let valid_dissection ~default_number_of_sections ~start_chunk ~stop_chunk + dissection = + let open Lwt_syntax in + let* res = + Game.Internal_for_tests.check_dissection + ~default_number_of_sections + ~start_chunk + ~stop_chunk + dissection + in + return (Result.is_ok res) + +(** [disputed_sections ~our_states dissection] returns the list of sections + in the [dissection] on which the player dissecting disagree with. + It uses [our_states], an assoc list between tick and state hashes to + compare opponent's claims against our point of view. *) +let disputed_sections ~our_states dissection = + let open Game in + let agree_on_state start_tick their_state = + let idx = tick_to_int_exn start_tick in + let our_state = list_assoc ~__LOC__ idx our_states in + Option.equal State_hash.equal our_state their_state + in + let rec traverse acc = function + | ({state_hash = their_start_state; tick = start_tick} as a) + :: ({state_hash = their_stop_state; tick = stop_tick} as b) + :: dissection -> + let rst = b :: dissection in + if agree_on_state start_tick their_start_state then + (* It's a disputed section if we agree on the start state but disagree + on the stop. *) + if agree_on_state stop_tick their_stop_state then traverse acc rst + else + let disputed_section = (a, b) in + traverse (disputed_section :: acc) rst + else traverse acc rst + | _ -> acc + in + traverse [] dissection + +let pick_disputed_sections disputed_sections = + QCheck2.Gen.oneofl disputed_sections + +let final_dissection ~our_states dissection = + let disputed_sections = disputed_sections ~our_states dissection in + let single_disputed_sections = + List.filter_map + (fun disputed_section -> + let Game.({tick = a_tick; _}, {tick = b_tick; _}) = disputed_section in + let distance = Tick.distance a_tick b_tick in + if Z.Compare.(distance = Z.one) then Some disputed_section else None) + disputed_sections + in + Compare.List_length_with.(single_disputed_sections > 0) + +(** Build a non-random dissection from [start_chunk] to [stop_chunk] using + [our_states] as the state hashes for each tick. *) +let build_dissection ~number_of_sections ~start_chunk ~stop_chunk ~our_states = + let open Lwt_result_syntax in + let state_hash_from_tick tick = + return @@ list_assoc ~__LOC__ (tick_to_int_exn tick) our_states + in + let our_stop_chunk = + Game. + { + stop_chunk with + state_hash = + list_assoc ~__LOC__ (tick_to_int_exn stop_chunk.tick) our_states; + } + in + (* TODO: https://gitlab.com/tezos/tezos/-/issues/3491 + + This dissection's building does not check the number of sections. Checks should + be added to verify that we don't generate invalid dissection and test the + incorrect cases. *) + Lwt_main.run + @@ let*! r = + Game_helpers.new_dissection + ~start_chunk + ~our_stop_chunk + ~default_number_of_sections:number_of_sections + ~state_hash_from_tick + in + Lwt.return @@ WithExceptions.Result.get_ok ~loc:__LOC__ r + +(** {2 Context free generators} *) + +(** Generate a {!State_hash.t}. + + We use a dirty hack {!QCheck2.Gen.make_primitive} to remove the + automatic shrinking. Shrinking on the states in a dissection can + be confusing, it can leads to a shrunk list with the same states in + each cell. +*) let gen_random_hash = let open QCheck2.Gen in - let* x = bytes_fixed_gen 32 in - return @@ State_hash.of_bytes_exn x - -let tick_of_int_exn n = - match Tick.of_int n with None -> assert false | Some t -> t - -let tick_to_int_exn t = - match Tick.to_int t with None -> assert false | Some n -> n + let gen = + let* x = bytes_fixed_gen 32 in + return @@ State_hash.of_bytes_exn x + in + (* This is not beautiful, but there is currently no other way to + remove the shrinker. *) + make_primitive + ~gen:(fun rand -> generate1 ~rand gen) + ~shrink:(fun _ -> Seq.empty) -(* Default number of sections in a dissection *) +(** Generate the number of sections in the dissection. *) let gen_num_sections = let open Tezos_protocol_alpha_parameters.Default_parameters in let testnet = constants_test.sc_rollup.number_of_sections_in_dissection in @@ -102,1059 +207,468 @@ let gen_num_sections = let sandbox = constants_sandbox.sc_rollup.number_of_sections_in_dissection in QCheck2.Gen.( frequency - [ - (5, pure mainnet); - (4, pure testnet); - (2, pure sandbox); - (1, int_range 4 100); - ]) - -let mk_dissection_chunk (state_hash, tick) = Game.{state_hash; tick} + [(5, pure mainnet); (4, pure testnet); (2, pure sandbox); (1, 4 -- 100)]) -let random_dissection ~default_number_of_sections start_at start_hash stop_at - stop_hash = +(** Generate a tick. *) +let gen_tick ?(lower_bound = 0) ?(upper_bound = 10_000) () = let open QCheck2.Gen in - let start_int = tick_to_int_exn start_at in - let stop_int = tick_to_int_exn stop_at in - let dist = stop_int - start_int in - let branch = min (dist + 1) default_number_of_sections in - let size = (dist + 1) / (branch - 1) in - - if dist = 1 then return None - else - let* random_hash = gen_random_hash in - return - @@ Result.to_option - (List.init branch ~when_negative_length:"error" (fun i -> - mk_dissection_chunk - @@ - if i = 0 then (Some start_hash, start_at) - else if i = branch - 1 then (stop_hash, stop_at) - else (Some random_hash, tick_of_int_exn (start_int + (i * size))))) - -(** - `genlist` is a `correct list` generator. It generates a list of strings that - are either integers or `+` to be consumed by the arithmetic PVM. - If a `+` is found then the previous two element of the stack are poped - then added and the result is pushed to the stack. - In particular, lists like `[1 +]` are incorrect. - - To preserve the correctness invariant, genlist is a recursive generator that - produce a pair `(stack_size, state_list)` where state_list is a correct list - of integers and `+` and consuming it will produce a `stack` of length - `stack_size`. - For example a result can be `(3, [1; 2; +; 3; +; 2; 2; +; 1;]). - Consuming the list will produce the stack`[6; 4; 2]` which has length 3. - The generator has two branches. - 1. with frequency 1 adds integers to state_list and increases the - corresponding stack_size. - 2. With frequency 2, at each step, it looks at the inductive result - `(self (n - 1))=(stack_size, state_list)`. - If the stack_size is smaller than 2 then it adds an integer to the state_list - and increases the stack_size - Otherwise it adds a plus to the state_list and decreases the stack_size. - Remark: The algorithm is linear in the size of the generated list and - generates all kinds of inputs not only those that produce a stack of size 1. -*) -let gen_list ~size = - QCheck2.Gen.( - map (fun (_, l) -> List.rev l) - @@ sized_size size - @@ fix (fun self n -> - match n with - | 0 -> map (fun x -> (1, [string_of_int x])) small_nat - | n -> - frequency - [ - ( 2, - map2 - (fun x (stack_size, state_list) -> - if stack_size >= 2 then - (stack_size - 1, "+" :: state_list) - else (stack_size + 1, string_of_int x :: state_list)) - small_nat - (self (n - 1)) ); - ( 1, - map2 - (fun x (i, y) -> (i + 1, string_of_int x :: y)) - small_nat - (self (n - 1)) ); - ])) - -(** This uses the above generator to produce a correct program with at - least 3 elements. *) - -let correct_program = - let open QCheck2.Gen in - gen_list ~size:(3 -- 1000) - -module type TestPVM = sig - include PVM.S with type hash = State_hash.t - - module Utils : sig - (** This a post-boot state. It is used as default in many functions. *) - val default_state : state - - (*TODO: These are not used in the current state. They are, however to be - used in the incoming more sophisticated set of tests from Thomas Athorne - *) - - (** [random_state n state] generates a random state. The integer n is - used as a seed in the generation. *) - val random_state : int -> state -> state QCheck2.Gen.t - - (** [make_proof start_state stop_state] produces a proof that the eval of - [start_state] is the [stop_state]. - It will be used by the `verify_proof`. In the arithPVM we use - `produce_tree_proof` which only requires a starting state (tree) - and the transition function. *) - val make_proof : state -> hash option -> proof Lwt.t - - (** Like [make_proof] but produces an invalid proof starting from - any hash. *) - val make_invalid_proof : hash -> hash option -> proof Lwt.t - end -end - -(** - - [MakeCountingPVM (P)] is a PVM whose state is an integer and that - can count up to a certain [P.target]. - - This PVM has no input states. - -*) -module MakeCountingPVM (P : sig - val target : int -end) : TestPVM with type state = int = struct - let name = "countingPVM" - - let parse_boot_sector x = Some x - - let pp_boot_sector fmt x = Format.fprintf fmt "%s" x - - type state = int - - let pp x = Lwt.return @@ fun fmt _ -> Format.pp_print_int fmt x - - type hash = State_hash.t - - type context = unit - - type proof = dummy_proof - - let proof_start_state = proof_start_state - - let proof_stop_state = proof_stop_state - - let proof_input_given _ = None - - let proof_input_requested _ = No_input_required - - let state_hash_ (x : state) = - State_hash.context_hash_to_state_hash - @@ Context_hash.hash_string [Int.to_string x] - - let state_hash (x : state) = return (state_hash_ x) - - let is_input_state x = - if x >= P.target then return Initial else return No_input_required - - let initial_state _ = return 0 - - let install_boot_sector _ _ = return P.target - - let set_input _ s = return s - - module Utils = struct - let default_state = P.target - - let random_state _ _ = QCheck2.Gen.int - - let make_proof s1 s2 = - let* s1 = state_hash s1 in - return {start = s1; stop = s2; valid = true} - - let make_invalid_proof s1 s2 = return {start = s1; stop = s2; valid = false} - end - - let proof_encoding = dummy_proof_encoding - - let eval state = if state >= P.target then return state else return (state + 1) - - let verify_proof proof = return proof.valid - - let produce_proof _ _ _ = Stdlib.failwith "Dummy PVM can't produce proof" - - let verify_origination_proof proof _ = return proof.valid - - let produce_origination_proof _ _ = - Stdlib.failwith "Dummy PVM can't produce proof" - - type output_proof = unit - - let output_proof_encoding = Data_encoding.unit - - let state_of_output_proof _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - let output_of_output_proof _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - let verify_output_proof _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - let produce_output_proof _ _ _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - module Internal_for_tests = struct - let insert_failure _ = Stdlib.failwith "Dummy PVM does not insert failures" - end -end - -(** This is a random PVM. Its state is a pair of a string and a - list of integers. An evaluation step consumes the next integer - of the list and concatenates its representation to the string. *) -module MakeRandomPVM (P : sig - val initial_prog : int list -end) : TestPVM with type state = string * int list = struct - let name = "randomPVM" - - let parse_boot_sector x = Some x - - let pp_boot_sector fmt x = Format.fprintf fmt "%s" x - - type state = string * int list - - let pp (s, xs) = - Lwt.return @@ fun fmt _ -> - Format.fprintf - fmt - "%s / %s" - s - (String.concat ":" @@ List.map string_of_int xs) - - type context = unit - - type proof = dummy_proof - - type hash = State_hash.t - - let to_string (a, b) = - Format.sprintf "(%s, [%s])" a (String.concat ";" @@ List.map Int.to_string b) - - let proof_start_state = proof_start_state - - let proof_stop_state = proof_stop_state - - let proof_input_given _ = None - - let proof_input_requested _ = No_input_required - - let state_hash_ x = - State_hash.context_hash_to_state_hash - @@ Context_hash.hash_string [to_string x] - - let state_hash (x : state) = return @@ state_hash_ x - - let initial_state _ = return ("", []) - - let install_boot_sector _ _ = return ("hello", P.initial_prog) - - let is_input_state (_, c) = - match c with [] -> return Initial | _ -> return No_input_required - - let set_input _ state = return state - - module Utils = struct - let default_state = ("hello", P.initial_prog) - - let random_state length ((_, program) : state) = - let open QCheck2.Gen in - let remaining_program = TzList.drop_n length program in - let+ stop_state = int in - (hash_state "" stop_state, remaining_program) - - let make_proof s1 s2 = - let* s1 = state_hash s1 in - return {start = s1; stop = s2; valid = true} - - let make_invalid_proof s1 s2 = return {start = s1; stop = s2; valid = false} - end - - let proof_encoding = dummy_proof_encoding - - let eval (hash, continuation) = - match continuation with - | [] -> return (hash, continuation) - | h :: tl -> return (hash_state hash h, tl) - - let verify_proof proof = return proof.valid - - let produce_proof _ _ _ = Stdlib.failwith "Dummy PVM can't produce proof" - - let verify_origination_proof proof _ = return proof.valid - - let produce_origination_proof _ _ = - Stdlib.failwith "Dummy PVM can't produce proof" - - type output_proof = unit - - let output_proof_encoding = Data_encoding.unit - - let state_of_output_proof _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - let output_of_output_proof _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - let verify_output_proof _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - let produce_output_proof _ _ _ = - Stdlib.failwith "Dummy PVM can't handle output proof" - - module Internal_for_tests = struct - let insert_failure _ = Stdlib.failwith "Dummy PVM does not insert failures" - end -end - -module ContextPVM = ArithPVM.Make (struct - open Tezos_context_memory.Context - - module Tree = struct - include Tezos_context_memory.Context.Tree - - type tree = Tezos_context_memory.Context.tree - - type t = Tezos_context_memory.Context.t - - type key = string list - - type value = bytes - end - - type tree = Tree.tree - - let hash_tree tree = - Sc_rollup.State_hash.context_hash_to_state_hash (Tree.hash tree) - - type proof = Proof.tree Proof.t - - let verify_proof proof f = - Lwt.map Result.to_option (verify_tree_proof proof f) - - let produce_proof context state f = - let* proof = - produce_tree_proof (index context) (`Value (Tree.hash state)) f - in - return (Some proof) - - let kinded_hash_to_state_hash = function - | `Value hash | `Node hash -> State_hash.context_hash_to_state_hash hash - - let proof_before proof = kinded_hash_to_state_hash proof.Proof.before - - let proof_after proof = kinded_hash_to_state_hash proof.Proof.after - - let proof_encoding = - let open Data_encoding in - conv (fun _ -> ()) (fun _ -> assert false) unit -end) - -module TestArith (P : sig - val inputs : string - - val evals : int -end) : TestPVM = struct - include ContextPVM - - let init_context = Tezos_context_memory.make_empty_context () - - module Utils = struct - let make_external_inbox_message str = - WithExceptions.Result.get_ok - ~loc:__LOC__ - Inbox.Message.(External str |> serialize) - - let default_state = - let promise = - let* boot = initial_state init_context in - let* boot = install_boot_sector boot "" in - let* boot = eval boot in - Format.printf "%s\n\n\n" P.inputs ; - let input = - { - inbox_level = Raw_level.root; - message_counter = Z.zero; - payload = make_external_inbox_message P.inputs; - } - in - let prelim = set_input input boot in - List.fold_left (fun acc _ -> acc >>= fun acc -> eval acc) prelim - @@ List.repeat P.evals () - in - Lwt_main.run promise - - let random_state i state = - let open QCheck2.Gen in - let+ program = correct_program in - let input = - { - inbox_level = Raw_level.root; - message_counter = Z.zero; - payload = make_external_inbox_message @@ String.concat " " program; - } + let+ tick = lower_bound -- upper_bound in + tick_of_int_exn ~__LOC__ tick + +(** Dissection helpers and tests *) +module Dissection = struct + (** Generate an initial *valid* dissection. The validity comes from a + mirrored implementation of {!Sc_rollup_game_repr.initial}. *) + let gen_initial_dissection ?ticks () = + let open QCheck2.Gen in + let* child_state = gen_random_hash and* parent_state = gen_random_hash in + let* ticks = + let+ ticks = + match ticks with + | None -> frequency [(1, pure 0); (9, 1 -- 1_000)] + | Some distance -> pure distance in - let prelim = set_input input state in - let open Lwt in - Lwt_main.run - @@ List.fold_left (fun acc _ -> acc >>= fun acc -> eval acc) prelim - @@ List.repeat (min i (List.length program - 2) + 1) () - - let make_proof s1 _s2 = - let* proof_opt = produce_proof init_context None s1 in - match proof_opt with Ok proof -> return proof | Error _ -> assert false - - let make_invalid_proof _ _ = - let* state = initial_state init_context in - let* state = install_boot_sector state "foooobaaar" in - let* proof_opt = produce_proof init_context None state in - match proof_opt with Ok proof -> return proof | Error _ -> assert false - end -end - -(** - This module introduces some testing strategies for a game created - from a PVM. -*) -module Strategies (PVM : TestPVM with type hash = State_hash.t) = struct - (** [exec_all state tick] runs eval until the state machine reaches a - state where it requires an input. It returns the new state and the - final tick. - *) - let exec_all state tick = - let rec loop state tick = - let* isinp = PVM.is_input_state state in - match isinp with - | No_input_required -> - let* s = PVM.eval state in - let* hash1 = PVM.state_hash state in - let* hash2 = PVM.state_hash s in - - if State_hash.equal hash1 hash2 then assert false - else loop s (Tick.next tick) - | _ -> return (state, tick) - in - loop state tick - - (** [state_at to_tick from_state from_tick] returns the state at tick - [to_tick], or [None] if that's past the point at which the machine - has stopped. *) - let state_at to_tick from_state from_tick = - let rec loop state tick = - let* isinp = PVM.is_input_state state in - if Tick.equal to_tick tick then return (Some state, tick) - else - match isinp with - | No_input_required -> - let* s = PVM.eval state in - let* hash1 = PVM.state_hash state in - let* hash2 = PVM.state_hash s in - - if State_hash.equal hash1 hash2 then assert false - else loop s (Tick.next tick) - | _ -> return (None, to_tick) + Z.of_int ticks in - loop from_state from_tick - - (** [dissection_of_section start_tick start_state stop_tick] creates - a dissection with at most {!default_number_of_sections} pieces - that are (roughly) equal - spaced and whose states are computed by running the eval function - until the correct tick. Note that the last piece can be as much - as {!default_number_of_sections} - 1 ticks longer than the others. *) - let dissection_of_section ~default_number_of_sections start_tick start_state - stop_tick = - let start_int = tick_to_int_exn start_tick in - let stop_int = tick_to_int_exn stop_tick in - let dist = stop_int - start_int in - if dist = 1 then return None + let* initial_tick = gen_tick () in + if Z.Compare.(ticks = Z.zero) then + pure + [ + Game.{state_hash = Some child_state; tick = initial_tick}; + Game.{state_hash = None; tick = Tick.next initial_tick}; + ] else - let branch = min (dist + 1) default_number_of_sections in - let size = (dist + 1) / (branch - 1) in - let tick_list = - Result.to_option - @@ List.init branch ~when_negative_length:"error" (fun i -> - if i = branch - 1 then stop_tick - else tick_of_int_exn (start_int + (i * size))) - in - let a = - Option.map - (fun a -> - List.map - (fun tick -> - let hash = - Lwt_main.run - @@ let* state, (_ : Tick.t) = - state_at tick start_state start_tick - in - match state with - | None -> return None - | Some s -> - let* h = PVM.state_hash s in - return (Some h) - in - mk_dissection_chunk (hash, tick)) - a) - tick_list - in - return a - - type client = { - initial : (Tick.t * PVM.hash) option Lwt.t; - gen_next_move : Game.t -> Game.refutation option Lwt.t QCheck2.Gen.t; - } - - type outcome_for_tests = Defender_wins | Refuter_wins - - let equal_outcome a b = - match (a, b) with - | Defender_wins, Defender_wins -> true - | Refuter_wins, Refuter_wins -> true - | _ -> false - - let loser_to_outcome_for_tests loser alice_is_refuter = - match loser with - | Game.Bob -> if alice_is_refuter then Refuter_wins else Defender_wins - | Game.Alice -> if alice_is_refuter then Defender_wins else Refuter_wins - - let run ~default_number_of_sections ~inbox ~refuter_client ~defender_client = - let refuter, (_ : public_key), (_ : Signature.secret_key) = - Signature.generate_key () - in - let defender, (_ : public_key), (_ : Signature.secret_key) = - Signature.generate_key () - in - let alice_is_refuter = Staker.(refuter < defender) in - let initial_game = - let* start_hash = PVM.state_hash PVM.Utils.default_state in - let* initial_data = defender_client.initial in - let tick, initial_hash = - match initial_data with None -> assert false | Some s -> s - in - let int_tick = tick_to_int_exn tick in - let number_of_ticks = Int32.of_int int_tick in - let parent = get_comm Commitment.Hash.zero 0l 1l start_hash in - let child = - get_comm Commitment.Hash.zero 0l number_of_ticks initial_hash - in - Lwt.return - @@ Game.initial - inbox - ~pvm_name:PVM.name - ~parent - ~child - ~refuter - ~defender - ~default_number_of_sections + let tick = Tick.jump initial_tick ticks in + pure + [ + Game.{state_hash = Some parent_state; tick = initial_tick}; + Game.{state_hash = Some child_state; tick}; + Game.{state_hash = None; tick = Tick.next tick}; + ] + + (** Generate a *valid* dissection. + It returns the dissection alongside the dissected start_chunk and + stop_chunk, but also the number of sections used to generate the + dissection. *) + let gen_dissection ~number_of_sections ~our_states dissection = + let open QCheck2.Gen in + let disputed_sections = disputed_sections ~our_states dissection in + assert (Compare.List_length_with.(disputed_sections > 0)) ; + let+ start_chunk, stop_chunk = pick_disputed_sections disputed_sections in + let dissection = + build_dissection ~number_of_sections ~start_chunk ~stop_chunk ~our_states in + (dissection, start_chunk, stop_chunk) - let outcome = - let rec loop game refuter_move = - let open QCheck2.Gen in - let* move = - if refuter_move then refuter_client.gen_next_move game - else defender_client.gen_next_move game - in - let move = Lwt_main.run move in - match move with - | None -> - return - @@ Lwt.return (if refuter_move then Defender_wins else Refuter_wins) - | Some move -> ( - let game_result = Lwt_main.run @@ Game.play game move in - match game_result with - | Either.Left outcome -> - return - @@ Lwt.return - (loser_to_outcome_for_tests outcome.loser alice_is_refuter) - | Either.Right game -> loop game (not refuter_move)) - in - loop (Lwt_main.run initial_game) true - in - outcome + let gen_initial_dissection_ticks = QCheck2.Gen.(0 -- 1_000) - let random_tick ?(from = 0) ~into () = - let open QCheck2.Gen in - let* x = from -- into in - return @@ Option.value ~default:Tick.initial (Tick.of_int x) + let gen_nonfinal_initial_dissection_ticks = QCheck2.Gen.(3 -- 1_000) - (** - checks that the stop state of a section conflicts with the one computed by the - evaluation. - *) - let conflicting_section tick state = - let* new_state, (_ : Tick.t) = - state_at tick PVM.Utils.default_state Tick.initial + (** Given an initial tick and state_hash: generates random state hashes for + every others [ticks]. + Having [our_states] provide the state hashes you believe to + be true. You can then generate a dissection from another one when + you disagree with some sections. *) + let gen_our_states dissection ticks = + let open QCheck2.Gen in + let Game.{tick = initial_tick; state_hash = initial_state_hash} = + initial_of_dissection dissection in - let* new_hash = - match new_state with - | None -> return None - | Some state -> - let* state = PVM.state_hash state in - return (Some state) + let initial_tick = tick_to_int_exn initial_tick in + let rec aux acc i = + if i < 0 then return acc + else if i = 0 then return ((initial_tick, initial_state_hash) :: acc) + else + let* state_hash = gen_random_hash in + aux ((i + initial_tick, Some state_hash) :: acc) (i - 1) in - - return @@ not (Option.equal ( = ) state new_hash) - - (** This function assembles 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 - decision with this dissection.*) - let random_decision ~default_number_of_sections d = - let open QCheck2.Gen in - let number_of_somes = - List.length - (List.filter (fun {Game.state_hash; _} -> Option.is_some state_hash) d) + aux [] ticks + + (** {3 Dissection tests} *) + + let count = 1_000 + + (** Test the validity of dissection generated by {!gen_dissection} on + an initial dissection generated by {!gen_initial_dissection}. + It is a self test that'll help detect issues in subsequent tests; + in case the generator does not produce valid dissections. *) + let test_valid_gen_dissection = + let open QCheck2 in + let gen = + let open Gen in + let* number_of_sections = gen_num_sections in + let* ticks = gen_initial_dissection_ticks in + let* dissection = gen_initial_dissection ~ticks () in + let* our_states = gen_our_states dissection (succ ticks) in + if final_dissection ~our_states dissection then + (* The initial dissection could not be dissected. *) + return (dissection, None, number_of_sections, our_states) + else + let* new_dissection, start_hash, stop_hash = + gen_dissection ~number_of_sections ~our_states dissection + in + return + ( dissection, + Some (new_dissection, start_hash, stop_hash), + number_of_sections, + our_states ) in - let* x = int_range 0 (number_of_somes - 1) in - let x = if x = number_of_somes - 1 then max 0 (x - 1) else x in - let start_hash, start = - match List.nth d x with - | Some Game.{state_hash = Some s; tick = t} -> (s, t) - | _ -> assert false + let print = + Print.( + quad + print_dissection + (option + (triple + print_dissection + print_dissection_chunk + print_dissection_chunk)) + int + print_our_states) in - let (_ : State_hash.t option), stop = - match List.nth d (x + 1) with - | Some Game.{state_hash; tick} -> (state_hash, tick) - | None -> assert false + qcheck_make_lwt + ~count + ~name:"gen_dissection produces a valid dissection" + ~print + ~gen + (fun (dissection, new_dissection, default_number_of_sections, our_states) + -> + let open Lwt_syntax in + match new_dissection with + | None -> return (final_dissection ~our_states dissection) + | Some (new_dissection, start_chunk, stop_chunk) -> + valid_dissection + ~default_number_of_sections + ~start_chunk + ~stop_chunk + new_dissection) + + (** Truncate a [dissection] and expect the + {!Sc_rollup_game_repr.check_dissection} to fail with an invalid + number of sections, where [expected_number_of_sections] is expected. *) + let truncate_and_check_error dissection start_chunk stop_chunk + default_number_of_sections expected_number_of_sections = + let open Lwt_syntax in + let truncated_dissection = + match dissection with + | x :: _ :: z :: rst -> x :: z :: rst + | _ -> + (* If the dissection is valid, this case can not be reached. *) + assert false in - let* stop_hash = gen_random_hash in - - let random_dissection = - random_dissection + let* res = + Game.Internal_for_tests.check_dissection ~default_number_of_sections - start - start_hash - stop - (Some stop_hash) - in - let* random_dissection = random_dissection and* hash = gen_random_hash in - - let game = - match random_dissection with - | None -> - let open Lwt.Syntax in - let* pvm_proof = - PVM.Utils.make_invalid_proof start_hash (Some hash) - in - let wrapped = - let module P = struct - include PVM - - let proof = pvm_proof - end in - Unencodable (module P) - in - let proof = Proof.{pvm_step = wrapped; inbox = None} in - Lwt.return (Some Game.{choice = start; step = Proof proof}) - | Some dissection -> - Lwt.return (Some Game.{choice = start; step = Dissection dissection}) + ~start_chunk + ~stop_chunk + truncated_dissection in - - return game - - (** There are two kinds of strategies, random and machine-directed. *) - type strategy = Random | MachineDirected - - (** - [find_conflict dissection] finds the section (if it exists) in a dissection that - conflicts with the actual computation. *) - let find_conflict dissection = - let rec aux states = - match states with - | start :: next :: rest -> - let Game.{state_hash = start_state; tick = start_tick} = start in - let Game.{state_hash = next_state; tick = next_tick} = next in - let* c0 = conflicting_section start_tick start_state in - let* c = conflicting_section next_tick next_state in - if c0 then assert false - else if c then - if next_state = None then return None - else - return (Some ((start_state, start_tick), (next_state, next_tick))) - else aux (next :: rest) - | _ -> return None + let expected_len = Z.of_int expected_number_of_sections in + let expected_reason = + Game.Dissection_number_of_sections_mismatch + {expected = expected_len; given = Z.pred expected_len} in - aux dissection - - (** [next_move branching dissection] finds the next move based on a - dissection. - It finds the first section of dissection that conflicts with the evaluation. - If the section has length one tick it returns a move with a Conclude - conflict_resolution_step. - If the section is longer it creates a new dissection with branching - many pieces and returns - a move with a Refine type conflict_resolution_step. - *) - let next_move ~default_number_of_sections dissection = - let* conflict = find_conflict dissection in - match conflict with - | Some ((_, start_tick), (_, next_tick)) -> - let* start_state, (_ : Tick.t) = - state_at start_tick PVM.Utils.default_state Tick.initial + return (expect_invalid_move expected_reason res) + + (** Test that if a dissection is smaller than the default number of + sections, the length is equal to (distance + 1) of the dissected + section. *) + let test_truncated_small_dissection = + let open QCheck2 in + qcheck_make_lwt + ~count + ~name: + "distance < nb_of_sections => (len dissection = succ (dist dissection))" + ~gen: + (let open Gen in + let* number_of_sections = gen_num_sections in + let* ticks = 3 -- (number_of_sections - 1) in + let* dissection = gen_initial_dissection ~ticks () in + let* our_states = gen_our_states dissection (succ ticks) in + let* new_dissection, start_hash, stop_hash = + gen_dissection ~number_of_sections ~our_states dissection in - let* next_dissection = - match start_state with - | None -> return None - | Some s -> - dissection_of_section - ~default_number_of_sections - start_tick - s - next_tick + return (new_dissection, start_hash, stop_hash, number_of_sections, ticks)) + (fun ( dissection, + start_chunk, + stop_chunk, + default_number_of_sections, + distance ) -> + let expected_len = succ distance in + truncate_and_check_error + dissection + start_chunk + stop_chunk + default_number_of_sections + expected_len) + + (** Test that if the distance in the dissected section is larger than + the default number of sections, the dissection length is exactly the + default number of sections. *) + let test_truncated_large_dissection = + let open QCheck2 in + qcheck_make_lwt + ~count + ~name:"distance >= nb_of_sections => (len dissection = nb_of_sections" + ~gen: + (let open Gen in + let* number_of_sections = gen_num_sections in + let* ticks = number_of_sections -- 1_000 in + let* dissection = gen_initial_dissection ~ticks () in + let* our_states = gen_our_states dissection (succ ticks) in + let* new_dissection, start_chunk, stop_chunk = + gen_dissection ~number_of_sections ~our_states dissection in - let* stop_state, (_ : Tick.t) = - match start_state with - | None -> return (None, next_tick) - | Some s -> state_at next_tick s start_tick - in - let* refutation = - match next_dissection with - | None -> - let* stop_hash = - match stop_state with - | None -> return None - | Some state -> - let* s = PVM.state_hash state in - return (Some s) - in - let* pvm_proof = - match start_state with - | Some s -> PVM.Utils.make_proof s stop_hash - | None -> assert false - in - let wrapped = - let module P = struct - include PVM - - let proof = pvm_proof - end in - Unencodable (module P) - in - let proof = Proof.{pvm_step = wrapped; inbox = None} in - return Game.{choice = start_tick; step = Proof proof} - | Some next_dissection -> - return - Game.{choice = start_tick; step = Dissection next_dissection} + return (new_dissection, start_chunk, stop_chunk, number_of_sections)) + (fun (dissection, start_chunk, stop_chunk, default_number_of_sections) -> + truncate_and_check_error + dissection + start_chunk + stop_chunk + default_number_of_sections + default_number_of_sections) + + (** Test that we can not change the start chunk of a section when we produce + a dissection. *) + let test_immutable_start_chunk = + let open QCheck2 in + qcheck_make_lwt + ~count + ~name:"dissection.start_chunk can not change" + ~gen: + (let open Gen in + let* number_of_sections = gen_num_sections in + let* ticks = gen_nonfinal_initial_dissection_ticks in + let* dissection = gen_initial_dissection ~ticks () in + let* our_states = gen_our_states dissection (succ ticks) in + let* new_dissection, start_chunk, stop_chunk = + gen_dissection ~number_of_sections ~our_states dissection in - - return (Some refutation) - | None -> return None - - (** This is an automatic client. It generates a "perfect" client. *) - let machine_directed = - let start_state = PVM.Utils.default_state in - let initial = - let* stop_state, stop_at = exec_all start_state Tick.initial in - let* stop_hash = PVM.state_hash stop_state in - return (Some (stop_at, stop_hash)) - in - - let gen_next_move (game : Game.t) = - let dissection = game.dissection in - let new_move = - let* mv = - next_move - ~default_number_of_sections:game.default_number_of_sections + let* new_state_hash = gen_random_hash in + return + ( new_dissection, + start_chunk, + stop_chunk, + number_of_sections, + new_state_hash )) + (fun ( dissection, + start_chunk, + stop_chunk, + default_number_of_sections, + new_state_hash ) -> + let open Lwt_syntax in + (* Check that we can not change the start hash. *) + let dissection_with_different_start = + modify_start + (fun chunk -> Game.{chunk with state_hash = Some new_state_hash}) dissection in - match mv with Some move -> return (Some move) | None -> return None - in - QCheck2.Gen.return new_move - in - - {initial; gen_next_move} - - (** This builds a client from a strategy. If the strategy is - MachineDirected it uses the above constructions. If the strategy - is random then it uses a random section for the initial - commitments and the random decision for the next move. *) - let player_from_strategy ~default_number_of_sections = function - | Random -> - let open QCheck2.Gen in - let* random_tick = - random_tick ~from:1 ~into:(default_number_of_sections - 1) () + let* res = + Game.Internal_for_tests.check_dissection + ~default_number_of_sections + ~start_chunk + ~stop_chunk + dissection_with_different_start in - let initial = - Lwt.Syntax.( - let random_state = PVM.Utils.default_state in - let* stop_hash = PVM.state_hash random_state in - Lwt.return (Some (random_tick, stop_hash))) + let expected_reason = + Game.Dissection_start_hash_mismatch + {expected = start_chunk.state_hash; given = Some new_state_hash} + in + return (expect_invalid_move expected_reason res)) + + (** Test that we can not produce a dissection that agrees with the stop hash. + Otherwise, there would be nothing to dispute. *) + let test_stop_hash_must_change = + let open QCheck2 in + qcheck_make_lwt + ~count + ~name:"dissection.stop_chunk must change" + ~gen: + (let open Gen in + let* number_of_sections = gen_num_sections in + let* ticks = gen_nonfinal_initial_dissection_ticks in + let* dissection = gen_initial_dissection ~ticks () in + let* our_states = gen_our_states dissection (succ ticks) in + let* new_dissection, start_chunk, stop_chunk = + gen_dissection ~number_of_sections ~our_states dissection + in + return (new_dissection, start_chunk, stop_chunk, number_of_sections)) + (fun (dissection, start_chunk, stop_chunk, default_number_of_sections) -> + let open Lwt_syntax in + let check_failure_on_same_stop_hash stop_hash = + let invalid_dissection = + modify_stop + (fun chunk -> Game.{chunk with state_hash = stop_hash}) + dissection + in + let stop_chunk = Game.{stop_chunk with state_hash = stop_hash} in + let* res = + Game.Internal_for_tests.check_dissection + ~default_number_of_sections + ~start_chunk + ~stop_chunk + invalid_dissection + in + let expected_reason = + Game.Dissection_stop_hash_mismatch stop_hash + (* match stop_hash with + * | None -> "The stop hash should not be None." + * | Some stop -> + * Format.asprintf + * "The stop hash should not be equal to %a" + * State_hash.pp + * stop *) + in + return (expect_invalid_move expected_reason res) + in + let* b1 = check_failure_on_same_stop_hash None in + let* b2 = check_failure_on_same_stop_hash stop_chunk.state_hash in + return (b1 && b2)) + + (** Test that we can not produce a dissection modifying the starting + end last point of a section. *) + let test_immutable_start_and_stop_ticks = + let open QCheck2 in + qcheck_make_lwt + ~count + ~name: + "start_chunk.tick and stop_chunk.tick can not change in the dissection" + ~gen: + (let open Gen in + let* number_of_sections = gen_num_sections in + let* ticks = gen_nonfinal_initial_dissection_ticks in + let* dissection = gen_initial_dissection ~ticks () in + let* our_states = gen_our_states dissection (succ ticks) in + let* new_dissection, start_chunk, stop_chunk = + gen_dissection ~number_of_sections ~our_states dissection + in + return (new_dissection, start_chunk, stop_chunk, number_of_sections)) + (fun (dissection, start_chunk, stop_chunk, default_number_of_sections) -> + let open Lwt_syntax in + let expected_reason dissection = + match (List.hd dissection, List.last_opt dissection) with + | Some Game.{tick = a_tick; _}, Some {tick = b_tick; _} -> + Game.Dissection_edge_ticks_mismatch + { + dissection_start_tick = a_tick; + dissection_stop_tick = b_tick; + chunk_start_tick = start_chunk.tick; + chunk_stop_tick = stop_chunk.tick; + } + | _ -> assert false + in + let modify_tick modify_X dissection = + let invalid_dissection = + modify_X + (fun chunk -> Game.{chunk with tick = Tick.next chunk.tick}) + dissection + in + let* res = + Game.Internal_for_tests.check_dissection + ~default_number_of_sections + ~start_chunk + ~stop_chunk + invalid_dissection + in + let expected_reason = expected_reason invalid_dissection in + return (expect_invalid_move expected_reason res) + in + (* We modify the start tick and expect the failure. *) + let* b1 = modify_tick modify_start dissection in + (* We modify the stop tick and expect the failure. *) + let* b2 = modify_tick modify_stop dissection in + return (b1 && b2)) + + (** Test that a valid dissection must have a proper distribution of the + sections. That is, a section should not be geq than half of the + dissected section's distance. *) + let test_badly_distributed_dissection = + let open QCheck2 in + qcheck_make_lwt + ~count + ~name:"dissection must be well distributed" + ~gen: + (let open Gen in + (* The test is not general enough to support all kind of number of + sections. *) + let number_of_sections = + Tezos_protocol_alpha_parameters.Default_parameters.constants_mainnet + .sc_rollup + .number_of_sections_in_dissection + in + let* picked_section = 0 -- (number_of_sections - 2) in + let* ticks = 100 -- 1_000 in + let* dissection = gen_initial_dissection ~ticks () in + let* our_states = gen_our_states dissection (succ ticks) in + let* new_dissection, start_chunk, stop_chunk = + gen_dissection ~number_of_sections ~our_states dissection in return - { - initial; - gen_next_move = - (fun game -> - random_decision - ~default_number_of_sections:game.default_number_of_sections - game.dissection); - } - | MachineDirected -> QCheck2.Gen.return machine_directed - - (** [test_strategies defender_strategy refuter_strategy expectation inbox] - runs a game based oin the two given strategies and checks that the - resulting outcome fits the expectations. *) - let test_strategies ~default_number_of_sections defender_strategy - refuter_strategy expectation inbox = - let open QCheck2.Gen in - let* defender_client = - player_from_strategy ~default_number_of_sections defender_strategy - in - let* refuter_client = - player_from_strategy ~default_number_of_sections refuter_strategy - in - - let* outcome = - run ~default_number_of_sections ~inbox ~defender_client ~refuter_client - in - return - Lwt.Syntax.( - let* outcome = outcome in - expectation outcome) - - (** the possible expectation functions *) - let defender_wins x = Lwt.return @@ equal_outcome Defender_wins x - - let refuter_wins x = Lwt.return @@ equal_outcome Refuter_wins x - - let all_win _ = Lwt.return_true + ( new_dissection, + start_chunk, + stop_chunk, + number_of_sections, + picked_section )) + (fun ( dissection, + start_chunk, + stop_chunk, + default_number_of_sections, + picked_section ) -> + let open Lwt_syntax in + (* We put a distance of [1] in every section. Then, we put the + distance's left in the [picked_section], it will create + an invalid section. *) + let distance = + Z.succ @@ Tick.distance start_chunk.tick stop_chunk.tick + in + let max_section_length = + Z.(succ @@ (distance - of_int default_number_of_sections)) + in + let section_length = Z.one in + + (* Replace the distance of the first [k] sections by [section_length]. + In practice, when [k = 0], we're at the last section of the + dissection. *) + let rec replace_distances tick k = function + | a :: b :: xs -> + let b, tick = + if k = 0 then + let tick = Tick.jump tick max_section_length in + (Game.{b with tick}, tick) + else + let tick = Tick.jump tick section_length in + (Game.{b with tick}, tick) + in + a :: replace_distances tick (k - 1) (b :: xs) + | xs -> xs + in + let invalid_dissection = + replace_distances start_chunk.tick picked_section dissection + in + let* res = + Game.Internal_for_tests.check_dissection + ~default_number_of_sections + ~start_chunk + ~stop_chunk + invalid_dissection + in + let expected_reason = Game.Dissection_invalid_distribution in + + return (expect_invalid_move expected_reason res)) + + let tests = + ( "Dissection", + qcheck_wrap + [ + test_valid_gen_dissection; + test_truncated_small_dissection; + test_truncated_large_dissection; + test_immutable_start_chunk; + test_stop_hash_must_change; + test_immutable_start_and_stop_ticks; + test_badly_distributed_dissection; + ] ) end -(* just the snapshot of an empty inbox to start.*) -let empty_snapshot = - let rollup = Address.hash_string [""] in - let level = Raw_level.root in - let context = Tezos_protocol_environment.Memory_context.empty in - let inbox = Lwt_main.run @@ Inbox.empty context rollup level in - Inbox.take_snapshot inbox - -(** The following are the possible combinations of strategy generators. *) -let perfect_perfect (module P : TestPVM) default_number_of_sections : - bool Lwt.t QCheck2.Gen.t = - let module R = Strategies (P) in - R.test_strategies - ~default_number_of_sections - MachineDirected - MachineDirected - R.defender_wins - empty_snapshot - -let random_random (module P : TestPVM) default_number_of_sections = - let module R = Strategies (P) in - R.test_strategies - ~default_number_of_sections - Random - Random - R.all_win - empty_snapshot - -let random_perfect (module P : TestPVM) default_number_of_sections = - let module S = Strategies (P) in - S.test_strategies - Random - MachineDirected - S.refuter_wins - empty_snapshot - ~default_number_of_sections - -let perfect_random (module P : TestPVM) default_number_of_sections = - let module S = Strategies (P) in - S.test_strategies - MachineDirected - Random - S.defender_wins - empty_snapshot - ~default_number_of_sections - -(* a generator for a randomPVM.*) -let gen_randomPVM = - let open QCheck2.Gen in - let* initial_prog = list_size small_int (int_range 1 100) in - return - (module MakeRandomPVM (struct - let initial_prog = initial_prog - end) : TestPVM) - -(* a generator for a countPVM.*) -let gen_countPVM = - let open QCheck2.Gen in - let* target = small_int in - return - (module MakeCountingPVM (struct - let target = target - end) : TestPVM) - -(* TODO: 3382 in the case that the inputs are generated with a large enough size - (say 10000) the limits on encoding/decoding make the test fail.*) -(* a generator for an arithPVM.*) -let gen_arithPVM = - let open QCheck2.Gen in - let* inputs = gen_list ~size:(3 -- 100) in - let* evals = small_int in - return - (module TestArith (struct - let inputs = String.concat " " inputs - - let evals = evals - end) : TestPVM) - -(* [generate_strategy_response strategy_gen pvm_gen] generate the boolean - response that you get by applying strategy_gen to pvm_gen. The strategy_gen - is one of [perfect_perfect, perfect_random, random_perfect, random_random] - and the pvm_gen is one of [gen_randomPVM, gen_countPVM, gen_arithPVM] *) -let generate_strategy_response func gen : bool Lwt.t QCheck2.Gen.t = - let open QCheck2.Gen in - let result1 = map func gen in - let result = result1 <*> gen_num_sections in - join result - -(** This assembles a test from a RandomPVM generator and a strategy generator. *) -let testing_PVM func mod_gen name = - let open QCheck2 in - Test.make ~name (generate_strategy_response func mod_gen) (fun x -> - Lwt_main.run x) - -(* generator for a dissection produced from of a fixed section*) -let generate_dissection_of_section (module P : TestPVM) = - let open P in - let module S = Strategies (P) in - let open QCheck2.Gen in - let* start_at = int_range 1 10000 - and* length = int_range 5 100 - and* stop_hash = gen_random_hash - and* default_number_of_sections = gen_num_sections in - let section_start_state = Utils.default_state in - let section_stop_at = tick_of_int_exn (start_at + length) in - let section_start_at = tick_of_int_exn start_at in - let result = - let open Lwt.Syntax in - let* option_dissection = - S.dissection_of_section - ~default_number_of_sections - section_start_at - section_start_state - section_stop_at - in - let dissection = - match option_dissection with - | None -> raise (Invalid_argument "no dissection") - | Some x -> x - in - - let* start = state_hash section_start_state in - - let* check = - Game.Internal_for_tests.check_dissection - ~default_number_of_sections - ~start_chunk:{state_hash = Some start; tick = section_start_at} - ~stop_chunk:{state_hash = Some stop_hash; tick = section_stop_at} - dissection - in - Lwt.return (Result.to_option check = Some ()) - in - return result - -let test_dissection_of_section = - let open QCheck2 in - let open Gen in - [ - Test.make - ~name:"randomVPN" - (let* x = gen_randomPVM in - generate_dissection_of_section x) - (fun r -> Lwt_main.run r); - Test.make - ~name:"count" - (let* x = gen_countPVM in - generate_dissection_of_section x) - (fun r -> Lwt_main.run r); - ] - -(* generator for a randomly produced dissection*) -let generate_random_dissection = - let open QCheck2.Gen in - let* start_at = int_range 1 10000 - and* length = int_range 5 100 - and* stop_hash = gen_random_hash - and* default_number_of_sections = gen_num_sections in - let* start_hash = gen_random_hash in - let* new_stop_hash = gen_random_hash in - let section_stop_at = tick_of_int_exn (start_at + length) in - let section_start_at = tick_of_int_exn start_at in - let* option_dissection = - random_dissection - ~default_number_of_sections - section_start_at - start_hash - section_stop_at - (Some stop_hash) - in - let result = - let open Lwt.Syntax in - let dissection = - match option_dissection with - | None -> raise (Invalid_argument "no dissection") - | Some x -> x - in - let* check = - Game.Internal_for_tests.check_dissection - ~default_number_of_sections - ~start_chunk:{state_hash = Some start_hash; tick = section_start_at} - ~stop_chunk:{state_hash = Some new_stop_hash; tick = section_stop_at} - dissection - in - Lwt.return (Result.to_option check = Some ()) - in - return result - -let test_random_dissection = - let open QCheck2 in - [Test.make ~name:"random_dissection" generate_random_dissection Lwt_main.run] +let tests = Dissection.tests :: Test_refutation_game_legacy.tests -let () = - Alcotest.run - "Refutation Game" - [ - ("Dissection tests", qcheck_wrap test_dissection_of_section); - ("Random dissection", qcheck_wrap test_random_dissection); - ( "RandomPVM", - qcheck_wrap - [ - testing_PVM perfect_perfect gen_randomPVM "perfect-perfect"; - testing_PVM random_random gen_randomPVM "random-random"; - testing_PVM random_perfect gen_randomPVM "random-perfect"; - testing_PVM perfect_random gen_randomPVM "perfect-random"; - ] ); - ( "CountingPVM", - qcheck_wrap - [ - testing_PVM perfect_perfect gen_countPVM "perfect-perfect"; - testing_PVM random_random gen_countPVM "random-random"; - testing_PVM random_perfect gen_countPVM "random-perfect"; - testing_PVM perfect_random gen_countPVM "perfect-random"; - ] ); - ( "ArithPVM", - qcheck_wrap - [ - testing_PVM perfect_perfect gen_arithPVM "perfect-perfect"; - testing_PVM random_random gen_arithPVM "random-random"; - testing_PVM random_perfect gen_arithPVM "random-perfect"; - testing_PVM perfect_random gen_arithPVM "perfect-random"; - ] ); - ] +let () = Alcotest.run "Refutation_game" tests diff --git a/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game_legacy.ml b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game_legacy.ml new file mode 100644 index 0000000000000000000000000000000000000000..e0bc5b3b92e287da6fd5fa72ced099858fd59057 --- /dev/null +++ b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game_legacy.ml @@ -0,0 +1,1158 @@ +(*****************************************************************************) +(* *) +(* 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. *) +(* *) +(*****************************************************************************) + +(** Testing + ------- + Component: PBT for the SCORU refutation game + Invocation: dune exec \ + src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.exe + Subject: SCORU refutation game +*) +open Protocol + +open Alpha_context +open Sc_rollup +open Lwt_syntax +open Lib_test.Qcheck2_helpers + +(** + + Helpers + +*) + +let hash_state state number = + Digest.bytes @@ Bytes.of_string @@ state ^ string_of_int number + +type dummy_proof = { + start : State_hash.t; + stop : State_hash.t option; + valid : bool; +} + +module Tick_map = Map.Make (Sc_rollup_tick_repr) + +let dummy_proof_encoding : dummy_proof Data_encoding.t = + let open Data_encoding in + conv + (fun {start; stop; valid} -> (start, stop, valid)) + (fun (start, stop, valid) -> {start; stop; valid}) + (obj3 + (req "start" State_hash.encoding) + (req "stop" (option State_hash.encoding)) + (req "valid" bool)) + +let proof_start_state proof = proof.start + +let proof_stop_state proof = proof.stop + +let number_of_ticks_exn n = + match Number_of_ticks.of_int32 n with + | Some x -> x + | None -> Stdlib.failwith "Bad Number_of_ticks" + +let get_comm pred inbox_level ticks state = + Commitment. + { + predecessor = pred; + inbox_level = Raw_level.of_int32_exn inbox_level; + number_of_ticks = number_of_ticks_exn ticks; + compressed_state = state; + } + +let gen_random_hash = + let open QCheck2.Gen in + let* x = bytes_fixed_gen 32 in + return @@ State_hash.of_bytes_exn x + +let tick_of_int_exn n = + match Tick.of_int n with None -> assert false | Some t -> t + +let tick_to_int_exn t = + match Tick.to_int t with None -> assert false | Some n -> n + +(* Default number of sections in a dissection *) +let gen_num_sections = + let open Tezos_protocol_alpha_parameters.Default_parameters in + let testnet = constants_test.sc_rollup.number_of_sections_in_dissection in + let mainnet = constants_mainnet.sc_rollup.number_of_sections_in_dissection in + let sandbox = constants_sandbox.sc_rollup.number_of_sections_in_dissection in + QCheck2.Gen.( + frequency + [ + (5, pure mainnet); + (4, pure testnet); + (2, pure sandbox); + (1, int_range 4 100); + ]) + +let mk_dissection_chunk (state_hash, tick) = Game.{state_hash; tick} + +let random_dissection ~default_number_of_sections start_at start_hash stop_at + stop_hash = + let open QCheck2.Gen in + let start_int = tick_to_int_exn start_at in + let stop_int = tick_to_int_exn stop_at in + let dist = stop_int - start_int in + let branch = min (dist + 1) default_number_of_sections in + let size = (dist + 1) / (branch - 1) in + + if dist = 1 then return None + else + let* random_hash = gen_random_hash in + return + @@ Result.to_option + (List.init branch ~when_negative_length:"error" (fun i -> + mk_dissection_chunk + @@ + if i = 0 then (Some start_hash, start_at) + else if i = branch - 1 then (stop_hash, stop_at) + else (Some random_hash, tick_of_int_exn (start_int + (i * size))))) + +(** + `genlist` is a `correct list` generator. It generates a list of strings that + are either integers or `+` to be consumed by the arithmetic PVM. + If a `+` is found then the previous two element of the stack are poped + then added and the result is pushed to the stack. + In particular, lists like `[1 +]` are incorrect. + + To preserve the correctness invariant, genlist is a recursive generator that + produce a pair `(stack_size, state_list)` where state_list is a correct list + of integers and `+` and consuming it will produce a `stack` of length + `stack_size`. + For example a result can be `(3, [1; 2; +; 3; +; 2; 2; +; 1;]). + Consuming the list will produce the stack`[6; 4; 2]` which has length 3. + The generator has two branches. + 1. with frequency 1 adds integers to state_list and increases the + corresponding stack_size. + 2. With frequency 2, at each step, it looks at the inductive result + `(self (n - 1))=(stack_size, state_list)`. + If the stack_size is smaller than 2 then it adds an integer to the state_list + and increases the stack_size + Otherwise it adds a plus to the state_list and decreases the stack_size. + Remark: The algorithm is linear in the size of the generated list and + generates all kinds of inputs not only those that produce a stack of size 1. +*) +let gen_list ~size = + QCheck2.Gen.( + map (fun (_, l) -> List.rev l) + @@ sized_size size + @@ fix (fun self n -> + match n with + | 0 -> map (fun x -> (1, [string_of_int x])) small_nat + | n -> + frequency + [ + ( 2, + map2 + (fun x (stack_size, state_list) -> + if stack_size >= 2 then + (stack_size - 1, "+" :: state_list) + else (stack_size + 1, string_of_int x :: state_list)) + small_nat + (self (n - 1)) ); + ( 1, + map2 + (fun x (i, y) -> (i + 1, string_of_int x :: y)) + small_nat + (self (n - 1)) ); + ])) + +(** This uses the above generator to produce a correct program with at + least 3 elements. *) + +let correct_program = + let open QCheck2.Gen in + gen_list ~size:(3 -- 1000) + +module type TestPVM = sig + include PVM.S with type hash = State_hash.t + + module Utils : sig + (** This a post-boot state. It is used as default in many functions. *) + val default_state : state + + (*TODO: These are not used in the current state. They are, however to be + used in the incoming more sophisticated set of tests from Thomas Athorne + *) + + (** [random_state n state] generates a random state. The integer n is + used as a seed in the generation. *) + val random_state : int -> state -> state QCheck2.Gen.t + + (** [make_proof start_state stop_state] produces a proof that the eval of + [start_state] is the [stop_state]. + It will be used by the `verify_proof`. In the arithPVM we use + `produce_tree_proof` which only requires a starting state (tree) + and the transition function. *) + val make_proof : state -> hash option -> proof Lwt.t + + (** Like [make_proof] but produces an invalid proof starting from + any hash. *) + val make_invalid_proof : hash -> hash option -> proof Lwt.t + end +end + +(** + + [MakeCountingPVM (P)] is a PVM whose state is an integer and that + can count up to a certain [P.target]. + + This PVM has no input states. + +*) +module MakeCountingPVM (P : sig + val target : int +end) : TestPVM with type state = int = struct + let name = "countingPVM" + + let parse_boot_sector x = Some x + + let pp_boot_sector fmt x = Format.fprintf fmt "%s" x + + type state = int + + let pp x = Lwt.return @@ fun fmt _ -> Format.pp_print_int fmt x + + type hash = State_hash.t + + type context = unit + + type proof = dummy_proof + + let proof_start_state = proof_start_state + + let proof_stop_state = proof_stop_state + + let proof_input_given _ = None + + let proof_input_requested _ = No_input_required + + let state_hash_ (x : state) = + State_hash.context_hash_to_state_hash + @@ Context_hash.hash_string [Int.to_string x] + + let state_hash (x : state) = return (state_hash_ x) + + let is_input_state x = + if x >= P.target then return Initial else return No_input_required + + let initial_state _ = return 0 + + let install_boot_sector _ _ = return P.target + + let set_input _ s = return s + + module Utils = struct + let default_state = P.target + + let random_state _ _ = QCheck2.Gen.int + + let make_proof s1 s2 = + let* s1 = state_hash s1 in + return {start = s1; stop = s2; valid = true} + + let make_invalid_proof s1 s2 = return {start = s1; stop = s2; valid = false} + end + + let proof_encoding = dummy_proof_encoding + + let eval state = if state >= P.target then return state else return (state + 1) + + let verify_proof proof = return proof.valid + + let produce_proof _ _ _ = Stdlib.failwith "Dummy PVM can't produce proof" + + let verify_origination_proof proof _ = return proof.valid + + let produce_origination_proof _ _ = + Stdlib.failwith "Dummy PVM can't produce proof" + + type output_proof = unit + + let output_proof_encoding = Data_encoding.unit + + let state_of_output_proof _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + let output_of_output_proof _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + let verify_output_proof _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + let produce_output_proof _ _ _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + module Internal_for_tests = struct + let insert_failure _ = Stdlib.failwith "Dummy PVM does not insert failures" + end +end + +(** This is a random PVM. Its state is a pair of a string and a + list of integers. An evaluation step consumes the next integer + of the list and concatenates its representation to the string. *) +module MakeRandomPVM (P : sig + val initial_prog : int list +end) : TestPVM with type state = string * int list = struct + let name = "randomPVM" + + let parse_boot_sector x = Some x + + let pp_boot_sector fmt x = Format.fprintf fmt "%s" x + + type state = string * int list + + let pp (s, xs) = + Lwt.return @@ fun fmt _ -> + Format.fprintf + fmt + "%s / %s" + s + (String.concat ":" @@ List.map string_of_int xs) + + type context = unit + + type proof = dummy_proof + + type hash = State_hash.t + + let to_string (a, b) = + Format.sprintf "(%s, [%s])" a (String.concat ";" @@ List.map Int.to_string b) + + let proof_start_state = proof_start_state + + let proof_stop_state = proof_stop_state + + let proof_input_given _ = None + + let proof_input_requested _ = No_input_required + + let state_hash_ x = + State_hash.context_hash_to_state_hash + @@ Context_hash.hash_string [to_string x] + + let state_hash (x : state) = return @@ state_hash_ x + + let initial_state _ = return ("", []) + + let install_boot_sector _ _ = return ("hello", P.initial_prog) + + let is_input_state (_, c) = + match c with [] -> return Initial | _ -> return No_input_required + + let set_input _ state = return state + + module Utils = struct + let default_state = ("hello", P.initial_prog) + + let random_state length ((_, program) : state) = + let open QCheck2.Gen in + let remaining_program = TzList.drop_n length program in + let+ stop_state = int in + (hash_state "" stop_state, remaining_program) + + let make_proof s1 s2 = + let* s1 = state_hash s1 in + return {start = s1; stop = s2; valid = true} + + let make_invalid_proof s1 s2 = return {start = s1; stop = s2; valid = false} + end + + let proof_encoding = dummy_proof_encoding + + let eval (hash, continuation) = + match continuation with + | [] -> return (hash, continuation) + | h :: tl -> return (hash_state hash h, tl) + + let verify_proof proof = return proof.valid + + let produce_proof _ _ _ = Stdlib.failwith "Dummy PVM can't produce proof" + + let verify_origination_proof proof _ = return proof.valid + + let produce_origination_proof _ _ = + Stdlib.failwith "Dummy PVM can't produce proof" + + type output_proof = unit + + let output_proof_encoding = Data_encoding.unit + + let state_of_output_proof _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + let output_of_output_proof _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + let verify_output_proof _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + let produce_output_proof _ _ _ = + Stdlib.failwith "Dummy PVM can't handle output proof" + + module Internal_for_tests = struct + let insert_failure _ = Stdlib.failwith "Dummy PVM does not insert failures" + end +end + +module ContextPVM = ArithPVM.Make (struct + open Tezos_context_memory.Context + + module Tree = struct + include Tezos_context_memory.Context.Tree + + type tree = Tezos_context_memory.Context.tree + + type t = Tezos_context_memory.Context.t + + type key = string list + + type value = bytes + end + + type tree = Tree.tree + + let hash_tree tree = + Sc_rollup.State_hash.context_hash_to_state_hash (Tree.hash tree) + + type proof = Proof.tree Proof.t + + let verify_proof proof f = + Lwt.map Result.to_option (verify_tree_proof proof f) + + let produce_proof context state f = + let* proof = + produce_tree_proof (index context) (`Value (Tree.hash state)) f + in + return (Some proof) + + let kinded_hash_to_state_hash = function + | `Value hash | `Node hash -> State_hash.context_hash_to_state_hash hash + + let proof_before proof = kinded_hash_to_state_hash proof.Proof.before + + let proof_after proof = kinded_hash_to_state_hash proof.Proof.after + + let proof_encoding = + let open Data_encoding in + conv (fun _ -> ()) (fun _ -> assert false) unit +end) + +module TestArith (P : sig + val inputs : string + + val evals : int +end) : TestPVM = struct + include ContextPVM + + let init_context = Tezos_context_memory.make_empty_context () + + module Utils = struct + let make_external_inbox_message str = + WithExceptions.Result.get_ok + ~loc:__LOC__ + Inbox.Message.(External str |> serialize) + + let default_state = + let promise = + let* boot = initial_state init_context in + let* boot = install_boot_sector boot "" in + let* boot = eval boot in + Format.printf "%s\n\n\n" P.inputs ; + let input = + { + inbox_level = Raw_level.root; + message_counter = Z.zero; + payload = make_external_inbox_message P.inputs; + } + in + let prelim = set_input input boot in + List.fold_left (fun acc _ -> acc >>= fun acc -> eval acc) prelim + @@ List.repeat P.evals () + in + Lwt_main.run promise + + let random_state i state = + let open QCheck2.Gen in + let+ program = correct_program in + let input = + { + inbox_level = Raw_level.root; + message_counter = Z.zero; + payload = make_external_inbox_message @@ String.concat " " program; + } + in + let prelim = set_input input state in + let open Lwt in + Lwt_main.run + @@ List.fold_left (fun acc _ -> acc >>= fun acc -> eval acc) prelim + @@ List.repeat (min i (List.length program - 2) + 1) () + + let make_proof s1 _s2 = + let* proof_opt = produce_proof init_context None s1 in + match proof_opt with Ok proof -> return proof | Error _ -> assert false + + let make_invalid_proof _ _ = + let* state = initial_state init_context in + let* state = install_boot_sector state "foooobaaar" in + let* proof_opt = produce_proof init_context None state in + match proof_opt with Ok proof -> return proof | Error _ -> assert false + end +end + +(** + This module introduces some testing strategies for a game created + from a PVM. +*) +module Strategies (PVM : TestPVM with type hash = State_hash.t) = struct + (** [exec_all state tick] runs eval until the state machine reaches a + state where it requires an input. It returns the new state and the + final tick. + *) + let exec_all state tick = + let rec loop state tick = + let* isinp = PVM.is_input_state state in + match isinp with + | No_input_required -> + let* s = PVM.eval state in + let* hash1 = PVM.state_hash state in + let* hash2 = PVM.state_hash s in + + if State_hash.equal hash1 hash2 then assert false + else loop s (Tick.next tick) + | _ -> return (state, tick) + in + loop state tick + + (** [state_at to_tick from_state from_tick] returns the state at tick + [to_tick], or [None] if that's past the point at which the machine + has stopped. *) + let state_at to_tick from_state from_tick = + let rec loop state tick = + let* isinp = PVM.is_input_state state in + if Tick.equal to_tick tick then return (Some state, tick) + else + match isinp with + | No_input_required -> + let* s = PVM.eval state in + let* hash1 = PVM.state_hash state in + let* hash2 = PVM.state_hash s in + + if State_hash.equal hash1 hash2 then assert false + else loop s (Tick.next tick) + | _ -> return (None, to_tick) + in + loop from_state from_tick + + (** [dissection_of_section start_tick start_state stop_tick] creates + a dissection with at most {!default_number_of_sections} pieces + that are (roughly) equal + spaced and whose states are computed by running the eval function + until the correct tick. Note that the last piece can be as much + as {!default_number_of_sections} - 1 ticks longer than the others. *) + let dissection_of_section ~default_number_of_sections start_tick start_state + stop_tick = + let start_int = tick_to_int_exn start_tick in + let stop_int = tick_to_int_exn stop_tick in + let dist = stop_int - start_int in + if dist = 1 then return None + else + let branch = min (dist + 1) default_number_of_sections in + let size = (dist + 1) / (branch - 1) in + let tick_list = + Result.to_option + @@ List.init branch ~when_negative_length:"error" (fun i -> + if i = branch - 1 then stop_tick + else tick_of_int_exn (start_int + (i * size))) + in + let a = + Option.map + (fun a -> + List.map + (fun tick -> + let hash = + Lwt_main.run + @@ let* state, (_ : Tick.t) = + state_at tick start_state start_tick + in + match state with + | None -> return None + | Some s -> + let* h = PVM.state_hash s in + return (Some h) + in + mk_dissection_chunk (hash, tick)) + a) + tick_list + in + return a + + type client = { + initial : (Tick.t * PVM.hash) option Lwt.t; + gen_next_move : Game.t -> Game.refutation option Lwt.t QCheck2.Gen.t; + } + + type outcome_for_tests = Defender_wins | Refuter_wins + + let equal_outcome a b = + match (a, b) with + | Defender_wins, Defender_wins -> true + | Refuter_wins, Refuter_wins -> true + | _ -> false + + let loser_to_outcome_for_tests loser alice_is_refuter = + match loser with + | Game.Bob -> if alice_is_refuter then Refuter_wins else Defender_wins + | Game.Alice -> if alice_is_refuter then Defender_wins else Refuter_wins + + let run ~default_number_of_sections ~inbox ~refuter_client ~defender_client = + let refuter, (_ : public_key), (_ : Signature.secret_key) = + Signature.generate_key () + in + let defender, (_ : public_key), (_ : Signature.secret_key) = + Signature.generate_key () + in + let alice_is_refuter = Staker.(refuter < defender) in + let initial_game = + let* start_hash = PVM.state_hash PVM.Utils.default_state in + let* initial_data = defender_client.initial in + let tick, initial_hash = + match initial_data with None -> assert false | Some s -> s + in + let int_tick = tick_to_int_exn tick in + let number_of_ticks = Int32.of_int int_tick in + let parent = get_comm Commitment.Hash.zero 0l 1l start_hash in + let child = + get_comm Commitment.Hash.zero 0l number_of_ticks initial_hash + in + Lwt.return + @@ Game.initial + inbox + ~pvm_name:PVM.name + ~parent + ~child + ~refuter + ~defender + ~default_number_of_sections + in + + let outcome = + let rec loop game refuter_move = + let open QCheck2.Gen in + let* move = + if refuter_move then refuter_client.gen_next_move game + else defender_client.gen_next_move game + in + let move = Lwt_main.run move in + match move with + | None -> + return + @@ Lwt.return (if refuter_move then Defender_wins else Refuter_wins) + | Some move -> ( + let game_result = Lwt_main.run @@ Game.play game move in + match game_result with + | Either.Left outcome -> + return + @@ Lwt.return + (loser_to_outcome_for_tests outcome.loser alice_is_refuter) + | Either.Right game -> loop game (not refuter_move)) + in + loop (Lwt_main.run initial_game) true + in + outcome + + let random_tick ?(from = 0) ~into () = + let open QCheck2.Gen in + let* x = from -- into in + return @@ Option.value ~default:Tick.initial (Tick.of_int x) + + (** + checks that the stop state of a section conflicts with the one computed by the + evaluation. + *) + let conflicting_section tick state = + let* new_state, (_ : Tick.t) = + state_at tick PVM.Utils.default_state Tick.initial + in + let* new_hash = + match new_state with + | None -> return None + | Some state -> + let* state = PVM.state_hash state in + return (Some state) + in + + return @@ not (Option.equal ( = ) state new_hash) + + (** This function assembles 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 + decision with this dissection.*) + let random_decision ~default_number_of_sections d = + let open QCheck2.Gen in + let number_of_somes = + List.length + (List.filter (fun {Game.state_hash; _} -> Option.is_some state_hash) d) + in + let* x = int_range 0 (number_of_somes - 1) in + let x = if x = number_of_somes - 1 then max 0 (x - 1) else x in + let start_hash, start = + match List.nth d x with + | Some Game.{state_hash = Some s; tick = t} -> (s, t) + | _ -> assert false + in + let (_ : State_hash.t option), stop = + match List.nth d (x + 1) with + | Some Game.{state_hash; tick} -> (state_hash, tick) + | None -> assert false + in + let* stop_hash = gen_random_hash in + + let random_dissection = + random_dissection + ~default_number_of_sections + start + start_hash + stop + (Some stop_hash) + in + let* random_dissection = random_dissection and* hash = gen_random_hash in + + let game = + match random_dissection with + | None -> + let open Lwt.Syntax in + let* pvm_proof = + PVM.Utils.make_invalid_proof start_hash (Some hash) + in + let wrapped = + let module P = struct + include PVM + + let proof = pvm_proof + end in + Unencodable (module P) + in + let proof = Proof.{pvm_step = wrapped; inbox = None} in + Lwt.return (Some Game.{choice = start; step = Proof proof}) + | Some dissection -> + Lwt.return (Some Game.{choice = start; step = Dissection dissection}) + in + + return game + + (** There are two kinds of strategies, random and machine-directed. *) + type strategy = Random | MachineDirected + + (** + [find_conflict dissection] finds the section (if it exists) in a dissection that + conflicts with the actual computation. *) + let find_conflict dissection = + let rec aux states = + match states with + | start :: next :: rest -> + let Game.{state_hash = start_state; tick = start_tick} = start in + let Game.{state_hash = next_state; tick = next_tick} = next in + let* c0 = conflicting_section start_tick start_state in + let* c = conflicting_section next_tick next_state in + if c0 then assert false + else if c then + if next_state = None then return None + else + return (Some ((start_state, start_tick), (next_state, next_tick))) + else aux (next :: rest) + | _ -> return None + in + aux dissection + + (** [next_move branching dissection] finds the next move based on a + dissection. + It finds the first section of dissection that conflicts with the evaluation. + If the section has length one tick it returns a move with a Conclude + conflict_resolution_step. + If the section is longer it creates a new dissection with branching + many pieces and returns + a move with a Refine type conflict_resolution_step. + *) + let next_move ~default_number_of_sections dissection = + let* conflict = find_conflict dissection in + match conflict with + | Some ((_, start_tick), (_, next_tick)) -> + let* start_state, (_ : Tick.t) = + state_at start_tick PVM.Utils.default_state Tick.initial + in + let* next_dissection = + match start_state with + | None -> return None + | Some s -> + dissection_of_section + ~default_number_of_sections + start_tick + s + next_tick + in + let* stop_state, (_ : Tick.t) = + match start_state with + | None -> return (None, next_tick) + | Some s -> state_at next_tick s start_tick + in + let* refutation = + match next_dissection with + | None -> + let* stop_hash = + match stop_state with + | None -> return None + | Some state -> + let* s = PVM.state_hash state in + return (Some s) + in + let* pvm_proof = + match start_state with + | Some s -> PVM.Utils.make_proof s stop_hash + | None -> assert false + in + let wrapped = + let module P = struct + include PVM + + let proof = pvm_proof + end in + Unencodable (module P) + in + let proof = Proof.{pvm_step = wrapped; inbox = None} in + return Game.{choice = start_tick; step = Proof proof} + | Some next_dissection -> + return + Game.{choice = start_tick; step = Dissection next_dissection} + in + + return (Some refutation) + | None -> return None + + (** This is an automatic client. It generates a "perfect" client. *) + let machine_directed = + let start_state = PVM.Utils.default_state in + let initial = + let* stop_state, stop_at = exec_all start_state Tick.initial in + let* stop_hash = PVM.state_hash stop_state in + return (Some (stop_at, stop_hash)) + in + + let gen_next_move (game : Game.t) = + let dissection = game.dissection in + let new_move = + let* mv = + next_move + ~default_number_of_sections:game.default_number_of_sections + dissection + in + match mv with Some move -> return (Some move) | None -> return None + in + QCheck2.Gen.return new_move + in + + {initial; gen_next_move} + + (** This builds a client from a strategy. If the strategy is + MachineDirected it uses the above constructions. If the strategy + is random then it uses a random section for the initial + commitments and the random decision for the next move. *) + let player_from_strategy ~default_number_of_sections = function + | Random -> + let open QCheck2.Gen in + let* random_tick = + random_tick ~from:1 ~into:(default_number_of_sections - 1) () + in + let initial = + Lwt.Syntax.( + let random_state = PVM.Utils.default_state in + let* stop_hash = PVM.state_hash random_state in + Lwt.return (Some (random_tick, stop_hash))) + in + return + { + initial; + gen_next_move = + (fun game -> + random_decision + ~default_number_of_sections:game.default_number_of_sections + game.dissection); + } + | MachineDirected -> QCheck2.Gen.return machine_directed + + (** [test_strategies defender_strategy refuter_strategy expectation inbox] + runs a game based oin the two given strategies and checks that the + resulting outcome fits the expectations. *) + let test_strategies ~default_number_of_sections defender_strategy + refuter_strategy expectation inbox = + let open QCheck2.Gen in + let* defender_client = + player_from_strategy ~default_number_of_sections defender_strategy + in + let* refuter_client = + player_from_strategy ~default_number_of_sections refuter_strategy + in + + let* outcome = + run ~default_number_of_sections ~inbox ~defender_client ~refuter_client + in + return + Lwt.Syntax.( + let* outcome = outcome in + expectation outcome) + + (** the possible expectation functions *) + let defender_wins x = Lwt.return @@ equal_outcome Defender_wins x + + let refuter_wins x = Lwt.return @@ equal_outcome Refuter_wins x + + let all_win _ = Lwt.return_true +end + +(* just the snapshot of an empty inbox to start.*) +let empty_snapshot = + let rollup = Address.hash_string [""] in + let level = Raw_level.root in + let context = Tezos_protocol_environment.Memory_context.empty in + let inbox = Lwt_main.run @@ Inbox.empty context rollup level in + Inbox.take_snapshot inbox + +(** The following are the possible combinations of strategy generators. *) +let perfect_perfect (module P : TestPVM) default_number_of_sections : + bool Lwt.t QCheck2.Gen.t = + let module R = Strategies (P) in + R.test_strategies + ~default_number_of_sections + MachineDirected + MachineDirected + R.defender_wins + empty_snapshot + +let random_random (module P : TestPVM) default_number_of_sections = + let module R = Strategies (P) in + R.test_strategies + ~default_number_of_sections + Random + Random + R.all_win + empty_snapshot + +let random_perfect (module P : TestPVM) default_number_of_sections = + let module S = Strategies (P) in + S.test_strategies + Random + MachineDirected + S.refuter_wins + empty_snapshot + ~default_number_of_sections + +let perfect_random (module P : TestPVM) default_number_of_sections = + let module S = Strategies (P) in + S.test_strategies + MachineDirected + Random + S.defender_wins + empty_snapshot + ~default_number_of_sections + +(* a generator for a randomPVM.*) +let gen_randomPVM = + let open QCheck2.Gen in + let* initial_prog = list_size small_int (int_range 1 100) in + return + (module MakeRandomPVM (struct + let initial_prog = initial_prog + end) : TestPVM) + +(* a generator for a countPVM.*) +let gen_countPVM = + let open QCheck2.Gen in + let* target = small_int in + return + (module MakeCountingPVM (struct + let target = target + end) : TestPVM) + +(* TODO: 3382 in the case that the inputs are generated with a large enough size + (say 10000) the limits on encoding/decoding make the test fail.*) +(* a generator for an arithPVM.*) +let gen_arithPVM = + let open QCheck2.Gen in + let* inputs = gen_list ~size:(3 -- 100) in + let* evals = small_int in + return + (module TestArith (struct + let inputs = String.concat " " inputs + + let evals = evals + end) : TestPVM) + +(* [generate_strategy_response strategy_gen pvm_gen] generate the boolean + response that you get by applying strategy_gen to pvm_gen. The strategy_gen + is one of [perfect_perfect, perfect_random, random_perfect, random_random] + and the pvm_gen is one of [gen_randomPVM, gen_countPVM, gen_arithPVM] *) +let generate_strategy_response func gen : bool Lwt.t QCheck2.Gen.t = + let open QCheck2.Gen in + let result1 = map func gen in + let result = result1 <*> gen_num_sections in + join result + +(** This assembles a test from a RandomPVM generator and a strategy generator. *) +let testing_PVM func mod_gen name = + let open QCheck2 in + Test.make ~name (generate_strategy_response func mod_gen) (fun x -> + Lwt_main.run x) + +(* generator for a dissection produced from of a fixed section*) +let generate_dissection_of_section (module P : TestPVM) = + let open P in + let module S = Strategies (P) in + let open QCheck2.Gen in + let* start_at = int_range 1 10000 + and* length = int_range 5 100 + and* stop_hash = gen_random_hash + and* default_number_of_sections = gen_num_sections in + let section_start_state = Utils.default_state in + let section_stop_at = tick_of_int_exn (start_at + length) in + let section_start_at = tick_of_int_exn start_at in + let result = + let open Lwt.Syntax in + let* option_dissection = + S.dissection_of_section + ~default_number_of_sections + section_start_at + section_start_state + section_stop_at + in + let dissection = + match option_dissection with + | None -> raise (Invalid_argument "no dissection") + | Some x -> x + in + + let* start = state_hash section_start_state in + + let* check = + Game.Internal_for_tests.check_dissection + ~default_number_of_sections + ~start_chunk:{state_hash = Some start; tick = section_start_at} + ~stop_chunk:{state_hash = Some stop_hash; tick = section_stop_at} + dissection + in + Lwt.return (Result.to_option check = Some ()) + in + return result + +let test_dissection_of_section = + let open QCheck2 in + let open Gen in + [ + Test.make + ~name:"randomVPN" + (let* x = gen_randomPVM in + generate_dissection_of_section x) + (fun r -> Lwt_main.run r); + Test.make + ~name:"count" + (let* x = gen_countPVM in + generate_dissection_of_section x) + (fun r -> Lwt_main.run r); + ] + +(* generator for a randomly produced dissection*) +let generate_random_dissection = + let open QCheck2.Gen in + let* start_at = int_range 1 10000 + and* length = int_range 5 100 + and* stop_hash = gen_random_hash + and* default_number_of_sections = gen_num_sections in + let* start_hash = gen_random_hash in + let* new_stop_hash = gen_random_hash in + let section_stop_at = tick_of_int_exn (start_at + length) in + let section_start_at = tick_of_int_exn start_at in + let* option_dissection = + random_dissection + ~default_number_of_sections + section_start_at + start_hash + section_stop_at + (Some stop_hash) + in + let result = + let open Lwt.Syntax in + let dissection = + match option_dissection with + | None -> raise (Invalid_argument "no dissection") + | Some x -> x + in + let* check = + Game.Internal_for_tests.check_dissection + ~default_number_of_sections + ~start_chunk:{state_hash = Some start_hash; tick = section_start_at} + ~stop_chunk:{state_hash = Some new_stop_hash; tick = section_stop_at} + dissection + in + Lwt.return (Result.to_option check = Some ()) + in + return result + +let test_random_dissection = + let open QCheck2 in + [Test.make ~name:"random_dissection" generate_random_dissection Lwt_main.run] + +let tests = + [ + ("Dissection tests", qcheck_wrap test_dissection_of_section); + ("Random dissection", qcheck_wrap test_random_dissection); + ( "RandomPVM", + qcheck_wrap + [ + testing_PVM perfect_perfect gen_randomPVM "perfect-perfect"; + testing_PVM random_random gen_randomPVM "random-random"; + testing_PVM random_perfect gen_randomPVM "random-perfect"; + testing_PVM perfect_random gen_randomPVM "perfect-random"; + ] ); + ( "CountingPVM", + qcheck_wrap + [ + testing_PVM perfect_perfect gen_countPVM "perfect-perfect"; + testing_PVM random_random gen_countPVM "random-random"; + testing_PVM random_perfect gen_countPVM "random-perfect"; + testing_PVM perfect_random gen_countPVM "perfect-random"; + ] ); + ( "ArithPVM", + qcheck_wrap + [ + testing_PVM perfect_perfect gen_arithPVM "perfect-perfect"; + testing_PVM random_random gen_arithPVM "random-random"; + testing_PVM random_perfect gen_arithPVM "random-perfect"; + testing_PVM perfect_random gen_arithPVM "perfect-random"; + ] ); + ] diff --git a/src/proto_alpha/lib_sc_rollup/game_helpers.ml b/src/proto_alpha/lib_sc_rollup/game_helpers.ml new file mode 100644 index 0000000000000000000000000000000000000000..62038eb312ccadeb43036cd7712d4c23e477e206 --- /dev/null +++ b/src/proto_alpha/lib_sc_rollup/game_helpers.ml @@ -0,0 +1,70 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 Nomadic Labs, *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +open Protocol.Alpha_context.Sc_rollup + +let new_dissection ~state_hash_from_tick ~default_number_of_sections + ~(start_chunk : Game.dissection_chunk) + ~(our_stop_chunk : Game.dissection_chunk) = + let open Lwt_result_syntax in + let max_number_of_sections = Z.of_int default_number_of_sections in + let trace_length = + Z.succ (Tick.distance our_stop_chunk.tick start_chunk.tick) + in + let number_of_sections = Z.min max_number_of_sections trace_length in + let rem = Z.(rem trace_length number_of_sections) in + let first_section_length, section_length = + if Compare.Z.(trace_length < max_number_of_sections) then + (* In this case, every section is of length one. *) + Z.(one, one) + else + let section_length = Z.(max one (div trace_length number_of_sections)) in + if Compare.Z.(section_length = Z.one) && not Compare.Z.(rem = Z.zero) then + (* If we put [section_length] in this situation, we will most likely + have a very long last section. *) + (rem, section_length) + else (section_length, section_length) + in + (* [k] is the number of sections in [rev_dissection]. *) + let rec make rev_dissection k tick : Game.dissection_chunk list tzresult Lwt.t + = + if Z.(equal k (pred number_of_sections)) then + return + @@ List.rev + (({ + state_hash = our_stop_chunk.state_hash; + tick = our_stop_chunk.tick; + } + : Game.dissection_chunk) + :: rev_dissection) + else + let* state_hash = state_hash_from_tick tick in + let next_tick = Tick.jump tick section_length in + make ({state_hash; tick} :: rev_dissection) (Z.succ k) next_tick + in + make + [{state_hash = start_chunk.state_hash; tick = start_chunk.tick}] + Z.one + (Tick.jump start_chunk.tick first_section_length) diff --git a/src/proto_alpha/lib_sc_rollup/game_helpers.mli b/src/proto_alpha/lib_sc_rollup/game_helpers.mli new file mode 100644 index 0000000000000000000000000000000000000000..ef07fc238306c99a59b4d8c5fe922feeb7e7d4fe --- /dev/null +++ b/src/proto_alpha/lib_sc_rollup/game_helpers.mli @@ -0,0 +1,36 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2022 Nomadic Labs, *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +open Protocol.Alpha_context.Sc_rollup + +(** Create a valid dissection based on the agreed [start_chunk] and our vision + of the stop chunk [our_stop_chunk]. We use [state_hash_from_tick] to + give our vision of the state hashes for each tick. *) +val new_dissection : + state_hash_from_tick:(Tick.t -> State_hash.t option tzresult Lwt.t) -> + default_number_of_sections:int -> + start_chunk:Game.dissection_chunk -> + our_stop_chunk:Game.dissection_chunk -> + Game.dissection_chunk list tzresult Lwt.t