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 82631b07af5a4fc9c4726eeded4f96108178b948..76bbf4699f437c7f1c928764c05a4f41d74b2e8d 100644
--- a/src/proto_alpha/bin_sc_rollup_node/refutation_game.ml
+++ b/src/proto_alpha/bin_sc_rollup_node/refutation_game.ml
@@ -123,8 +123,21 @@ module Make (Interpreter : Interpreter.S) :
       @@ (Sc_rollup.Proof.produce (module P) game.level
          >|= Environment.wrap_tzresult)
     in
+    let* inbox_proof_opt =
+      match r.inbox with
+      | None -> return_none
+      | Some serialized_proof -> (
+          match Sc_rollup.Inbox.of_serialized_proof serialized_proof with
+          | None -> assert false
+          | Some inbox_proof -> return_some inbox_proof)
+    in
     let+ check =
-      Sc_rollup.Proof.valid history_proof game.level ~pvm_name:game.pvm_name r
+      Sc_rollup.Proof.valid
+        history_proof
+        game.level
+        ~pvm_name:game.pvm_name
+        r
+        inbox_proof_opt
       >|= Environment.wrap_tzresult
     in
     assert check ;
diff --git a/src/proto_alpha/lib_benchmarks_proto/sc_rollup_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/sc_rollup_benchmarks.ml
index de3d0f7670b9f671462fad2218dcac8e446bd834..874590d84c883f897c46f9109bac87038fab0b3d 100644
--- a/src/proto_alpha/lib_benchmarks_proto/sc_rollup_benchmarks.ml
+++ b/src/proto_alpha/lib_benchmarks_proto/sc_rollup_benchmarks.ml
@@ -25,6 +25,9 @@
 
 open Protocol
 
