From 4b11f4387591b9bfb0dc7332dddd7f1b86413bb3 Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Fri, 25 Mar 2022 16:38:44 +0000 Subject: [PATCH 01/11] SCORU: added refutation tests for ArithPVM --- .../lib_protocol/sc_rollup_arith.ml | 5 +- .../lib_protocol/sc_rollup_arith.mli | 6 +- src/proto_alpha/lib_protocol/test/pbt/dune | 1 + .../test/pbt/refutation_game_pbt.ml | 154 +++++++++++++++++- 4 files changed, 163 insertions(+), 3 deletions(-) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml index 67d40d068be5..06d77030a44e 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml @@ -85,7 +85,10 @@ module type S = sig end module Make (Context : P) : - S with type context = Context.Tree.t and type state = Context.tree = struct + S + with type context = Context.Tree.t + and type state = Context.tree + and type proof = Context.proof = struct module Tree = Context.Tree type context = Context.Tree.t diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli index cb3fc4bfbdea..7788b995fd61 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli @@ -138,4 +138,8 @@ module type P = sig Lwt.t end -module Make (Context : P) : S with type context = Context.Tree.t +module Make (Context : P) : + S + with type context = Context.Tree.t + and type state = Context.tree + and type proof = Context.proof \ No newline at end of file diff --git a/src/proto_alpha/lib_protocol/test/pbt/dune b/src/proto_alpha/lib_protocol/test/pbt/dune index 71dca108c8c3..3e19dee877fe 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/dune +++ b/src/proto_alpha/lib_protocol/test/pbt/dune @@ -17,6 +17,7 @@ tezos-client-alpha tezos-test-helpers tezos-alpha-test-helpers + tezos-context alcotest qcheck-alcotest tezos-benchmark diff --git a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml index f548b4824d99..9034583d4343 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml @@ -51,6 +51,36 @@ let assume_some opt f = match opt with Some x -> f x | None -> assert false let hash_state state number = Digest.bytes @@ Bytes.of_string @@ state ^ string_of_int number +let check li = + if List.length li < 5 then false + else + try + let l = + List.fold_left + (fun acc el -> + let nacc = if el = "+" then acc - 1 else acc + 1 in + assert (nacc > 0) ; + nacc) + 0 + li + in + l >= 0 + with _ -> false + +let gen_list () = + QCheck2.Gen.( + list + (oneof + [ + return "+"; + (let* x = nat in + return (string_of_int x)); + ])) + +let rec correct_string () = + let c = QCheck2.Gen.(generate1 (gen_list ())) in + if check c then c else correct_string () + module type TestPVM = sig include Sc_rollup_PVM_sem.S @@ -180,6 +210,105 @@ end) : TestPVM with type state = string * int list = struct eval a >>= fun x -> Lwt.return (equal_states x b) end +module ContextPVM = Sc_rollup_arith.Make (struct + 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 = Tezos_context_memory.Context.tree + + type proof = + Tezos_context_memory.Context.Proof.tree Tezos_context_memory.Context.Proof.t + + let verify_proof = Tezos_context_memory.Context.verify_tree_proof + + let kinded_hash_to_state_hash = function + | `Value hash | `Node hash -> + State_hash.hash_bytes [Context_hash.to_bytes hash] + + let proof_start_state proof = + kinded_hash_to_state_hash proof.Tezos_context_memory.Context.Proof.before + + let proof_stop_state proof = + kinded_hash_to_state_hash proof.Tezos_context_memory.Context.Proof.after + + let proof_encoding = + Tezos_context_helpers.Context.Proof_encoding.V2.Tree32.tree_proof_encoding +end) + +module MakeArith (P : sig + val inputs : string + + val evals : int +end) : TestPVM = struct + include ContextPVM + + let init_context = Tezos_context_memory.Context.empty + + module Internal_for_tests = struct + let initial_state = + let promise = + let* boot = initial_state init_context "" >>= eval in + let input = + Sc_rollup_PVM_sem. + { + inbox_level = Raw_level.root; + message_counter = Z.zero; + payload = P.inputs; + } + in + let prelim = set_input input boot in + List.fold_left + (fun acc _ -> acc >>= fun acc -> ContextPVM.eval acc) + prelim + @@ List.repeat P.evals () + in + Lwt_main.run promise + + (* let to_kindered_hash h = + `Value (Context_hash.hash_bytes [State_hash.to_bytes h]) *) + + let random_state i state = + let open ContextPVM in + let program = correct_string () in + let input = + Sc_rollup_PVM_sem. + { + inbox_level = Raw_level.root; + message_counter = Z.zero; + payload = String.concat " " program; + } + in + let prelim = set_input input state in + Lwt_main.run + @@ List.fold_left + (fun acc _ -> acc >>= fun acc -> ContextPVM.eval acc) + prelim + @@ List.repeat i () + + let make_proof before_state _ : proof = + let open Tezos_context_memory.Context in + let promise = + let* ctx = add_tree init_context [] before_state in + let _ = commit ~time:(Tezos_base.Time.Protocol.of_seconds 0L) ctx in + let h = Tree.hash before_state in + produce_tree_proof (index init_context) (`Node h) (fun x -> + let* result = eval x in + Lwt.return (result, ())) + in + let (pf, ()) = Lwt_main.run promise in + pf + end +end + (** This module introduces some testing strategies for a game created from a PVM *) module Strategies (P : TestPVM) = struct @@ -194,7 +323,7 @@ module Strategies (P : TestPVM) = struct if pred tick state then Lwt.return (tick, state) else PVM.eval state >>= fun s -> - if s = state then Lwt.return (tick, state) + if P.state_hash s = P.state_hash state then Lwt.return (tick, state) else loop s (Sc_rollup_tick_repr.next tick) in loop state tick @@ -783,6 +912,21 @@ let testing_countPVM (f : (module TestPVM) -> int option -> bool) name = end)) (Some target)) +let testing_arith (f : (module TestPVM) -> int option -> bool) name = + let open QCheck2 in + Test.make + ~name + Gen.(pair (gen_list ()) small_int) + (fun (inputs, evals) -> + assume (check inputs && evals > List.length inputs / 2) ; + f + (module MakeArith (struct + let inputs = String.concat " " inputs + + let evals = evals + end)) + (Some evals)) + let test_random_dissection (module P : TestPVM) start_at length branching = let open P in let module S = Strategies (P) in @@ -873,4 +1017,12 @@ let () = testing_countPVM random_perfect "random-perfect"; testing_countPVM perfect_random "perfect-random"; ] ); + ( "ArithPVM", + qcheck_wrap + [ + testing_arith perfect_perfect "perfect-perfect"; + testing_arith random_random "random-random"; + testing_arith random_perfect "random-perfect"; + testing_arith perfect_random "perfect-random"; + ] ); ] -- GitLab From 366d713709af31c1a09ff387548e708fb9c3f903 Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Fri, 25 Mar 2022 17:28:58 +0000 Subject: [PATCH 02/11] fixup! SCORU: added refutation tests for ArithPVM --- src/proto_alpha/lib_protocol/sc_rollup_arith.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli index 7788b995fd61..02af78e028b5 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli @@ -142,4 +142,4 @@ module Make (Context : P) : S with type context = Context.Tree.t and type state = Context.tree - and type proof = Context.proof \ No newline at end of file + and type proof = Context.proof -- GitLab From 1ddc1c8f44c8ae8c694e222fd75d92f1a0a01391 Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Mon, 28 Mar 2022 12:30:04 +0100 Subject: [PATCH 03/11] SCORU: bugfix for ArithmeticPVM --- src/proto_alpha/lib_protocol/sc_rollup_arith.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml index 06d77030a44e..cb4f6de4ff21 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml @@ -171,6 +171,8 @@ module Make (Context : P) : val remove : Tree.key -> unit t + val clear_error : unit t + val find_value : Tree.key -> 'a Data_encoding.t -> 'a option t val get_value : default:'a -> Tree.key -> 'a Data_encoding.t -> 'a t @@ -209,6 +211,8 @@ module Make (Context : P) : let* tree = Tree.remove tree key in return (tree, Some ()) + let clear_error = remove internal_error_key + let find_value key encoding state = let open Lwt_syntax in let* obytes = Tree.find state key in @@ -710,6 +714,7 @@ module Make (Context : P) : let open Monad.Syntax in let* () = EvaluationResult.set None in let* () = Stack.clear in + let* () = NextMessage.set None in let* () = Status.set Evaluating in return () @@ -787,6 +792,7 @@ module Make (Context : P) : let reboot = let open Monad.Syntax in let* () = Status.set WaitingForInputMessage in + let* () = clear_error in let* () = Stack.clear in let* () = Code.clear in return () -- GitLab From ff77ae93e12a0e3de1ee06361c4c94283f31bcfd Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Mon, 28 Mar 2022 14:09:31 +0100 Subject: [PATCH 04/11] fixup! fixup! SCORU: added refutation tests for ArithPVM --- src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml index 9034583d4343..76af64501644 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml @@ -918,7 +918,10 @@ let testing_arith (f : (module TestPVM) -> int option -> bool) name = ~name Gen.(pair (gen_list ()) small_int) (fun (inputs, evals) -> - assume (check inputs && evals > List.length inputs / 2) ; + assume + (check inputs + && evals > List.length inputs / 2 + && evals <= List.length inputs) ; f (module MakeArith (struct let inputs = String.concat " " inputs -- GitLab From 0d7e81d62acc452e9078f0563092d3a4ed8d1a29 Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Tue, 29 Mar 2022 11:23:17 +0100 Subject: [PATCH 05/11] fixup! fixup! fixup! SCORU: added refutation tests for ArithPVM --- .../test/pbt/refutation_game_pbt.ml | 119 +++++++++--------- 1 file changed, 59 insertions(+), 60 deletions(-) diff --git a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml index 76af64501644..53e8991f8b25 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml @@ -51,44 +51,48 @@ let assume_some opt f = match opt with Some x -> f x | None -> assert false let hash_state state number = Digest.bytes @@ Bytes.of_string @@ state ^ string_of_int number -let check li = - if List.length li < 5 then false - else - try - let l = - List.fold_left - (fun acc el -> - let nacc = if el = "+" then acc - 1 else acc + 1 in - assert (nacc > 0) ; - nacc) - 0 - li - in - l >= 0 - with _ -> false - -let gen_list () = +(** This is a `correct list` generator. It generates a list of strings that are either integers or `+` +to be consumed by the arithmetic PVM.*) +let gen_list = QCheck2.Gen.( - list - (oneof - [ - return "+"; - (let* x = nat in - return (string_of_int x)); - ])) - + map (fun (_, l) -> List.rev l) + @@ sized + @@ fix (fun self n -> + match n with + | 0 -> map (fun x -> (1, [string_of_int x])) nat + | n -> + frequency + [ + ( 2, + map2 + (fun x (i, y) -> + if i > 2 then (i - 1, "+" :: y) + else (i + 1, string_of_int x :: y)) + nat + (self (n - 1)) ); + ( 1, + map2 + (fun x (i, y) -> (i + 1, string_of_int x :: y)) + nat + (self (n - 1)) ); + ])) + +(**Thi uses the above generator to produce a correct program with at least 3 elements*) let rec correct_string () = - let c = QCheck2.Gen.(generate1 (gen_list ())) in - if check c then c else correct_string () + let x = QCheck2.Gen.(generate1 gen_list) in + if List.length x < 3 then correct_string () else x module type TestPVM = sig include Sc_rollup_PVM_sem.S module Internal_for_tests : sig - val initial_state : state + (** This a post-boot state. It is used as default in many functions. *) + val default_state : state + (** this generates a random state*) val random_state : int -> state -> state + (** This makes a proof from a pair of states. In the arithPVM only one such is needed.*) val make_proof : state -> state -> proof end end @@ -127,7 +131,7 @@ end) : TestPVM with type state = int = struct let set_input _ s = Lwt.return s module Internal_for_tests = struct - let initial_state = P.target + let default_state = P.target let random_state _ _ = Random.bits () @@ -178,7 +182,7 @@ end) : TestPVM with type state = string * int list = struct let set_input _ state = Lwt.return state module Internal_for_tests = struct - let initial_state = ("hello", P.initial_prog) + let default_state = ("hello", P.initial_prog) let random_state length ((_, program) : state) = let remaining_program = TzList.drop_n length program in @@ -244,7 +248,7 @@ module ContextPVM = Sc_rollup_arith.Make (struct Tezos_context_helpers.Context.Proof_encoding.V2.Tree32.tree_proof_encoding end) -module MakeArith (P : sig +module TestArith (P : sig val inputs : string val evals : int @@ -254,7 +258,7 @@ end) : TestPVM = struct let init_context = Tezos_context_memory.Context.empty module Internal_for_tests = struct - let initial_state = + let default_state = let promise = let* boot = initial_state init_context "" >>= eval in let input = @@ -273,9 +277,6 @@ end) : TestPVM = struct in Lwt_main.run promise - (* let to_kindered_hash h = - `Value (Context_hash.hash_bytes [State_hash.to_bytes h]) *) - let random_state i state = let open ContextPVM in let program = correct_string () in @@ -330,11 +331,11 @@ module Strategies (P : TestPVM) = struct let remember history t s = Sc_rollup_tick_repr.Map.add t s history - (** [state_at history tick initial_state] is a lookup in the history. + (** [state_at history tick default_state] is a lookup in the history. If no value at tick exists then it runs eval from the tick t0 to t starting - from initial_state. Here t0 is the last known tick smaller that t + from default_state. Here t0 is the last known tick smaller that t (or the intial tick if no such exits) *) - let state_at history tick initial_state = + let state_at history tick default_state = let (lower, ostate, _) = Sc_rollup_tick_repr.Map.split tick history in match ostate with | Some state -> Lwt.return (state, history) @@ -342,7 +343,7 @@ module Strategies (P : TestPVM) = struct let (tick0, state0) = match Sc_rollup_tick_repr.Map.max_binding lower with | Some (t, s) -> (t, s) - | None -> (Sc_rollup_tick_repr.initial, initial_state) + | None -> (Sc_rollup_tick_repr.initial, default_state) in execute_until tick0 state0 (fun tick' _ -> @@ -393,11 +394,11 @@ module Strategies (P : TestPVM) = struct (Sc_rollup_tick_repr.of_int stop_at) in let* (starting_state, history) = - state_at history section_start_at P.Internal_for_tests.initial_state + state_at history section_start_at P.Internal_for_tests.default_state in let* section_start_state = P.state_hash starting_state in let* (stoping_state, history) = - state_at history section_stop_at P.Internal_for_tests.initial_state + state_at history section_stop_at P.Internal_for_tests.default_state in let* section_stop_state = P.state_hash stoping_state in @@ -430,6 +431,7 @@ module Strategies (P : TestPVM) = struct in let outcome = let rec loop game move = + pp_player Format.std_formatter game.turn ; play game move >>= function | Over outcome -> Lwt.return outcome | Ongoing game -> @@ -479,7 +481,7 @@ module Strategies (P : TestPVM) = struct let section_stop_at = Option.value ~default:start_at stop_at in let random_stop_state = - P.Internal_for_tests.(random_state length initial_state) + P.Internal_for_tests.(random_state length default_state) in let* section_stop_state = P.state_hash random_stop_state in Lwt.return @@ -547,7 +549,7 @@ module Strategies (P : TestPVM) = struct in let section_start_at = section.section_start_at in let section_stop_at = section.section_stop_at in - let start_state = P.Internal_for_tests.(random_state 0 initial_state) in + let start_state = P.Internal_for_tests.(random_state 0 default_state) in let* section_start_state = P.state_hash start_state in let stop_state = assume_some (Sc_rollup_tick_repr.to_int section_stop_at) @@ -555,7 +557,7 @@ module Strategies (P : TestPVM) = struct assume_some (Sc_rollup_tick_repr.to_int section_start_at) @@ fun section_start_at -> P.Internal_for_tests.( - random_state (section_stop_at - section_start_at) initial_state) + random_state (section_stop_at - section_start_at) default_state) in let* section_stop_state = P.state_hash stop_state in @@ -599,7 +601,7 @@ module Strategies (P : TestPVM) = struct state_at history section.section_stop_at - P.Internal_for_tests.initial_state + P.Internal_for_tests.default_state in let* new_hash = P.state_hash new_state in Lwt.return @@ not (section.section_stop_state = new_hash) @@ -633,7 +635,6 @@ module Strategies (P : TestPVM) = struct | None -> raise (TickNotFound Sc_rollup_tick_repr.initial) | Some s -> Lwt.return s in - Game.Section.pp_section Format.std_formatter section ; let* (next_dissection, history) = dissection_of_section history branching section in @@ -645,13 +646,13 @@ module Strategies (P : TestPVM) = struct state_at history (Sc_rollup_tick_repr.next section.section_start_at) - P.Internal_for_tests.initial_state + P.Internal_for_tests.default_state in let* (start_state, _) = state_at history section.section_start_at - P.Internal_for_tests.initial_state + P.Internal_for_tests.default_state in Lwt.return ( Conclude @@ -662,7 +663,7 @@ module Strategies (P : TestPVM) = struct state_at history section.section_stop_at - P.Internal_for_tests.initial_state + P.Internal_for_tests.default_state in let* stop_state = P.state_hash state in Lwt.return (Refine {stop_state; next_dissection}, history) @@ -698,7 +699,7 @@ module Strategies (P : TestPVM) = struct in ({initial; next_move} : _ client) - (** this is an outomatic refuter client. It generates a "perfect" client + (** this is an automatic refuter client. It generates a "perfect" client for the refuter.*) let machine_directed_refuter {branching; _} = let history = Sc_rollup_tick_repr.Map.empty in @@ -727,7 +728,7 @@ module Strategies (P : TestPVM) = struct state_at history section_start_at - P.Internal_for_tests.initial_state + P.Internal_for_tests.default_state in Lwt.return @@ Conclude (None, P.Internal_for_tests.make_proof state stop_state) @@ -802,12 +803,13 @@ module Strategies (P : TestPVM) = struct runs a game based oin the two given strategies and checks that the resulting outcome fits the expectations. *) let test_strategies committer_strategy refuter_strategy expectation = - let start_state = P.Internal_for_tests.initial_state in + let start_state = P.Internal_for_tests.default_state in let committer = committer_from_strategy committer_strategy in let refuter = refuter_from_strategy refuter_strategy in let outcome = run ~start_at:Sc_rollup_tick_repr.initial ~start_state ~committer ~refuter in + pp_outcome Format.std_formatter @@ Lwt_main.run outcome ; expectation outcome (** This is a commuter client having a perfect strategy*) @@ -916,14 +918,11 @@ let testing_arith (f : (module TestPVM) -> int option -> bool) name = let open QCheck2 in Test.make ~name - Gen.(pair (gen_list ()) small_int) + Gen.(pair gen_list small_int) (fun (inputs, evals) -> - assume - (check inputs - && evals > List.length inputs / 2 - && evals <= List.length inputs) ; + assume (evals > 1 && evals < List.length inputs - 1) ; f - (module MakeArith (struct + (module TestArith (struct let inputs = String.concat " " inputs let evals = evals @@ -933,7 +932,7 @@ let testing_arith (f : (module TestPVM) -> int option -> bool) name = let test_random_dissection (module P : TestPVM) start_at length branching = let open P in let module S = Strategies (P) in - let* section_start_state = P.state_hash @@ Internal_for_tests.initial_state in + let* section_start_state = P.state_hash @@ Internal_for_tests.default_state in let section_stop_at = match Sc_rollup_tick_repr.of_int (start_at + length) with | None -> assert false @@ -945,7 +944,7 @@ let test_random_dissection (module P : TestPVM) start_at length branching = | Some x -> x in let* section_stop_state = - P.state_hash @@ Internal_for_tests.(random_state length initial_state) + P.state_hash @@ Internal_for_tests.(random_state length default_state) in let section = S.Game.Section. -- GitLab From a2be5e459e8700651610d4a559b7add51fb9f24f Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Tue, 29 Mar 2022 13:48:10 +0100 Subject: [PATCH 06/11] fixup! fixup! SCORU: added refutation tests for ArithPVM --- .../lib_protocol/test/pbt/refutation_game_pbt.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml index 53e8991f8b25..af8d5963fb78 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml @@ -323,8 +323,11 @@ module Strategies (P : TestPVM) = struct let rec loop state tick = if pred tick state then Lwt.return (tick, state) else - PVM.eval state >>= fun s -> - if P.state_hash s = P.state_hash state then Lwt.return (tick, state) + let* s = PVM.eval state in + let* hash1 = P.state_hash state in + let* hash2 = P.state_hash s in + + if State_hash.equal hash1 hash2 then Lwt.return (tick, state) else loop s (Sc_rollup_tick_repr.next tick) in loop state tick -- GitLab From f2e84858b1e98b601f8f697228d91bc3f3bbd2e3 Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Tue, 19 Apr 2022 09:52:07 +0100 Subject: [PATCH 07/11] fixup! fixup! fixup! SCORU: added refutation tests for ArithPVM --- .../lib_protocol/test/pbt/refutation_game_pbt.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml index af8d5963fb78..d6b17d21aada 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml @@ -293,7 +293,8 @@ end) : TestPVM = struct @@ List.fold_left (fun acc _ -> acc >>= fun acc -> ContextPVM.eval acc) prelim - @@ List.repeat i () + @@ List.repeat (min i (List.length program - 2) + 1) () + (*this avoids a `too long` or `too short` i*) let make_proof before_state _ : proof = let open Tezos_context_memory.Context in @@ -434,7 +435,6 @@ module Strategies (P : TestPVM) = struct in let outcome = let rec loop game move = - pp_player Format.std_formatter game.turn ; play game move >>= function | Over outcome -> Lwt.return outcome | Ongoing game -> @@ -812,7 +812,6 @@ module Strategies (P : TestPVM) = struct let outcome = run ~start_at:Sc_rollup_tick_repr.initial ~start_state ~committer ~refuter in - pp_outcome Format.std_formatter @@ Lwt_main.run outcome ; expectation outcome (** This is a commuter client having a perfect strategy*) @@ -920,6 +919,7 @@ let testing_countPVM (f : (module TestPVM) -> int option -> bool) name = let testing_arith (f : (module TestPVM) -> int option -> bool) name = let open QCheck2 in Test.make + ~count:10000 ~name Gen.(pair gen_list small_int) (fun (inputs, evals) -> -- GitLab From 2ec5ae0b3f7b1db8d3efc2ba19fa0ed0ae48260e Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Tue, 19 Apr 2022 10:28:09 +0100 Subject: [PATCH 08/11] fixup! fixup! fixup! fixup! SCORU: added refutation tests for ArithPVM --- src/proto_alpha/lib_protocol/test/pbt/dune | 70 +++++++++++-------- ...on_game_pbt.ml => test_refutation_game.ml} | 2 +- 2 files changed, 41 insertions(+), 31 deletions(-) rename src/proto_alpha/lib_protocol/test/pbt/{refutation_game_pbt.ml => test_refutation_game.ml} (99%) diff --git a/src/proto_alpha/lib_protocol/test/pbt/dune b/src/proto_alpha/lib_protocol/test/pbt/dune index 3e19dee877fe..20160a422b91 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/dune +++ b/src/proto_alpha/lib_protocol/test/pbt/dune @@ -1,32 +1,42 @@ (tests (package tezos-protocol-alpha-tests) - (names liquidity_baking_pbt - saturation_fuzzing - test_merkle_list - test_gas_properties - test_sampler - test_script_comparison - test_tez_repr - test_tx_rollup_l2_encoding - test_tx_rollup_l2_withdraw_storage - test_sc_rollup_tick_repr - refutation_game_pbt - test_carbonated_map) - (libraries tezos-base - tezos-micheline - tezos-client-alpha - tezos-test-helpers - tezos-alpha-test-helpers - tezos-context - alcotest - qcheck-alcotest - tezos-benchmark - tezos-benchmark-alpha) - (flags (:standard - -open Tezos_base__TzPervasives - -open Tezos_micheline - -open Tezos_client_alpha - -open Tezos_protocol_alpha - -open Tezos_alpha_test_helpers - -open Tezos_benchmark_alpha - -open Tezos_benchmark_type_inference_alpha))) + (names + liquidity_baking_pbt + saturation_fuzzing + test_merkle_list + test_gas_properties + test_sampler + test_script_comparison + test_tez_repr + test_tx_rollup_l2_encoding + test_tx_rollup_l2_withdraw_storage + test_sc_rollup_tick_repr + test_refutation_game + test_carbonated_map) + (libraries + tezos-base + tezos-micheline + tezos-client-alpha + tezos-test-helpers + tezos-alpha-test-helpers + tezos-context + alcotest + qcheck-alcotest + tezos-benchmark + tezos-benchmark-alpha) + (flags + (:standard + -open + Tezos_base__TzPervasives + -open + Tezos_micheline + -open + Tezos_client_alpha + -open + Tezos_protocol_alpha + -open + Tezos_alpha_test_helpers + -open + Tezos_benchmark_alpha + -open + Tezos_benchmark_type_inference_alpha))) diff --git a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml similarity index 99% rename from src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml rename to src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml index d6b17d21aada..853f2d072172 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml @@ -28,7 +28,7 @@ ------- Component: PBT for the SCORU refutation game Invocation: dune exec \ - src/proto_alpha/lib_protocol/test/pbt/refutation_game_pbt.exe + src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.exe Subject: SCORU refutation game *) open Protocol -- GitLab From 17c7c3476b6553cfc93047abb0685ead688465e1 Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Wed, 20 Apr 2022 10:05:49 +0100 Subject: [PATCH 09/11] fixup! fixup! SCORU: added refutation tests for ArithPVM --- src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml | 1 - 1 file changed, 1 deletion(-) 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 853f2d072172..6af621de060b 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 @@ -919,7 +919,6 @@ let testing_countPVM (f : (module TestPVM) -> int option -> bool) name = let testing_arith (f : (module TestPVM) -> int option -> bool) name = let open QCheck2 in Test.make - ~count:10000 ~name Gen.(pair gen_list small_int) (fun (inputs, evals) -> -- GitLab From 654be62b348fd539676438d887230b3ce6c61f8c Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Wed, 20 Apr 2022 10:29:26 +0100 Subject: [PATCH 10/11] fixup! fixup! SCORU: added refutation tests for ArithPVM --- src/proto_alpha/lib_protocol/test/pbt/dune | 70 ++++++++++------------ 1 file changed, 30 insertions(+), 40 deletions(-) diff --git a/src/proto_alpha/lib_protocol/test/pbt/dune b/src/proto_alpha/lib_protocol/test/pbt/dune index 20160a422b91..33a0ff231539 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/dune +++ b/src/proto_alpha/lib_protocol/test/pbt/dune @@ -1,42 +1,32 @@ (tests (package tezos-protocol-alpha-tests) - (names - liquidity_baking_pbt - saturation_fuzzing - test_merkle_list - test_gas_properties - test_sampler - test_script_comparison - test_tez_repr - test_tx_rollup_l2_encoding - test_tx_rollup_l2_withdraw_storage - test_sc_rollup_tick_repr - test_refutation_game - test_carbonated_map) - (libraries - tezos-base - tezos-micheline - tezos-client-alpha - tezos-test-helpers - tezos-alpha-test-helpers - tezos-context - alcotest - qcheck-alcotest - tezos-benchmark - tezos-benchmark-alpha) - (flags - (:standard - -open - Tezos_base__TzPervasives - -open - Tezos_micheline - -open - Tezos_client_alpha - -open - Tezos_protocol_alpha - -open - Tezos_alpha_test_helpers - -open - Tezos_benchmark_alpha - -open - Tezos_benchmark_type_inference_alpha))) + (names liquidity_baking_pbt + saturation_fuzzing + test_merkle_list + test_gas_properties + test_sampler + test_script_comparison + test_tez_repr + test_tx_rollup_l2_encoding + test_tx_rollup_l2_withdraw_storage + test_sc_rollup_tick_repr + test_refutation_game + test_carbonated_map) + (libraries tezos-base + tezos-micheline + tezos-client-alpha + tezos-test-helpers + tezos-alpha-test-helpers + tezos-context + alcotest + qcheck-alcotest + tezos-benchmark + tezos-benchmark-alpha) + (flags (:standard + -open Tezos_base__TzPervasives + -open Tezos_micheline + -open Tezos_client_alpha + -open Tezos_protocol_alpha + -open Tezos_alpha_test_helpers + -open Tezos_benchmark_alpha + -open Tezos_benchmark_type_inference_alpha))) -- GitLab From 2594d08383aadf71313b048e47110c47645a6916 Mon Sep 17 00:00:00 2001 From: Corneliu Hoffman Date: Mon, 25 Apr 2022 10:18:23 +0100 Subject: [PATCH 11/11] SCORU: added documentation to the function --- .../test/pbt/test_refutation_game.ml | 99 ++++++++++--------- 1 file changed, 50 insertions(+), 49 deletions(-) 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 6af621de060b..acda2b5381e8 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 @@ -51,8 +51,26 @@ let assume_some opt f = match opt with Some x -> f x | None -> assert false let hash_state state number = Digest.bytes @@ Bytes.of_string @@ state ^ string_of_int number -(** This is a `correct list` generator. It generates a list of strings that are either integers or `+` -to be consumed by the arithmetic PVM.*) +(** + `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 = QCheck2.Gen.( map (fun (_, l) -> List.rev l) @@ -65,9 +83,10 @@ let gen_list = [ ( 2, map2 - (fun x (i, y) -> - if i > 2 then (i - 1, "+" :: y) - else (i + 1, string_of_int x :: y)) + (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)) nat (self (n - 1)) ); ( 1, @@ -77,7 +96,7 @@ let gen_list = (self (n - 1)) ); ])) -(**Thi uses the above generator to produce a correct program with at least 3 elements*) +(** This uses the above generator to produce a correct program with at least 3 elements. *) let rec correct_string () = let x = QCheck2.Gen.(generate1 gen_list) in if List.length x < 3 then correct_string () else x @@ -85,14 +104,16 @@ let rec correct_string () = module type TestPVM = sig include Sc_rollup_PVM_sem.S - module Internal_for_tests : sig - (** This a post-boot state. It is used as default in many functions. *) + module Utils : sig + (** This a post-boot state. It is used as default in many functions. *) val default_state : state - (** this generates a random state*) + (** [random_state n state] generates a random state. *) val random_state : int -> state -> state - (** This makes a proof from a pair of states. In the arithPVM only one such is needed.*) + (** [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 -> state -> proof end end @@ -130,7 +151,7 @@ end) : TestPVM with type state = int = struct let set_input _ s = Lwt.return s - module Internal_for_tests = struct + module Utils = struct let default_state = P.target let random_state _ _ = Random.bits () @@ -181,7 +202,7 @@ end) : TestPVM with type state = string * int list = struct let set_input _ state = Lwt.return state - module Internal_for_tests = struct + module Utils = struct let default_state = ("hello", P.initial_prog) let random_state length ((_, program) : state) = @@ -257,7 +278,7 @@ end) : TestPVM = struct let init_context = Tezos_context_memory.Context.empty - module Internal_for_tests = struct + module Utils = struct let default_state = let promise = let* boot = initial_state init_context "" >>= eval in @@ -398,11 +419,11 @@ module Strategies (P : TestPVM) = struct (Sc_rollup_tick_repr.of_int stop_at) in let* (starting_state, history) = - state_at history section_start_at P.Internal_for_tests.default_state + state_at history section_start_at P.Utils.default_state in let* section_start_state = P.state_hash starting_state in let* (stoping_state, history) = - state_at history section_stop_at P.Internal_for_tests.default_state + state_at history section_stop_at P.Utils.default_state in let* section_stop_state = P.state_hash stoping_state in @@ -482,10 +503,7 @@ module Strategies (P : TestPVM) = struct Sc_rollup_tick_repr.(of_int (start_at + length)) in let section_stop_at = Option.value ~default:start_at stop_at in - - let random_stop_state = - P.Internal_for_tests.(random_state length default_state) - in + let random_stop_state = P.Utils.(random_state length default_state) in let* section_stop_state = P.state_hash random_stop_state in Lwt.return Section. @@ -552,18 +570,16 @@ module Strategies (P : TestPVM) = struct in let section_start_at = section.section_start_at in let section_stop_at = section.section_stop_at in - let start_state = P.Internal_for_tests.(random_state 0 default_state) in + let start_state = P.Utils.(random_state 0 default_state) in let* section_start_state = P.state_hash start_state in let stop_state = assume_some (Sc_rollup_tick_repr.to_int section_stop_at) @@ fun section_stop_at -> assume_some (Sc_rollup_tick_repr.to_int section_start_at) @@ fun section_start_at -> - P.Internal_for_tests.( - random_state (section_stop_at - section_start_at) default_state) + P.Utils.(random_state (section_stop_at - section_start_at) default_state) in let* section_stop_state = P.state_hash stop_state in - let* next_dissection = random_dissection section in let section = { @@ -575,8 +591,7 @@ module Strategies (P : TestPVM) = struct in let conflict_resolution_step = match next_dissection with - | None -> - Conclude (None, P.Internal_for_tests.make_proof start_state stop_state) + | None -> Conclude (None, P.Utils.make_proof start_state stop_state) | Some next_dissection -> Refine {stop_state = section.section_stop_state; next_dissection} in @@ -601,10 +616,7 @@ module Strategies (P : TestPVM) = struct *) let conflicting_section history (section : Section.section) = let* (new_state, _) = - state_at - history - section.section_stop_at - P.Internal_for_tests.default_state + state_at history section.section_stop_at P.Utils.default_state in let* new_hash = P.state_hash new_state in Lwt.return @@ not (section.section_stop_state = new_hash) @@ -649,24 +661,17 @@ module Strategies (P : TestPVM) = struct state_at history (Sc_rollup_tick_repr.next section.section_start_at) - P.Internal_for_tests.default_state + P.Utils.default_state in let* (start_state, _) = - state_at - history - section.section_start_at - P.Internal_for_tests.default_state + state_at history section.section_start_at P.Utils.default_state in Lwt.return - ( Conclude - (None, P.Internal_for_tests.make_proof start_state stop_state), + ( Conclude (None, P.Utils.make_proof start_state stop_state), empty_history ) | Some next_dissection -> let* (state, history) = - state_at - history - section.section_stop_at - P.Internal_for_tests.default_state + state_at history section.section_stop_at P.Utils.default_state in let* stop_state = P.state_hash state in Lwt.return (Refine {stop_state; next_dissection}, history) @@ -728,13 +733,9 @@ module Strategies (P : TestPVM) = struct match next_dissection with | None -> let* (state, _) = - state_at - history - section_start_at - P.Internal_for_tests.default_state + state_at history section_start_at P.Utils.default_state in - Lwt.return - @@ Conclude (None, P.Internal_for_tests.make_proof state stop_state) + Lwt.return @@ Conclude (None, P.Utils.make_proof state stop_state) | Some next_dissection -> Lwt.return @@ Refine {stop_state = section_stop_state; next_dissection} @@ -806,7 +807,7 @@ module Strategies (P : TestPVM) = struct runs a game based oin the two given strategies and checks that the resulting outcome fits the expectations. *) let test_strategies committer_strategy refuter_strategy expectation = - let start_state = P.Internal_for_tests.default_state in + let start_state = P.Utils.default_state in let committer = committer_from_strategy committer_strategy in let refuter = refuter_from_strategy refuter_strategy in let outcome = @@ -934,7 +935,7 @@ let testing_arith (f : (module TestPVM) -> int option -> bool) name = let test_random_dissection (module P : TestPVM) start_at length branching = let open P in let module S = Strategies (P) in - let* section_start_state = P.state_hash @@ Internal_for_tests.default_state in + let* section_start_state = P.state_hash @@ Utils.default_state in let section_stop_at = match Sc_rollup_tick_repr.of_int (start_at + length) with | None -> assert false @@ -946,7 +947,7 @@ let test_random_dissection (module P : TestPVM) start_at length branching = | Some x -> x in let* section_stop_state = - P.state_hash @@ Internal_for_tests.(random_state length default_state) + P.state_hash @@ Utils.(random_state length default_state) in let section = S.Game.Section. -- GitLab