diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml index 67d40d068be537a18a6b394d9164ce9281e69b13..cb4f6de4ff211d9ea41f94aaa2d3c5af4e6a1192 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 @@ -168,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 @@ -206,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 @@ -707,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 () @@ -784,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 () diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli index ec7706492a3910f9a72a74d3469d8474743307c5..02af78e028b5047b36c4c4722287d2a04b501f6b 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli +++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli @@ -139,4 +139,7 @@ module type P = sig end module Make (Context : P) : - S with type context = Context.Tree.t and type state = Context.tree + S + with type context = Context.Tree.t + and type state = Context.tree + and type proof = Context.proof diff --git a/src/proto_alpha/lib_protocol/test/pbt/dune b/src/proto_alpha/lib_protocol/test/pbt/dune index 7a94c6ae263a2d1f9b86ea32eb8b06980a2b5be0..448b98a4e933f5ec68d2eb81339d4db148fca0c8 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/dune +++ b/src/proto_alpha/lib_protocol/test/pbt/dune @@ -10,13 +10,14 @@ test_tx_rollup_l2_encoding test_bitset test_sc_rollup_tick_repr - refutation_game_pbt + 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 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 77% 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 f548b4824d991a623f27960779138db3fa6b3183..acda2b5381e8c61bfdb679fa1f69d58e81c1903d 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 @@ -51,14 +51,69 @@ 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 +(** + `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) + @@ sized + @@ fix (fun self n -> + match n with + | 0 -> map (fun x -> (1, [string_of_int x])) 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)) + nat + (self (n - 1)) ); + ( 1, + map2 + (fun x (i, y) -> (i + 1, string_of_int x :: y)) + nat + (self (n - 1)) ); + ])) + +(** 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 + module type TestPVM = sig include Sc_rollup_PVM_sem.S - module Internal_for_tests : sig - val initial_state : state + module Utils : sig + (** This a post-boot state. It is used as default in many functions. *) + val default_state : state + (** [random_state n state] generates a random state. *) val random_state : int -> state -> state + (** [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 @@ -96,8 +151,8 @@ end) : TestPVM with type state = int = struct let set_input _ s = Lwt.return s - module Internal_for_tests = struct - let initial_state = P.target + module Utils = struct + let default_state = P.target let random_state _ _ = Random.bits () @@ -147,8 +202,8 @@ 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) + module Utils = struct + let default_state = ("hello", P.initial_prog) let random_state length ((_, program) : state) = let remaining_program = TzList.drop_n length program in @@ -180,6 +235,103 @@ 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 TestArith (P : sig + val inputs : string + + val evals : int +end) : TestPVM = struct + include ContextPVM + + let init_context = Tezos_context_memory.Context.empty + + module Utils = struct + let default_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 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 (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 + 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 @@ -193,19 +345,22 @@ 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 s = 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 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) @@ -213,7 +368,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' _ -> @@ -264,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.initial_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.initial_state + state_at history section_stop_at P.Utils.default_state in let* section_stop_state = P.state_hash stoping_state in @@ -348,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 initial_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. @@ -418,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 initial_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) initial_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 = { @@ -441,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 @@ -467,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.initial_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) @@ -504,7 +650,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 @@ -516,24 +661,17 @@ module Strategies (P : TestPVM) = struct state_at history (Sc_rollup_tick_repr.next section.section_start_at) - P.Internal_for_tests.initial_state + P.Utils.default_state in let* (start_state, _) = - state_at - history - section.section_start_at - P.Internal_for_tests.initial_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.initial_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) @@ -569,7 +707,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 @@ -595,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.initial_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} @@ -673,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.initial_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 = @@ -783,10 +917,25 @@ 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 (evals > 1 && evals < List.length inputs - 1) ; + f + (module TestArith (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 - let* section_start_state = P.state_hash @@ Internal_for_tests.initial_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 @@ -798,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 initial_state) + P.state_hash @@ Utils.(random_state length default_state) in let section = S.Game.Section. @@ -873,4 +1022,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"; + ] ); ]