+let assert_ok_lwt x =
+  match Lwt_main.run x with Ok x -> x | Error _ -> assert false
+
 (** A benchmark for estimating the gas cost of
     {!Sc_rollup_costs.Constants.cost_update_num_and_size_of_messages}. This
     value is used to consume the gas cost internally in
@@ -304,6 +307,362 @@ module Sc_rollup_add_external_messages_benchmark = struct
     Registration.register_for_codegen name (Model.For_codegen add_message_model)
 end
 
+(* A model to estimate [Sc_rollup_inbox_repr.hash_skip_list_cell]. *)
+module Sc_rollup_inbox_repr_hash_skip_list_cell = struct
+  let name = "Sc_rollup_inbox_hash_skip_list_cell"
+
+  let info = "Estimating the costs of hashing a skip list cell"
+
+  let tags = ["scoru"]
+
+  open Sc_rollup_inbox_repr.Internal_for_snoop
+  module Hash = Sc_rollup_inbox_repr.Hash
+
+  type config = {max_index : int}
+
+  let config_encoding =
+    let open Data_encoding in
+    conv
+      (fun {max_index} -> max_index)
+      (fun max_index -> {max_index})
+      (obj1 (req "max_index" int31))
+
+  let default_config = {max_index = 1_000_000}
+
+  type workload = {max_nb_backpointers : int}
+
+  let workload_encoding =
+    let open Data_encoding in
+    conv
+      (fun {max_nb_backpointers} -> max_nb_backpointers)
+      (fun max_nb_backpointers -> {max_nb_backpointers})
+      (obj1 (req "max_nb_backpointers" int31))
+
+  let workload_to_vector {max_nb_backpointers} =
+    Sparse_vec.String.of_list
+      [("max_nb_backpointers", float_of_int max_nb_backpointers)]
+
+  let hash_skip_list_cell_model =
+    Model.make
+      ~conv:(fun {max_nb_backpointers} -> (max_nb_backpointers, ()))
+      ~model:
+        (Model.affine
+           ~intercept:(Free_variable.of_string "cost_hash_skip_list_cell")
+           ~coeff:(Free_variable.of_string "cost_hash_skip_list_cell_coef"))
+
+  let models = [("scoru", hash_skip_list_cell_model)]
+
+  let benchmark rng_state conf () =
+    let skip_list_len =
+      Base_samplers.sample_in_interval
+        ~range:{min = 1; max = conf.max_index}
+        rng_state
+    in
+    let random_hash () =
+      Hash.hash_string
+        [Base_samplers.string ~size:{min = 1; max = 25} rng_state]
+    in
+    let cell =
+      let rec repeat n cell =
+        if n = 0 then cell
+        else
+          let prev_cell = cell and prev_cell_ptr = hash_skip_list_cell cell in
+          repeat
+            (n - 1)
+            (Skip_list.next ~prev_cell ~prev_cell_ptr (random_hash ()))
+      in
+      repeat skip_list_len (Skip_list.genesis (random_hash ()))
+    in
+    let max_nb_backpointers = Skip_list.number_of_back_pointers cell in
+    let workload = {max_nb_backpointers} in
+    let closure () = ignore (hash_skip_list_cell cell) in
+    Generator.Plain {workload; closure}
+
+  let create_benchmarks ~rng_state ~bench_num config =
+    List.repeat bench_num (benchmark rng_state config)
+
+  let () =
+    Registration.register_for_codegen
+      name
+      (Model.For_codegen hash_skip_list_cell_model)
+end
+
+(* A model to estimate [Skip_list_valid_back_path ~equal_ptr:Hash.equal]
+   as used in [Sc_rollup_inbox_repr]. *)
+module Skip_list_valid_back_path_hash_equal = struct
+  let name = "Skip_list_valid_back_path_hash_equal"
+
+  let info =
+    "Estimating the costs of validating a path in a merkelized skip list"
+
+  let tags = ["scoru"]
+
+  open Sc_rollup_inbox_repr.Internal_for_snoop
+  module Hash = Sc_rollup_inbox_repr.Hash
+
+  type config = {max_index : int}
+
+  let config_encoding =
+    let open Data_encoding in
+    conv
+      (fun {max_index} -> max_index)
+      (fun max_index -> {max_index})
+      (obj1 (req "max_index" int31))
+
+  let default_config = {max_index = 18}
+
+  type workload = {path_len : int}
+
+  let workload_encoding =
+    let open Data_encoding in
+    conv
+      (fun {path_len} -> path_len)
+      (fun path_len -> {path_len})
+      (obj1 (req "path_len" int31))
+
+  let workload_to_vector {path_len} =
+    Sparse_vec.String.of_list [("path_len", float_of_int path_len)]
+
+  let skip_list_valid_back_path_hash_equal_model =
+    Model.make
+      ~conv:(fun {path_len; _} -> (path_len, ()))
+      ~model:
+        (Model.nlogn
+           ~intercept:
+             (Free_variable.of_string
+                "cost_skip_list_valid_back_path_hash_equal")
+           ~coeff:
+             (Free_variable.of_string
+                "cost_skip_list_valid_back_path_hash_equal_coeff"))
+
+  let models = [("scoru", skip_list_valid_back_path_hash_equal_model)]
+
+  let benchmark rng_state conf () =
+    let skip_list_len =
+      1
+      lsl Base_samplers.sample_in_interval
+            ~range:{min = 1; max = conf.max_index}
+            rng_state
+      - 1
+    in
+    let random_hash () =
+      Hash.hash_string
+        [Base_samplers.string ~size:{min = 1; max = 25} rng_state]
+    in
+    let genesis_cell = Skip_list.genesis (random_hash ()) in
+    let cell, map =
+      let rec repeat n (cell, map) =
+        if n = 0 then (cell, map)
+        else
+          let prev_cell = cell and prev_cell_ptr = hash_skip_list_cell cell in
+          let map = (prev_cell_ptr, prev_cell) :: map in
+          let cell =
+            Skip_list.next ~prev_cell ~prev_cell_ptr (random_hash ())
+          in
+          repeat (n - 1) (cell, map)
+      in
+      repeat skip_list_len (genesis_cell, [])
+    in
+    let cell_ptr = hash_skip_list_cell cell in
+    let deref_of_map map =
+      let map = Hash.Map.of_seq (List.to_seq @@ ((cell_ptr, cell) :: map)) in
+      fun k -> Hash.Map.find k map
+    in
+    let deref = deref_of_map map in
+    let target_index = 0 in
+    let equal_ptr = Hash.equal in
+    let target_ptr = hash_skip_list_cell genesis_cell in
+    let path_opt = Skip_list.back_path ~deref ~cell_ptr ~target_index in
+    let path =
+      match path_opt with
+      | None ->
+          (* Absurd by construction of [cell]. *)
+          assert false
+      | Some path -> path
+    in
+    let deref =
+      deref_of_map
+      @@ List.map
+           (fun h ->
+             match deref h with
+             | None ->
+                 (* Impossible because the path is taken in the reachable cells from [deref]. *)
+                 assert false
+             | Some c -> (h, c))
+           path
+    in
+    let workload = {path_len = 1 + List.length path} in
+    let closure () =
+      let open Skip_list in
+      ignore (valid_back_path ~equal_ptr ~deref ~cell_ptr ~target_ptr path)
+    in
+    Generator.Plain {workload; closure}
+
+  let create_benchmarks ~rng_state ~bench_num config =
+    List.repeat bench_num (benchmark rng_state config)
+
+  let () =
+    Registration.register_for_codegen
+      name
+      (Model.For_codegen skip_list_valid_back_path_hash_equal_model)
+end
+
+(* A model to estimate [verify_proof_about_payload_and_level] as used
+   in [Sc_rollup_inbox_repr]. *)
+module Sc_rollup_verify_proof_about_payload_and_level = struct
+  let name = "Sc_rollup_verify_proof_about_payload_and_level"
+
+  let info =
+    "Estimating the costs of verifying a proof about level tree contents"
+
+  let tags = ["scoru"]
+
+  module Hash = Sc_rollup_inbox_repr.Hash
+
+  module Tree = struct
+    open Tezos_context_memory.Context
+
+    type nonrec t = t
+
+    type nonrec tree = tree
+
+    module Tree = struct
+      include Tezos_context_memory.Context.Tree
+
+      type nonrec t = t
+
+      type nonrec tree = tree
+
+      type key = string list
+
+      type value = bytes
+    end
+
+    let commit_tree context key tree =
+      let open Lwt_syntax in
+      let* ctxt = Tezos_context_memory.Context.add_tree context key tree in
+      let* _ = commit ~time:Time.Protocol.epoch ~message:"" ctxt in
+      return ()
+
+    let lookup_tree context hash =
+      let open Lwt_syntax in
+      let* _, tree =
+        produce_tree_proof
+          (index context)
+          (`Node (Hash.to_context_hash hash))
+          (fun x -> Lwt.return (x, x))
+      in
+      return (Some 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 tree f =
+      let open Lwt_syntax in
+      let* proof =
+        produce_tree_proof (index context) (`Node (Tree.hash tree)) f
+      in
+      return (Some proof)
+
+    let kinded_hash_to_inbox_hash = function
+      | `Value hash | `Node hash -> Hash.of_context_hash hash
+
+    let proof_before proof = kinded_hash_to_inbox_hash proof.Proof.before
+
+    let proof_encoding =
+      Tezos_context_merkle_proof_encoding.Merkle_proof_encoding.V2.Tree32
+      .tree_proof_encoding
+  end
+
+  module Op = Sc_rollup_inbox_repr.Make_hashing_scheme (Tree)
+  open Op.Internal_MerkelizedOperations_for_snoop
+
+  type config = {max_number_of_messages : int}
+
+  let config_encoding =
+    let open Data_encoding in
+    conv
+      (fun {max_number_of_messages} -> max_number_of_messages)
+      (fun max_number_of_messages -> {max_number_of_messages})
+      (obj1 (req "max_number_of_messages" int31))
+
+  let default_config = {max_number_of_messages = (1 lsl 16) - 1}
+
+  type workload = {number_of_messages : int; proof : Op.P.proof; index : Z.t}
+
+  let workload_encoding =
+    let open Data_encoding in
+    conv
+      (fun {number_of_messages; proof; index} ->
+        (number_of_messages, proof, index))
+      (fun (number_of_messages, proof, index) ->
+        {number_of_messages; proof; index})
+      (obj3
+         (req "number_of_messages" int31)
+         (req "proof" Op.P.proof_encoding)
+         (req "index" Data_encoding.z))
+
+  let workload_to_vector {number_of_messages; proof = _; index = _} =
+    Sparse_vec.String.of_list
+      [("number_of_messages", float_of_int number_of_messages)]
+
+  let verify_proof_about_payload_and_level_model =
+    Model.make
+      ~conv:(fun {number_of_messages; _} -> (number_of_messages, ()))
+      ~model:
+        (Model.logn
+         (* ~intercept:
+          *   (Free_variable.of_string
+          *      "cost_verify_proof_about_payload_and_level") *)
+           ~coeff:
+             (Free_variable.of_string
+                "cost_verify_proof_about_payload_and_level_coeff"))
+
+  let models = [("scoru", verify_proof_about_payload_and_level_model)]
+
+  let benchmark rng_state conf () =
+    let number_of_messages =
+      Base_samplers.sample_in_interval
+        ~range:{min = 1; max = conf.max_number_of_messages}
+        rng_state
+    in
+    let ctxt =
+      let open Lwt_syntax in
+      Lwt_main.run
+      @@ let* index = Tezos_context_memory.Context.init "foo" in
+         return @@ Tezos_context_memory.Context.empty index
+    in
+    let index =
+      Z.of_int
+        (Base_samplers.sample_in_interval
+           ~range:{min = 0; max = number_of_messages - 1}
+           rng_state)
+    in
+    let proof =
+      Lwt_main.run
+      @@ produce_proof_about_payload_and_level ctxt number_of_messages index
+      |> function
+      | None -> assert false
+      | Some proof -> proof
+    in
+    let workload = {number_of_messages; proof; index} in
+    let closure () =
+      Lwt_main.run @@ verify_proof_about_payload_and_level proof index
+      |> fun b -> assert b
+    in
+    Generator.Plain {workload; closure}
+
+  let create_benchmarks ~rng_state ~bench_num config =
+    List.repeat bench_num (benchmark rng_state config)
+
+  let () =
+    Registration.register_for_codegen
+      name
+      (Model.For_codegen verify_proof_about_payload_and_level_model)
+end
+
 let () =
   Registration_helpers.register
     (module Sc_rollup_add_external_messages_benchmark)
@@ -311,3 +670,14 @@ let () =
 let () =
   Registration_helpers.register
     (module Sc_rollup_update_num_and_size_of_messages_benchmark)
+
+let () =
+  Registration_helpers.register
+    (module Sc_rollup_inbox_repr_hash_skip_list_cell)
+
+let () =
+  Registration_helpers.register (module Skip_list_valid_back_path_hash_equal)
+
+let () =
+  Registration_helpers.register
+    (module Sc_rollup_verify_proof_about_payload_and_level)
diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli
index 64e2726632d2f2fa424b9a59441870a9d9b6fc18..ac979204bc1cce831472a0094ea5c3f0ae8d4e1a 100644
--- a/src/proto_alpha/lib_protocol/alpha_context.mli
+++ b/src/proto_alpha/lib_protocol/alpha_context.mli
@@ -2948,6 +2948,34 @@ module Sc_rollup : sig
 
     val serialized_proof_encoding : serialized_proof Data_encoding.t
 
+    module type P = sig
+      module Tree :
+        Context.TREE with type key = string list and type value = bytes
+
+      type t = Tree.t
+
+      type tree = Tree.tree
+
+      val commit_tree : t -> string list -> tree -> unit Lwt.t
+
+      val lookup_tree : t -> Hash.t -> tree option Lwt.t
+
+      type proof
+
+      val proof_encoding : proof Data_encoding.t
+
+      val proof_before : proof -> Hash.t
+
+      val verify_proof :
+        proof -> (tree -> (tree * 'a) Lwt.t) -> (tree * 'a) option Lwt.t
+
+      val produce_proof :
+        Tree.t ->
+        tree ->
+        (tree -> (tree * 'a) Lwt.t) ->
+        (proof * 'a) option Lwt.t
+    end
+
     module type Merkelized_operations = sig
       type tree
 
@@ -3005,12 +3033,17 @@ module Sc_rollup : sig
 
       val of_serialized_proof : serialized_proof -> proof option
 
+      val cost_of_serialized_proof : serialized_proof -> Gas.cost
+
       val verify_proof :
         Raw_level.t * Z.t ->
         history_proof ->
         proof ->
         Sc_rollup_PVM_sem.input option tzresult Lwt.t
 
+      val cost_verify_proof :
+        Raw_level_repr.t * Z.t -> history_proof -> proof -> Gas.cost
+
       val produce_proof :
         inbox_context ->
         History.t ->
@@ -3020,7 +3053,15 @@ module Sc_rollup : sig
 
       val empty : inbox_context -> Sc_rollup_repr.t -> Raw_level.t -> t Lwt.t
 
-      (*xx*)
+      module P : P
+
+      module Internal_MerkelizedOperations_for_snoop : sig
+        val produce_proof_about_payload_and_level :
+          inbox_context -> int -> Z.t -> P.proof option Lwt.t
+
+        val verify_proof_about_payload_and_level : P.proof -> Z.t -> bool Lwt.t
+      end
+
       module Internal_for_tests : sig
         val eq_tree : tree -> tree -> bool
 
@@ -3037,34 +3078,6 @@ module Sc_rollup : sig
         with type tree = Context.tree
          and type inbox_context = Context.t
 
-    module type P = sig
-      module Tree :
-        Context.TREE with type key = string list and type value = bytes
-
-      type t = Tree.t
-
-      type tree = Tree.tree
-
-      val commit_tree : t -> string list -> tree -> unit Lwt.t
-
-      val lookup_tree : t -> Hash.t -> tree option Lwt.t
-
-      type proof
-
-      val proof_encoding : proof Data_encoding.t
-
-      val proof_before : proof -> Hash.t
-
-      val verify_proof :
-        proof -> (tree -> (tree * 'a) Lwt.t) -> (tree * 'a) option Lwt.t
-
-      val produce_proof :
-        Tree.t ->
-        tree ->
-        (tree -> (tree * 'a) Lwt.t) ->
-        (proof * 'a) option Lwt.t
-    end
-
     module Make_hashing_scheme (P : P) :
       Merkelized_operations with type tree = P.tree and type inbox_context = P.t
 
@@ -3181,6 +3194,8 @@ module Sc_rollup : sig
 
       val verify_proof : proof -> bool Lwt.t
 
+      val cost_verify_proof : proof -> Gas.cost
+
       val produce_proof :
         context -> input option -> state -> (proof, error) result Lwt.t
 
@@ -3445,6 +3460,7 @@ module Sc_rollup : sig
       Raw_level.t ->
       pvm_name:string ->
       t ->
+      Inbox.proof option ->
       bool tzresult Lwt.t
 
     val produce :
@@ -3554,7 +3570,11 @@ module Sc_rollup : sig
       default_number_of_sections:int ->
       t
 
-    val play : t -> refutation -> (outcome, t) Either.t Lwt.t
+    val play :
+      context ->
+      t ->
+      refutation ->
+      ((outcome, t) Either.t * context) tzresult Lwt.t
 
     type timeout = {alice : int; bob : int; last_turn_level : Raw_level_repr.t}
 
diff --git a/src/proto_alpha/lib_protocol/saturation_repr.ml b/src/proto_alpha/lib_protocol/saturation_repr.ml
index 4494c9c45ef50d0aba7d5c88835ba881d68042dd..9e28c4f9c2ac8d55a7f7810919581d3e61d45680 100644
--- a/src/proto_alpha/lib_protocol/saturation_repr.ml
+++ b/src/proto_alpha/lib_protocol/saturation_repr.ml
@@ -173,3 +173,13 @@ let z_encoding = Data_encoding.(check_size 9 (conv to_z t_to_z_exn z))
 let n_encoding = Data_encoding.(check_size 9 (conv to_z t_to_z_exn n))
 
 let pp fmt x = Format.pp_print_int fmt x
+
+module Syntax = struct
+  let ( + ) = add
+
+  let ( * ) = mul
+
+  let ( - ) = sub
+
+  let ( / ) = ediv
+end
diff --git a/src/proto_alpha/lib_protocol/saturation_repr.mli b/src/proto_alpha/lib_protocol/saturation_repr.mli
index b95399d5f4faf2fe4332667296d176b5b9f09468..5a0a58966955b5d892a85a5ead27df8216cd9a5a 100644
--- a/src/proto_alpha/lib_protocol/saturation_repr.mli
+++ b/src/proto_alpha/lib_protocol/saturation_repr.mli
@@ -205,3 +205,13 @@ val n_encoding : _ t Data_encoding.t
 
 (** A pretty-printer for native integers. *)
 val pp : Format.formatter -> _ t -> unit
+
+module Syntax : sig
+  val ( + ) : _ t -> _ t -> may_saturate t
+
+  val ( * ) : _ t -> _ t -> may_saturate t
+
+  val ( - ) : 'a t -> _ t -> 'a t
+
+  val ( / ) : 'a t -> _ t -> 'a t
+end
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml
index cc6a37cfacb6dbd07b361ba3f09b23bd87dd3962..221cc0aed40755714ec12ee6758f1cb7a8279201 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml
@@ -54,6 +54,13 @@ let input_equal (a : input) (b : input) : bool =
   && Z.equal message_counter b.message_counter
   && String.equal (payload :> string) (b.payload :> string)
 
+let input_size_in_bytes a =
+  let payload_size_in_bytes = String.length (a.payload :> string) in
+  8 + ((7 + Z.numbits a.message_counter) / 8) + payload_size_in_bytes
+
+let cost_input_equal (a : input) (b : input) : Gas_limit_repr.cost =
+  Sc_rollup_costs.cost_compare (input_size_in_bytes a) (input_size_in_bytes b)
+
 type input_request =
   | No_input_required
   | Initial
@@ -176,6 +183,8 @@ module type S = sig
 
   val verify_proof : proof -> bool Lwt.t
 
+  val cost_verify_proof : proof -> Gas_limit_repr.cost
+
   val produce_proof :
     context -> input option -> state -> (proof, error) result Lwt.t
 
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.mli b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.mli
index 98fa6552ddd71b15eead25c9b136b54685a13d38..238032baf9ec6951aadeab8e5789c7abd3a77e63 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.mli
@@ -62,6 +62,8 @@ val input_encoding : input Data_encoding.t
 (** [input_equal i1 i2] return whether [i1] and [i2] are equal. *)
 val input_equal : input -> input -> bool
 
+val cost_input_equal : input -> input -> Gas_limit_repr.cost
+
 (** The PVM's current input expectations:
     - [No_input_required] if the machine is busy and has no need for new input.
 
@@ -233,6 +235,8 @@ module type S = sig
       type. *)
   val verify_proof : proof -> bool Lwt.t
 
+  val cost_verify_proof : proof -> Gas_limit_repr.cost
+
   (** [produce_proof ctxt input_given state] should return a [proof] for
       the PVM step starting from [state], if possible. This may fail for
       a few reasons:
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml
index 36a9ea2d5fd6ad7276bb8d8c45e4d42e10753c0e..1051af0d38d82afe8626ac2a3360c109638ba134 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml
@@ -1103,6 +1103,11 @@ module Make (Context : P) :
     | Some (_, request) ->
         return (PS.input_request_equal request proof.requested)
 
+  let cost_verify_proof _proof =
+    let open Gas_limit_repr in
+    (* FIXME: To be defined by forthcoming commits. *)
+    free
+
   type error += Arith_proof_production_failed
 
   let produce_proof context input_given state =
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_costs.ml b/src/proto_alpha/lib_protocol/sc_rollup_costs.ml
index 5ff7a524d3b82cbba820c7055e559e03cd8a4fb5..7ec2085c81e7c1cdf0796693601c658ee58a57a1 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_costs.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_costs.ml
@@ -135,3 +135,20 @@ let cost_hash_bytes ~bytes_len =
   let open S_syntax in
   let v0 = S.safe_int bytes_len in
   S.safe_int 430 + v0 + (v0 lsr 3)
+
+let cost_compare a_size_in_bytes b_size_in_bytes =
+  let open S_syntax in
+  let size_in_bytes = Compare.Int.min a_size_in_bytes b_size_in_bytes in
+  let v0 = S.safe_int size_in_bytes in
+  S.safe_int 35 + ((v0 lsr 6) + (v0 lsr 7))
+
+let search_in_tick_list len tick_size =
+  S_syntax.(S.safe_int len * cost_compare tick_size tick_size)
+
+let cost_find_choice ~number_of_sections ~tick_size =
+  search_in_tick_list number_of_sections tick_size
+
+let cost_check_dissection ~number_of_states ~tick_size ~hash_size =
+  let open S_syntax in
+  search_in_tick_list number_of_states tick_size
+  + (S.safe_int 2 * cost_compare hash_size hash_size)
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_costs.mli b/src/proto_alpha/lib_protocol/sc_rollup_costs.mli
index 5b47cc667a711f63cfe7ec33be85c8e216edfffa..c10f9b0e1a12ec42bbadbd09b0bbc563a34ca341 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_costs.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_costs.mli
@@ -80,3 +80,22 @@ val cost_serialize_external_inbox_message : bytes_len:int -> Gas_limit_repr.cost
 
 (** [cost_hash_bytes ~bytes_len] is the cost of hashing [bytes_len] bytes. *)
 val cost_hash_bytes : bytes_len:int -> Gas_limit_repr.cost
+
+(** [cost_check_dissection ~number_of_states ~tick_size ~hash_size] is
+   the cost of checking that a dissection with a given
+   [number_of_states] used in a refutation game is well-formed. This
+   includes the comparison of a linear number of ticks as well as the
+   verification of two hashes of given [hash_size]. *)
+val cost_check_dissection :
+  number_of_states:int -> tick_size:int -> hash_size:int -> Gas_limit_repr.cost
+
+(** [cost_find_choice ~number_of_sections ~tick_size ~hash_size] is
+    the cost of searching for a tick of a give [tick_size] within a
+    given [number_of_sections]. *)
+val cost_find_choice :
+  number_of_sections:int -> tick_size:int -> Gas_limit_repr.cost
+
+(** [cost_compare a_size_in_bytes b_size_in_bytes] returns the gas
+    cost of comparing two values given their respective sizes [a_size_in_bytes]
+    and [b_size_in_bytes]. *)
+val cost_compare : int -> int -> Gas_limit_repr.cost
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 dcaca8ad3e5a841ee56b681f8f5082db0db162a7..90b7f66c3657d616c41843ada6e16e01ff9923d0 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml
@@ -825,7 +825,11 @@ let check_proof_start_stop ~start_chunk ~stop_chunk proof =
     (Proof_stop_state_hash_mismatch
        {stop_state_hash = stop_chunk.state_hash; stop_proof})
 
-let play game refutation =
+let wrap_reason game = function
+  | Ok x -> Lwt.return x
+  | Error reason -> Lwt.return @@ Either.Left {loser = game.turn; reason}
+
+let play_aux game refutation inbox_proof_opt =
   let open Lwt_result_syntax in
   let*! result =
     let* start_chunk, stop_chunk = find_choice game refutation.choice in
@@ -852,7 +856,12 @@ let play game refutation =
         let* () = check_proof_start_stop ~start_chunk ~stop_chunk proof in
         let {inbox_snapshot; level; pvm_name; _} = game in
         let*! (proof_valid_tzresult : bool tzresult) =
-          Sc_rollup_proof_repr.valid inbox_snapshot level ~pvm_name proof
+          Sc_rollup_proof_repr.valid
+            inbox_snapshot
+            level
+            ~pvm_name
+            proof
+            inbox_proof_opt
         in
         let* () =
           match proof_valid_tzresult with
@@ -864,9 +873,68 @@ let play game refutation =
         return
           (Either.Left {loser = opponent game.turn; reason = Conflict_resolved})
   in
-  match result with
-  | Ok x -> Lwt.return x
-  | Error reason -> Lwt.return @@ Either.Left {loser = game.turn; reason}
+  wrap_reason game result
+
+(* Cost of checking the start and stop hashes of a proof. *)
+let cost_check_proof_start_stop =
+  let size = State_hash.size in
+  Saturation_repr.(mul (safe_int 2) (Sc_rollup_costs.cost_compare size size))
+
+let cost_play game refutation inbox_proof_opt =
+  let open Gas_limit_repr in
+  (* The gas cost is defined over the structure of [play]. *)
+  let number_of_sections = List.length game.dissection in
+  let tick_size = Sc_rollup_tick_repr.size_in_bytes refutation.choice in
+  Sc_rollup_costs.cost_find_choice ~number_of_sections ~tick_size
+  +@
+  match refutation.step with
+  | Dissection states ->
+      let number_of_states = List.length states in
+      let hash_size = State_hash.size in
+      Sc_rollup_costs.cost_check_dissection
+        ~number_of_states
+        ~tick_size
+        ~hash_size
+  | Proof proof ->
+      let {inbox_snapshot; level; pvm_name; _} = game in
+      cost_check_proof_start_stop
+      +@ Sc_rollup_proof_repr.cost_valid
+           inbox_snapshot
+           level
+           ~pvm_name
+           proof
+           inbox_proof_opt
+
+let play ctxt game refutation =
+  let open Lwt_tzresult_syntax in
+  let* inbox_proof_opt, ctxt =
+    match refutation.step with
+    | Proof proof -> (
+        match proof.inbox with
+        | None -> return @@ (Either.Left None, ctxt)
+        | Some p -> (
+            let*? ctxt =
+              Raw_context.consume_gas
+                ctxt
+                (Sc_rollup_inbox_repr.cost_of_serialized_proof p)
+            in
+            match Sc_rollup_inbox_repr.of_serialized_proof p with
+            | None ->
+                return
+                @@ ( Either.Right
+                       (Invalid_move (Proof_invalid "unreadable proof")),
+                     ctxt )
+            | Some p -> return @@ (Either.Left (Some p), ctxt)))
+    | Dissection _ -> return @@ (Either.Left None, ctxt)
+  in
+  match inbox_proof_opt with
+  | Either.Left inbox_proof_opt ->
+      let*? ctxt =
+        Raw_context.consume_gas ctxt (cost_play game refutation inbox_proof_opt)
+      in
+      let*! result = play_aux game refutation inbox_proof_opt in
+      return (result, ctxt)
+  | Either.Right reason -> return (Either.Left {loser = game.turn; reason}, ctxt)
 
 module Internal_for_tests = struct
   let find_choice = find_choice
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 e661acdab27ba6b3207749287bb6491ddfdd4fcc..5e4186a457879c605e6b851cb46c1707219aa19a 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli
@@ -374,7 +374,11 @@ val outcome_encoding : outcome Data_encoding.t
     In the case of the game continuing, this swaps the current
     player and updates the [dissection]. In the case of a [Proof]
     being provided this returns an [outcome]. *)
-val play : t -> refutation -> (outcome, t) Either.t Lwt.t
+val play :
+  Raw_context.t ->
+  t ->
+  refutation ->
+  ((outcome, t) Either.t * Raw_context.t) tzresult Lwt.t
 
 (** A type that represents the number of blocks left for players to play. Each
     player has her timeout value. `timeout` is expressed in the number of
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml
index 6c89524a2d2fe0078869aec20c66023b4fcab6e1..70b0a370e83effbd46de4d62e9185c040538d616 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml
@@ -142,11 +142,28 @@ let hash_skip_list_cell cell =
   :: List.map Hash.to_bytes back_pointers_hashes
   |> Hash.hash_bytes
 
+let cost_hash_skip_list_cell cell =
+  (* From model Sc_rollup_inbox_hash_skip_list_cell. *)
+  let open Saturation_repr in
+  let nb_backpointers = Skip_list.number_of_back_pointers cell in
+  Syntax.((safe_int 31 * safe_int nb_backpointers) + safe_int 725)
+
 module V1 = struct
   type history_proof = (Hash.t, Hash.t) Skip_list.cell
 
   let equal_history_proof = Skip_list.equal Hash.equal Hash.equal
 
+  let cost_hash_equal = Sc_rollup_costs.cost_compare Hash.size Hash.size
+
+  let cost_equal_history_proof h1 h2 =
+    let n1 = Skip_list.number_of_back_pointers h1
+    and n2 = Skip_list.number_of_back_pointers h2 in
+    if Compare.Int.(n1 = n2) then
+      let n = Compare.Int.(min n1 n2) in
+      Saturation_repr.(
+        Syntax.(safe_int n * (cost_hash_equal + cost_hash_equal)))
+    else Gas_limit_repr.free
+
   let history_proof_encoding : history_proof Data_encoding.t =
     Skip_list.encoding Hash.encoding Hash.encoding
 
@@ -360,6 +377,12 @@ module V1 = struct
         = 0l) ;
       start_new_commitment_period inbox new_starting_level)
     else inbox
+
+  module Internal_for_snoop = struct
+    module Skip_list = Skip_list
+
+    let hash_skip_list_cell = hash_skip_list_cell
+  end
 end
 
 type versioned = V1 of V1.t
@@ -391,6 +414,30 @@ type serialized_proof = bytes
 
 let serialized_proof_encoding = Data_encoding.bytes
 
+module type P = sig
+  module Tree : Context.TREE with type key = string list and type value = bytes
+
+  type t = Tree.t
+
+  type tree = Tree.tree
+
+  val commit_tree : Tree.t -> string list -> Tree.tree -> unit Lwt.t
+
+  val lookup_tree : Tree.t -> Hash.t -> tree option Lwt.t
+
+  type proof
+
+  val proof_encoding : proof Data_encoding.t
+
+  val proof_before : proof -> Hash.t
+
+  val verify_proof :
+    proof -> (tree -> (tree * 'a) Lwt.t) -> (tree * 'a) option Lwt.t
+
+  val produce_proof :
+    Tree.t -> tree -> (tree -> (tree * 'a) Lwt.t) -> (proof * 'a) option Lwt.t
+end
+
 module type Merkelized_operations = sig
   type inbox_context
 
@@ -448,12 +495,17 @@ module type Merkelized_operations = sig
 
   val of_serialized_proof : serialized_proof -> proof option
 
+  val cost_of_serialized_proof : serialized_proof -> Gas_limit_repr.cost
+
   val verify_proof :
     Raw_level_repr.t * Z.t ->
     history_proof ->
     proof ->
     Sc_rollup_PVM_sem.input option tzresult Lwt.t
 
+  val cost_verify_proof :
+    Raw_level_repr.t * Z.t -> history_proof -> proof -> Gas_limit_repr.cost
+
   val produce_proof :
     inbox_context ->
     History.t ->
@@ -463,6 +515,15 @@ module type Merkelized_operations = sig
 
   val empty : inbox_context -> Sc_rollup_repr.t -> Raw_level_repr.t -> t Lwt.t
 
+  module P : P
+
+  module Internal_MerkelizedOperations_for_snoop : sig
+    val produce_proof_about_payload_and_level :
+      inbox_context -> int -> Z.t -> P.proof option Lwt.t
+
+    val verify_proof_about_payload_and_level : P.proof -> Z.t -> bool Lwt.t
+  end
+
   module Internal_for_tests : sig
     val eq_tree : tree -> tree -> bool
 
@@ -474,33 +535,11 @@ module type Merkelized_operations = sig
   end
 end
 
-module type P = sig
-  module Tree : Context.TREE with type key = string list and type value = bytes
-
-  type t = Tree.t
-
-  type tree = Tree.tree
-
-  val commit_tree : Tree.t -> string list -> Tree.tree -> unit Lwt.t
-
-  val lookup_tree : Tree.t -> Hash.t -> tree option Lwt.t
-
-  type proof
-
-  val proof_encoding : proof Data_encoding.t
-
-  val proof_before : proof -> Hash.t
-
-  val verify_proof :
-    proof -> (tree -> (tree * 'a) Lwt.t) -> (tree * 'a) option Lwt.t
-
-  val produce_proof :
-    Tree.t -> tree -> (tree -> (tree * 'a) Lwt.t) -> (proof * 'a) option Lwt.t
-end
-
 module Make_hashing_scheme (P : P) :
-  Merkelized_operations with type tree = P.tree and type inbox_context = P.t =
-struct
+  Merkelized_operations
+    with type tree = P.tree
+     and type inbox_context = P.t
+     and module P = P = struct
   module Tree = P.Tree
 
   type inbox_context = P.t
@@ -529,16 +568,19 @@ struct
     let tree = Tree.empty ctxt in
     set_level tree level
 
+  let add_message_in_level_tree level_tree message_index payload =
+    Tree.add
+      level_tree
+      (key_of_message message_index)
+      (Bytes.of_string
+         (payload : Sc_rollup_inbox_message_repr.serialized :> string))
+
   let add_message inbox payload level_tree =
     let open Lwt_tzresult_syntax in
     let message_index = inbox.message_counter in
     let message_counter = Z.succ message_index in
     let*! level_tree =
-      Tree.add
-        level_tree
-        (key_of_message message_index)
-        (Bytes.of_string
-           (payload : Sc_rollup_inbox_message_repr.serialized :> string))
+      add_message_in_level_tree level_tree message_index payload
     in
     let nb_messages_in_commitment_period =
       Int64.succ inbox.nb_messages_in_commitment_period
@@ -717,6 +759,34 @@ struct
       ~target_ptr
       path
 
+  let cost_valid_back_path proof_len _max_nb_backpointers =
+    (* The following cost function comes from snoop's
+       [model_Skip_list_valid_back_path_hash_equal]. *)
+    let open Saturation_repr in
+    let size = safe_int proof_len in
+    Syntax.(safe_int 30 * (size * (safe_int @@ numbits (safe_int 1 + size))))
+
+  let cost_verify_inclusion_proof proof a b =
+    let open Saturation_repr in
+    let open Syntax in
+    (* This function is defined over the structure of [verify_inclusion_proof]. *)
+    let cost_hash_skip_list_cells =
+      cost_hash_skip_list_cell a + cost_hash_skip_list_cell b
+      + List.fold_left
+          (fun accu c -> accu + cost_hash_skip_list_cell c)
+          (safe_int 0)
+          proof
+    in
+    let max_nb_backpointers =
+      List.fold_left
+        (fun accu c ->
+          Compare.Int.max accu (Skip_list.number_of_back_pointers c))
+        0
+        proof
+    in
+    cost_hash_skip_list_cells
+    + cost_valid_back_path (List.length proof) max_nb_backpointers
+
   type proof =
     (* See the main docstring for this type (in the mli file) for
        definitions of the three proof parameters [starting_point],
@@ -865,6 +935,11 @@ struct
 
   let of_serialized_proof = Data_encoding.Binary.of_bytes_opt proof_encoding
 
+  let cost_of_serialized_proof p =
+    let blen = Bytes.length p in
+    (* The following model is copied from {!Michelson_v1_gas.Cost_of.unpack}. *)
+    Saturation_repr.(Syntax.(safe_int 260 + safe_int (blen lsr 3)))
+
   let to_serialized_proof = Data_encoding.Binary.to_bytes_exn proof_encoding
 
   let proof_error reason =
@@ -900,6 +975,18 @@ struct
               && Hash.equal p (hash_skip_list_cell lower)))
       "invalid inclusions"
 
+  let cost_check_inclusions proof snapshot =
+    let open Gas_limit_repr in
+    (* This function is defined over the structure of [check_inclusions]. *)
+    match proof with
+    | Single_level {inc; level; _} ->
+        cost_verify_inclusion_proof inc level snapshot
+    | Level_crossing {inc; lower = _; upper; _} -> (
+        let prev_cell = Skip_list.back_pointer upper 0 in
+        match prev_cell with
+        | None -> free
+        | Some _p -> cost_verify_inclusion_proof inc upper snapshot)
+
   (** To construct or verify a tree proof we need a function of type
 
       [tree -> (tree, result) Lwt.t]
@@ -924,6 +1011,14 @@ struct
     let* level = find_level tree in
     return (tree, (payload, level))
 
+  let verify_proof_about_payload_and_level message_proof n =
+    P.verify_proof message_proof (payload_and_level n)
+
+  let cost_verify_about_payload_and_level _message_proof _n =
+    let open Gas_limit_repr in
+    (* FIXME: This function will be defined by forthcoming commits. *)
+    free
+
   (** Utility function that handles all the verification needed for a
       particular message proof at a particular level. It calls
       [P.verify_proof], but also checks the proof has the correct
@@ -936,7 +1031,7 @@ struct
         (Hash.equal level_hash (P.proof_before message_proof))
         (Format.sprintf "message_proof (%s) does not match history" label)
     in
-    let*! result = P.verify_proof message_proof (payload_and_level n) in
+    let*! result = verify_proof_about_payload_and_level message_proof n in
     match result with
     | None -> proof_error (Format.sprintf "message_proof is invalid (%s)" label)
     | Some (_, (_, None)) ->
@@ -950,6 +1045,13 @@ struct
         in
         return payload_opt
 
+  let cost_check_message_proof message_proof _level_hash (_l, n) =
+    (* This function is defined over the structure of [check_message_proof]. *)
+    let open Saturation_repr in
+    let open Syntax in
+    (safe_int 2 * cost_hash_equal)
+    + cost_verify_about_payload_and_level message_proof n
+
   let verify_proof (l, n) snapshot proof =
     assert (Z.(geq n zero)) ;
     let open Lwt_tzresult_syntax in
@@ -1005,6 +1107,28 @@ struct
                      payload;
                    })
 
+  let cost_verify_proof (l, n) snapshot proof =
+    let open Saturation_repr.Syntax in
+    (* This function is defined over the structure of [verify_proof]. *)
+    let cost_message_proof_verification =
+      match proof with
+      | Single_level p ->
+          let level_hash = Skip_list.content p.level in
+          cost_check_message_proof p.message_proof level_hash (l, n)
+          + cost_equal_history_proof snapshot p.level
+      | Level_crossing p ->
+          let lower_level_hash = Skip_list.content p.lower in
+          let upper_level_hash = Skip_list.content p.upper in
+          cost_check_message_proof p.lower_message_proof lower_level_hash (l, n)
+          + cost_check_message_proof
+              p.upper_message_proof
+              upper_level_hash
+              (p.upper_level, Z.zero)
+          + cost_equal_history_proof snapshot p.upper
+    in
+
+    cost_check_inclusions proof snapshot + cost_message_proof_verification
+
   (** Utility function; we convert all our calls to be consistent with
       [Lwt_tzresult_syntax]. *)
   let option_to_result e lwt_opt =
@@ -1134,6 +1258,47 @@ struct
         old_levels_messages = Skip_list.genesis initial_hash;
       }
 
+  module P = P
+
+  module Internal_MerkelizedOperations_for_snoop = struct
+    (* The size of the proof depends on the [number_of_messages]
+       pushed in the level tree. *)
+    let produce_proof_about_payload_and_level ctxt number_of_messages pn =
+      let open Lwt_syntax in
+      let payload =
+        let open Sc_rollup_inbox_message_repr in
+        (* FIXME: The size of the payload may count! *)
+        let serialized = serialize (External "Some payload") in
+        match serialized with
+        | Ok s -> s
+        | Error _ ->
+            (* By construction of serialized. *)
+            assert false
+      in
+      let* tree =
+        let* initial_tree = new_level_tree ctxt Raw_level_repr.root in
+        let rec aux index tree =
+          if Compare.Int.(index = number_of_messages) then return tree
+          else
+            let* tree =
+              add_message_in_level_tree tree (Z.of_int index) payload
+            in
+            aux (index + 1) tree
+        in
+        aux 0 initial_tree
+      in
+      let* () = P.commit_tree ctxt ["level_tree"] tree in
+      let* res = P.produce_proof ctxt tree (payload_and_level pn) in
+      match res with
+      | None -> return_none
+      | Some (proof, (_, _)) -> return_some proof
+
+    let verify_proof_about_payload_and_level proof pn =
+      let open Lwt_syntax in
+      let* res = verify_proof_about_payload_and_level proof pn in
+      match res with None -> return_false | Some _ -> return_true
+  end
+
   module Internal_for_tests = struct
     let eq_tree = Tree.equal
 
@@ -1149,49 +1314,55 @@ struct
   end
 end
 
-include (
-  Make_hashing_scheme (struct
-    module Tree = struct
-      include Context.Tree
+module ProtoContextTree = struct
+  include Context.Tree
 
-      type t = Context.t
+  type t = Context.t
 
-      type tree = Context.tree
+  type tree = Context.tree
 
-      type value = bytes
+  type value = bytes
 
-      type key = string list
-    end
+  type key = string list
+end
+
+module ProtoP : P with module Tree = ProtoContextTree = struct
+  module Tree = ProtoContextTree
 
-    type t = Context.t
+  type t = Context.t
 
-    type tree = Context.tree
+  type tree = Context.tree
 
-    let commit_tree _ctxt _key _tree =
-      (* This is a no-op in the protocol inbox implementation *)
-      Lwt.return ()
+  let commit_tree _ctxt _key _tree =
+    (* This is a no-op in the protocol inbox implementation *)
+    Lwt.return ()
 
-    let lookup_tree _ctxt _hash =
-      (* We cannot find the tree without a full inbox_context *)
-      Lwt.return None
+  let lookup_tree _ctxt _hash =
+    (* We cannot find the tree without a full inbox_context *)
+    Lwt.return None
 
-    type proof = Context.Proof.tree Context.Proof.t
+  type proof = Context.Proof.tree Context.Proof.t
 
-    let proof_encoding = Context.Proof_encoding.V1.Tree32.tree_proof_encoding
+  let proof_encoding = Context.Proof_encoding.V1.Tree32.tree_proof_encoding
 
-    let proof_before proof =
-      match proof.Context.Proof.before with
-      | `Value hash | `Node hash -> Hash.of_context_hash hash
+  let proof_before proof =
+    match proof.Context.Proof.before with
+    | `Value hash | `Node hash -> Hash.of_context_hash hash
 
-    let verify_proof p f =
-      Lwt.map Result.to_option (Context.verify_tree_proof p f)
+  let verify_proof p f =
+    Lwt.map Result.to_option (Context.verify_tree_proof p f)
 
-    let produce_proof _ _ _ =
-      (* We cannot produce a proof without full inbox_context *)
-      Lwt.return None
-  end) :
-    Merkelized_operations
-      with type tree = Context.tree
-       and type inbox_context = Context.t)
+  let produce_proof _ _ _ =
+    (* We cannot produce a proof without full inbox_context *)
+    Lwt.return None
+end
+
+include (
+  Make_hashing_scheme
+    (ProtoP) :
+      Merkelized_operations
+        with type tree = Context.tree
+         and type inbox_context = Context.t
+         and module P = ProtoP)
 
 type inbox = t
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli
index 82b5fa8646f5a3e75c979fafe8e3c50f1b3af7d8..13bb325253c327a3e498c05fbef7a595236c00bf 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli
@@ -218,6 +218,12 @@ include Sc_rollup_data_version_sig.S with type t = V1.t
 
 include module type of V1 with type t = V1.t
 
+module Internal_for_snoop : sig
+  module Skip_list : Skip_list_repr.S
+
+  val hash_skip_list_cell : (Hash.t, Hash.t) Skip_list.cell -> Hash.t
+end
+
 (** This extracts the current level hash from the inbox. Note: the
     current level hash is stored lazily as [fun () -> ...], and this
     function will call that function. So don't use this if you want to
@@ -228,6 +234,31 @@ type serialized_proof
 
 val serialized_proof_encoding : serialized_proof Data_encoding.t
 
+(** Merkelized operations for the inbox are parameterized by {!P}. *)
+module type P = sig
+  module Tree : Context.TREE with type key = string list and type value = bytes
+
+  type tree = Tree.tree
+
+  type t = Tree.t
+
+  val commit_tree : t -> string list -> tree -> unit Lwt.t
+
+  val lookup_tree : t -> Hash.t -> tree option Lwt.t
+
+  type proof
+
+  val proof_encoding : proof Data_encoding.t
+
+  val proof_before : proof -> Hash.t
+
+  val verify_proof :
+    proof -> (tree -> (tree * 'a) Lwt.t) -> (tree * 'a) option Lwt.t
+
+  val produce_proof :
+    Tree.t -> tree -> (tree -> (tree * 'a) Lwt.t) -> (proof * 'a) option Lwt.t
+end
+
 (** The following operations are subject to cross-validation between
     rollup nodes and the layer 1. *)
 module type Merkelized_operations = sig
@@ -367,6 +398,8 @@ module type Merkelized_operations = sig
 
   val of_serialized_proof : serialized_proof -> proof option
 
+  val cost_of_serialized_proof : serialized_proof -> Gas_limit_repr.cost
+
   (** See the docstring for the [proof] type for details of proof semantics.
 
       [verify_proof starting_point inbox proof] will return the third
@@ -377,6 +410,11 @@ module type Merkelized_operations = sig
     proof ->
     Sc_rollup_PVM_sem.input option tzresult Lwt.t
 
+  (** [cost_verify_proof starting_point inbox proof] returns the gas cost
+      for the execution of [verify_proof starting_point inbox proof]. *)
+  val cost_verify_proof :
+    Raw_level_repr.t * Z.t -> history_proof -> proof -> Gas_limit_repr.cost
+
   (** [produce_proof ctxt history inbox (level, counter)] creates an
       inbox proof proving the first message after the index [counter] at
       location [level]. This will fail if the [ctxt] given doesn't have
@@ -393,6 +431,15 @@ module type Merkelized_operations = sig
       message at all. *)
   val empty : inbox_context -> Sc_rollup_repr.t -> Raw_level_repr.t -> t Lwt.t
 
+  module P : P
+
+  module Internal_MerkelizedOperations_for_snoop : sig
+    val produce_proof_about_payload_and_level :
+      inbox_context -> int -> Z.t -> P.proof option Lwt.t
+
+    val verify_proof_about_payload_and_level : P.proof -> Z.t -> bool Lwt.t
+  end
+
   module Internal_for_tests : sig
     val eq_tree : tree -> tree -> bool
 
@@ -406,30 +453,6 @@ module type Merkelized_operations = sig
   end
 end
 
-module type P = sig
-  module Tree : Context.TREE with type key = string list and type value = bytes
-
-  type tree = Tree.tree
-
-  type t = Tree.t
-
-  val commit_tree : t -> string list -> tree -> unit Lwt.t
-
-  val lookup_tree : t -> Hash.t -> tree option Lwt.t
-
-  type proof
-
-  val proof_encoding : proof Data_encoding.t
-
-  val proof_before : proof -> Hash.t
-
-  val verify_proof :
-    proof -> (tree -> (tree * 'a) Lwt.t) -> (tree * 'a) option Lwt.t
-
-  val produce_proof :
-    Tree.t -> tree -> (tree -> (tree * 'a) Lwt.t) -> (proof * 'a) option Lwt.t
-end
-
 (**
 
    This validation is based on a standardized Merkelization
@@ -444,7 +467,10 @@ end
 
 *)
 module Make_hashing_scheme (P : P) :
-  Merkelized_operations with type tree = P.tree and type inbox_context = P.t
+  Merkelized_operations
+    with type tree = P.tree
+     and type inbox_context = P.t
+     and module P = P
 
 include
   Merkelized_operations
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml
index f6313e7904f9d1b395353f93fc8affe21c9a651c..5eded6f253b59a4008fae9d325d3e13e9020bd4a 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml
@@ -80,30 +80,35 @@ let check p reason =
   let open Lwt_tzresult_syntax in
   if p then return () else proof_error reason
 
-let check_inbox_proof snapshot serialized_inbox_proof (level, counter) =
-  match Sc_rollup_inbox_repr.of_serialized_proof serialized_inbox_proof with
-  | None -> return None
-  | Some inbox_proof ->
-      Sc_rollup_inbox_repr.verify_proof (level, counter) snapshot inbox_proof
+let cost_check_inbox_proof _snapshot _inbox_proof =
+  let open Gas_limit_repr in
+  (* FIXME: To be defined by forthcoming commits. *)
+  free
 
 let pp_proof fmt serialized_inbox_proof =
   match Sc_rollup_inbox_repr.of_serialized_proof serialized_inbox_proof with
   | None -> Format.pp_print_string fmt "<invalid-proof-serialization>"
   | Some proof -> Sc_rollup_inbox_repr.pp_proof fmt proof
 
-let valid snapshot commit_level ~pvm_name proof =
+let valid snapshot commit_level ~pvm_name proof inbox_proof =
   let open Lwt_tzresult_syntax in
   let (module P) = Sc_rollups.wrapped_proof_module proof.pvm_step in
   let* () = check (String.equal P.name pvm_name) "Incorrect PVM kind" in
   let input_requested = P.proof_input_requested P.proof in
   let input_given = P.proof_input_given P.proof in
   let* input =
-    match (input_requested, proof.inbox) with
+    match (input_requested, inbox_proof) with
     | Sc_rollup_PVM_sem.No_input_required, None -> return None
     | Sc_rollup_PVM_sem.Initial, Some inbox_proof ->
-        check_inbox_proof snapshot inbox_proof (Raw_level_repr.root, Z.zero)
+        Sc_rollup_inbox_repr.verify_proof
+          (Raw_level_repr.root, Z.zero)
+          snapshot
+          inbox_proof
     | Sc_rollup_PVM_sem.First_after (level, counter), Some inbox_proof ->
-        check_inbox_proof snapshot inbox_proof (level, Z.succ counter)
+        Sc_rollup_inbox_repr.verify_proof
+          (level, Z.succ counter)
+          snapshot
+          inbox_proof
     | _ ->
         proof_error
           (Format.asprintf
@@ -123,6 +128,34 @@ let valid snapshot commit_level ~pvm_name proof =
   in
   Lwt.map Result.ok (P.verify_proof P.proof)
 
+let cost_valid snapshot _commit_level ~pvm_name:_ proof inbox_proof_opt =
+  let open Gas_limit_repr in
+  (* The cost is defined over the structure of [valid]. *)
+  let (module P) = Sc_rollups.wrapped_proof_module proof.pvm_step in
+  let cost_check_pvm_name_equality =
+    (* The cost of the equality is bounded by the cost of comparing
+       with the longest PVM name. *)
+    Saturation_repr.safe_int 35
+  in
+  let input_requested = P.proof_input_requested P.proof in
+  let cost_input =
+    match (input_requested, inbox_proof_opt) with
+    | Sc_rollup_PVM_sem.No_input_required, _ -> free
+    | _, Some inbox_proof -> cost_check_inbox_proof snapshot inbox_proof
+    | _, _ ->
+        (* The function will fail. *)
+        free
+  in
+  let cost_check_input_equality =
+    match P.proof_input_given P.proof with
+    | None -> free
+    | Some input_given ->
+        Sc_rollup_PVM_sem.cost_input_equal input_given input_given
+  in
+  let ( + ) = Saturation_repr.add in
+  cost_check_pvm_name_equality + cost_input + cost_check_input_equality
+  + P.cost_verify_proof P.proof
+
 module type PVM_with_context_and_state = sig
   include Sc_rollups.PVM.S
 
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli
index 81efa00c44362ba2a517b99a66a644d71dcf0d25..e8cd90b3caa4c2efc7fc2a57a205360e30334d2f 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli
@@ -96,8 +96,19 @@ val valid :
   Raw_level_repr.t ->
   pvm_name:string ->
   t ->
+  Sc_rollup_inbox_repr.proof option ->
   bool tzresult Lwt.t
 
+(** [cost_valid history_proof level ~pvm_name proof inbox_proof]
+   returns the cost of refutation proof validation. *)
+val cost_valid :
+  Sc_rollup_inbox_repr.history_proof ->
+  Raw_level_repr.t ->
+  pvm_name:string ->
+  t ->
+  Sc_rollup_inbox_repr.proof option ->
+  Gas_limit_repr.cost
+
 module type PVM_with_context_and_state = sig
   include Sc_rollups.PVM.S
 
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_refutation_storage.ml b/src/proto_alpha/lib_protocol/sc_rollup_refutation_storage.ml
index 6a316e6200fa625bbdb171be8487e83a0a849439..ddbf425b3525d7557e74c5620b046cdf5781ed59 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_refutation_storage.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_refutation_storage.ml
@@ -286,7 +286,7 @@ let game_move ctxt rollup ~player ~opponent refutation =
          (Sc_rollup_game_repr.Index.staker idx game.turn))
       Sc_rollup_wrong_turn
   in
-  let*! move_result = Sc_rollup_game_repr.play game refutation in
+  let* move_result, ctxt = Sc_rollup_game_repr.play ctxt game refutation in
   match move_result with
   | Either.Left outcome -> return (Some outcome, ctxt)
   | Either.Right new_game ->
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml
index 9e19e92abac11f0949f46f6c3cf005f1c5f03ccd..87b5f2b435b1a7312db0963ec877670bd616255f 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.ml
@@ -59,4 +59,9 @@ let ( = ) = equal
 
 let ( <> ) x y = not (x = y)
 
+let size_in_bytes tick =
+  (* Same definition as in {!Michelson_v1_gas}. *)
+  let bits = numbits tick in
+  (7 + bits) / 8
+
 module Map = Map.Make (Z)
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli
index 19d8d34c74c67da22fad35f2cabed38ba6559337..47774acc0cceb76b113be2e28a49054ab0c7352a 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_tick_repr.mli
@@ -59,6 +59,10 @@ val of_number_of_ticks : Sc_rollup_repr.Number_of_ticks.t -> t
 
 val of_z : Z.t -> t
 
+(** [size_in_bytes tick] is the size in bytes of [tick] internal
+   representation. This function is used by the gas model. *)
+val size_in_bytes : t -> int
+
 val encoding : t Data_encoding.t
 
 val pp : Format.formatter -> t -> unit
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml
index 1c9f2227d59866161ea1258362b61085e5d46baa..2817d39a6908e1172198513b78bae34296a7f21e 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml
@@ -328,6 +328,11 @@ module V2_0_0 = struct
       | Some (_, request) ->
           return (PS.input_request_equal request proof.requested)
 
+    let cost_verify_proof _proof =
+      let open Gas_limit_repr in
+      (* FIXME: To be defined by forthcoming commits. *)
+      free
+
     type error += WASM_proof_production_failed
 
     let produce_proof context input_given state =
diff --git a/src/proto_alpha/lib_protocol/skip_list_repr.ml b/src/proto_alpha/lib_protocol/skip_list_repr.ml
index d8c46df0212b5a8d77422abd4251e5238a440fe2..d6d2692f5e6952b16942716cb3775f9bfa51d423 100644
--- a/src/proto_alpha/lib_protocol/skip_list_repr.ml
+++ b/src/proto_alpha/lib_protocol/skip_list_repr.ml
@@ -53,6 +53,8 @@ module type S = sig
 
   val back_pointers : ('content, 'ptr) cell -> 'ptr list
 
+  val number_of_back_pointers : ('content, 'ptr) cell -> int
+
   val genesis : 'content -> ('content, 'ptr) cell
 
   val next :
@@ -138,6 +140,8 @@ end) : S = struct
     && Compare.Int.equal index cell2.index
     && equal_back_pointers back_pointers cell2.back_pointers
 
+  let number_of_back_pointers cell = FallbackArray.length cell.back_pointers
+
   let index cell = cell.index
 
   let back_pointers_to_list a =
@@ -257,7 +261,7 @@ end) : S = struct
             (*
               If (mid_cell_index > target_index) &&
                  (prev_mid_cell_index < target_index)
-              then we found the closest cell to the target, which is mid_cell,
+              then we found the closest cell to the target, which is mid_cell.
               so we return its index [mid_idx] in the array of back_pointers.
             *)
             Some mid_idx
@@ -280,18 +284,6 @@ end) : S = struct
     in
     aux [] cell_ptr
 
-  let mem equal x l =
-    let open FallbackArray in
-    let n = length l in
-    let rec aux idx =
-      if Compare.Int.(idx >= n) then false
-      else
-        match get l idx with
-        | None -> aux (idx + 1)
-        | Some y -> if equal x y then true else aux (idx + 1)
-    in
-    aux 0
-
   let assume_some o f = match o with None -> false | Some x -> f x
 
   let valid_back_path ~equal_ptr ~deref ~cell_ptr ~target_ptr path =
@@ -307,12 +299,11 @@ end) : S = struct
       | cell_ptr, cell_ptr' :: path ->
           assume_some (deref cell_ptr) @@ fun cell ->
           assume_some (deref cell_ptr') @@ fun cell' ->
-          mem equal_ptr cell_ptr' cell.back_pointers
-          && assume_some (best_skip cell target_index powers) @@ fun best_idx ->
-             assume_some (back_pointer cell best_idx) @@ fun best_ptr ->
-             let minimal = equal_ptr best_ptr cell_ptr' in
-             let index' = cell'.index in
-             minimal && valid_path index' cell_ptr' path
+          assume_some (best_skip cell target_index powers) @@ fun best_idx ->
+          assume_some (back_pointer cell best_idx) @@ fun best_ptr ->
+          let minimal = equal_ptr best_ptr cell_ptr' in
+          let index' = cell'.index in
+          minimal && valid_path index' cell_ptr' path
     in
     match path with
     | [] -> false
diff --git a/src/proto_alpha/lib_protocol/skip_list_repr.mli b/src/proto_alpha/lib_protocol/skip_list_repr.mli
index c2c3348e4d78c86393d62fd3714ef006adab67b2..666c6518141accf995d127d0cf4f8f9687101b1c 100644
--- a/src/proto_alpha/lib_protocol/skip_list_repr.mli
+++ b/src/proto_alpha/lib_protocol/skip_list_repr.mli
@@ -84,6 +84,10 @@ module type S = sig
   (** [back_pointers cell] returns the back pointers of [cell]. *)
   val back_pointers : ('content, 'ptr) cell -> 'ptr list
 
+  (** [number_of_back_pointers cell] returns the number of back
+      pointers of [cell]. *)
+  val number_of_back_pointers : ('content, 'ptr) cell -> int
+
   (** [genesis content] is the first cell of a skip list. It has
       no back pointers. *)
   val genesis : 'content -> ('content, 'ptr) cell