From 724e2673889e272797e3e962b64a1c509158d529 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Sat, 11 Jun 2022 19:31:03 +0200
Subject: [PATCH 01/10] Proto/Cache_memory_helpers: move 2 values

---
 src/proto_alpha/lib_protocol/cache_memory_helpers.ml | 4 ++++
 src/proto_alpha/lib_protocol/contract_repr.ml        | 8 --------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/proto_alpha/lib_protocol/cache_memory_helpers.ml b/src/proto_alpha/lib_protocol/cache_memory_helpers.ml
index 45c1ec4c1dfe..137f19977931 100644
--- a/src/proto_alpha/lib_protocol/cache_memory_helpers.ml
+++ b/src/proto_alpha/lib_protocol/cache_memory_helpers.ml
@@ -128,6 +128,10 @@ let bytes_size b = string_size_gen (Bytes.length b)
 
 let string_size s = string_size_gen (String.length s)
 
+let blake2b_hash_size = h1w +! string_size_gen 20
+
+let public_key_hash_in_memory_size = h1w +! blake2b_hash_size
+
 let ret_adding (nodes, size) added = (nodes, size +! added)
 
 let ret_succ_adding (nodes, size) added = (Nodes.succ nodes, size +! added)
diff --git a/src/proto_alpha/lib_protocol/contract_repr.ml b/src/proto_alpha/lib_protocol/contract_repr.ml
index 20045646df69..e1073e1253d9 100644
--- a/src/proto_alpha/lib_protocol/contract_repr.ml
+++ b/src/proto_alpha/lib_protocol/contract_repr.ml
@@ -39,14 +39,6 @@ include Compare.Make (struct
     | Originated _, Implicit _ -> 1
 end)
 
-let blake2b_hash_size =
-  let open Cache_memory_helpers in
-  h1w +! string_size_gen 20
-
-let public_key_hash_in_memory_size =
-  let open Cache_memory_helpers in
-  header_size +! word_size +! blake2b_hash_size
-
 let in_memory_size =
   let open Cache_memory_helpers in
   function
-- 
GitLab


From bc1e33cddb480a5a184005ee5cc0945c678f6c49 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Sat, 11 Jun 2022 19:33:35 +0200
Subject: [PATCH 02/10] Proto: expose in_memory_size for rollups

---
 src/proto_alpha/lib_protocol/alpha_context.mli | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli
index ec0a6a33a992..462b29885ef4 100644
--- a/src/proto_alpha/lib_protocol/alpha_context.mli
+++ b/src/proto_alpha/lib_protocol/alpha_context.mli
@@ -1791,6 +1791,8 @@ end
 module Tx_rollup : sig
   include BASIC_DATA
 
+  val in_memory_size : t -> Cache_memory_helpers.sint
+
   val rpc_arg : t RPC_arg.arg
 
   val to_b58check : t -> string
@@ -2754,6 +2756,8 @@ module Sc_rollup : sig
 
   type rollup := t
 
+  val in_memory_size : t -> Cache_memory_helpers.sint
+
   module Staker :
     S.SIGNATURE_PUBLIC_KEY_HASH with type t = Signature.Public_key_hash.t
 
-- 
GitLab


From 4a98899aa3a29952dfbc9fe07a79222729add727 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Tue, 14 Jun 2022 22:45:31 +0200
Subject: [PATCH 03/10] Proto/Michelson: parse_contract_data already returns a
 typed contract

---
 src/proto_alpha/lib_protocol/script_ir_translator.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index 951bf1470c08..55868ea65001 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml
@@ -2480,7 +2480,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data :
             arg_ty
             address.destination
             ~entrypoint:address.entrypoint
-          >|=? fun (ctxt, _) -> (Typed_contract {arg_ty; address}, ctxt) )
+          >|=? fun (ctxt, typed_contract) -> (typed_contract, ctxt) )
   (* Pairs *)
   | Pair_t (tl, tr, _, _), expr ->
       let r_witness = comb_witness1 tr in
-- 
GitLab


From 11d1111058db84174b4d0d56059a2abeaa65e39d Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Tue, 14 Jun 2022 22:52:51 +0200
Subject: [PATCH 04/10] Proto/Michelson: inline and unfactorized
 make_transaction_to_contract

---
 .../lib_protocol/script_interpreter_defs.ml   | 83 +++++++++----------
 1 file changed, 40 insertions(+), 43 deletions(-)

diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
index d18d1a8927e5..99103b20a210 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
@@ -464,40 +464,6 @@ let apply ctxt gas capture_ty capture lam =
       let gas, ctxt = local_gas_counter_and_outdated_context ctxt in
       return (lam', ctxt, gas)
 
-let make_transaction_to_contract ctxt ~(destination : Contract.t) ~amount
-    ~entrypoint ~location ~parameters_ty ~parameters =
-  unparse_data ctxt Optimized parameters_ty parameters
-  >>=? fun (unparsed_parameters, ctxt) ->
-  Lwt.return
-    ( Gas.consume ctxt (Script.strip_locations_cost unparsed_parameters)
-    >|? fun ctxt ->
-      let unparsed_parameters = Micheline.strip_locations unparsed_parameters in
-      match destination with
-      | Implicit destination ->
-          ( Transaction_to_implicit
-              {
-                destination;
-                amount;
-                entrypoint;
-                location;
-                parameters_ty;
-                parameters;
-                unparsed_parameters;
-              },
-            ctxt )
-      | Originated destination ->
-          ( Transaction_to_smart_contract
-              {
-                destination;
-                amount;
-                entrypoint;
-                location;
-                parameters_ty;
-                parameters;
-                unparsed_parameters;
-              },
-            ctxt ) )
-
 let make_transaction_to_tx_rollup (type t tc) ctxt ~destination ~amount
     ~entrypoint ~(parameters_ty : (t, tc) ty) ~parameters =
   (* The entrypoints of a transaction rollup are polymorphic wrt. the
@@ -602,15 +568,46 @@ let transfer (ctxt, sc) gas amount location parameters_ty parameters
     ~temporary:true
   >>=? fun (parameters, lazy_storage_diff, ctxt) ->
   (match destination with
-  | Contract destination ->
-      make_transaction_to_contract
-        ctxt
-        ~destination
-        ~amount
-        ~entrypoint
-        ~location
-        ~parameters_ty
-        ~parameters
+  | Contract (Implicit destination) ->
+      unparse_data ctxt Optimized parameters_ty parameters
+      >>=? fun (unparsed_parameters, ctxt) ->
+      Lwt.return
+        ( Gas.consume ctxt (Script.strip_locations_cost unparsed_parameters)
+        >|? fun ctxt ->
+          let unparsed_parameters =
+            Micheline.strip_locations unparsed_parameters
+          in
+          ( Transaction_to_implicit
+              {
+                destination;
+                amount;
+                entrypoint;
+                location;
+                parameters_ty;
+                parameters;
+                unparsed_parameters;
+              },
+            ctxt ) )
+  | Contract (Originated destination) ->
+      unparse_data ctxt Optimized parameters_ty parameters
+      >>=? fun (unparsed_parameters, ctxt) ->
+      Lwt.return
+        ( Gas.consume ctxt (Script.strip_locations_cost unparsed_parameters)
+        >|? fun ctxt ->
+          let unparsed_parameters =
+            Micheline.strip_locations unparsed_parameters
+          in
+          ( Transaction_to_smart_contract
+              {
+                destination;
+                amount;
+                entrypoint;
+                location;
+                parameters_ty;
+                parameters;
+                unparsed_parameters;
+              },
+            ctxt ) )
   | Tx_rollup destination ->
       make_transaction_to_tx_rollup
         ctxt
-- 
GitLab


From eb44e931fd04413b2423f5b19402ee16439eb743 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Sat, 11 Jun 2022 18:59:15 +0200
Subject: [PATCH 05/10] Proto/Michelson: add typed_destination

---
 src/proto_alpha/lib_protocol/script_typed_ir.ml  | 8 ++++++++
 src/proto_alpha/lib_protocol/script_typed_ir.mli | 8 ++++++++
 2 files changed, 16 insertions(+)

diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml
index 66aa00a23b18..83bd2e426e12 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml
@@ -1110,6 +1110,14 @@ and ('arg, 'ret) lambda =
       -> ('arg, 'ret) lambda
 [@@coq_force_gadt]
 
+and 'arg typed_destination =
+  | Typed_implicit : public_key_hash -> unit typed_destination
+  | Typed_originated of Contract_hash.t
+  | Typed_tx_rollup :
+      Tx_rollup.t
+      -> (_ ticket, tx_rollup_l2_address) pair typed_destination
+  | Typed_sc_rollup of Sc_rollup.t
+
 and 'arg typed_contract =
   | Typed_contract : {
       arg_ty : ('arg, _) ty;
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli
index 5dbff914eb23..a984dc6ca3b6 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli
@@ -1111,6 +1111,14 @@ and ('arg, 'ret) lambda =
       -> ('arg, 'ret) lambda
 [@@coq_force_gadt]
 
+and 'arg typed_destination =
+  | Typed_implicit : public_key_hash -> unit typed_destination
+  | Typed_originated of Contract_hash.t
+  | Typed_tx_rollup :
+      Tx_rollup.t
+      -> (_ ticket, tx_rollup_l2_address) pair typed_destination
+  | Typed_sc_rollup of Sc_rollup.t
+
 and 'arg typed_contract =
   | Typed_contract : {
       arg_ty : ('arg, _) ty;
-- 
GitLab


From 2d0c78607ffd074d78204729911ab8724737546d Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Sat, 11 Jun 2022 19:18:31 +0200
Subject: [PATCH 06/10] Proto/Michelson: add conversion between typed and
 untyped destination

---
 .../lib_protocol/script_typed_ir.ml           | 28 +++++++++++++++++++
 .../lib_protocol/script_typed_ir.mli          | 11 ++++++++
 2 files changed, 39 insertions(+)

diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml
index 83bd2e426e12..9fed3fa4edf7 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml
@@ -2154,3 +2154,31 @@ let value_traverse (type t tc) (ty : (t, tc) ty) (x : t) init f =
 
 let stack_top_ty : type a b s. (a, b * s) stack_ty -> a ty_ex_c = function
   | Item_t (ty, _) -> Ty_ex_c ty
+
+module Typed_destination = struct
+  let untyped : type a. a typed_destination -> Destination.t = function
+    | Typed_implicit pkh -> Destination.Contract (Implicit pkh)
+    | Typed_originated contract_hash ->
+        Destination.Contract (Originated contract_hash)
+    | Typed_tx_rollup tx_rollup -> Destination.Tx_rollup tx_rollup
+    | Typed_sc_rollup sc_rollup -> Destination.Sc_rollup sc_rollup
+
+  module Internal_for_tests = struct
+    let typed_exn :
+        type a ac. (a, ac) ty -> Destination.t -> a typed_destination =
+     fun ty destination ->
+      match (destination, ty) with
+      | Contract (Implicit pkh), Unit_t -> Typed_implicit pkh
+      | Contract (Implicit _), _ ->
+          invalid_arg "Implicit contracts expect type unit"
+      | Contract (Originated contract_hash), _ -> Typed_originated contract_hash
+      | Tx_rollup tx_rollup, Pair_t (Ticket_t _, Tx_rollup_l2_address_t, _, _)
+        ->
+          Typed_tx_rollup tx_rollup
+      | Tx_rollup _, _ ->
+          invalid_arg
+            "Transaction rollups expect type (pair (ticket _) \
+             tx_rollup_l2_address)"
+      | Sc_rollup sc_rollup, _ -> Typed_sc_rollup sc_rollup
+  end
+end
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli
index a984dc6ca3b6..165078192c8c 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli
@@ -1760,3 +1760,14 @@ type 'a value_traverse = {apply : 't 'tc. 'a -> ('t, 'tc) ty -> 't -> 'a}
 val value_traverse : ('t, _) ty -> 't -> 'r -> 'r value_traverse -> 'r
 
 val stack_top_ty : ('a, 'b * 's) stack_ty -> 'a ty_ex_c
+
+module Typed_destination : sig
+  val untyped : _ typed_destination -> Destination.t
+
+  module Internal_for_tests : sig
+    (* This function doesn't guarantee that the contract is well-typed wrt its
+       registered type at origination, it only guarantees that the type is
+       plausible wrt to the destination kind. *)
+    val typed_exn : ('a, _) ty -> Destination.t -> 'a typed_destination
+  end
+end
-- 
GitLab


From cb9aa90fba99235996c10167fef31f0d0b845182 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Sat, 11 Jun 2022 18:51:03 +0200
Subject: [PATCH 07/10] Proto/Michelson: inline address in typed_contract

---
 .../lib_benchmark/michelson_samplers.ml       | 12 +++------
 .../lib_protocol/script_interpreter.ml        | 25 +++++++++++--------
 .../lib_protocol/script_ir_translator.ml      | 16 ++++++------
 .../lib_protocol/script_typed_ir.ml           |  3 ++-
 .../lib_protocol/script_typed_ir.mli          |  3 ++-
 .../lib_protocol/script_typed_ir_size.ml      |  6 +++--
 .../michelson/test_script_typed_ir_size.ml    |  4 +--
 .../michelson/test_typechecking.ml            |  9 +++----
 8 files changed, 38 insertions(+), 40 deletions(-)

diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
index e45390cbba73..e00bf8572ee4 100644
--- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml
+++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
@@ -538,8 +538,7 @@ end)
       let* c = originated in
       let* entrypoint = entrypoint in
       let destination = Alpha_context.Destination.Contract (Originated c) in
-      let address = {destination; entrypoint} in
-      return (Typed_contract {arg_ty; address})
+      return (Typed_contract {arg_ty; destination; entrypoint})
 
     let generate_sc_rollup_contract :
         type arg argc.
@@ -550,8 +549,7 @@ end)
       let* ru = sc_rollup in
       let* entrypoint = entrypoint in
       let destination = Alpha_context.Destination.Sc_rollup ru in
-      let address = {destination; entrypoint} in
-      return (Typed_contract {arg_ty; address})
+      return (Typed_contract {arg_ty; destination; entrypoint})
 
     let generate_any_type_contract :
         type arg argc.
@@ -578,8 +576,7 @@ end)
               Alpha_context.Destination.Contract (Implicit pkh)
             in
             let entrypoint = Alpha_context.Entrypoint.default in
-            let address = {destination; entrypoint} in
-            return (Typed_contract {arg_ty; address})
+            return (Typed_contract {arg_ty; destination; entrypoint})
           else generate_any_type_contract arg_ty
       | Pair_t (Ticket_t _, Tx_rollup_l2_address_t, _, _) ->
           let* b = Base_samplers.uniform_bool in
@@ -587,8 +584,7 @@ end)
             let* tx_rollup = tx_rollup in
             let destination = Alpha_context.Destination.Tx_rollup tx_rollup in
             let entrypoint = Alpha_context.Tx_rollup.deposit_entrypoint in
-            let address = {destination; entrypoint} in
-            return (Typed_contract {arg_ty; address})
+            return (Typed_contract {arg_ty; destination; entrypoint})
           else generate_any_type_contract arg_ty
       | _ -> generate_any_type_contract arg_ty
 
diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml
index deeddb0b3e90..f4eeea798be8 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter.ml
@@ -1101,7 +1101,8 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
           >>=? fun (opt, ctxt, gas) ->
           (step [@ocaml.tailcall]) (ctxt, sc) gas k ks opt stack
       | IAddress (_, k) ->
-          let (Typed_contract {address; _}) = accu in
+          let (Typed_contract {destination; entrypoint; _}) = accu in
+          let address = {destination; entrypoint} in
           (step [@ocaml.tailcall]) g gas k ks address stack
       | IContract (loc, t, entrypoint, k) -> (
           let addr = accu in
@@ -1126,21 +1127,24 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
           | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack)
       | ITransfer_tokens (loc, k) ->
           let p = accu in
-          let amount, (Typed_contract {arg_ty; address}, stack) = stack in
-          let {destination; entrypoint} = address in
+          let amount, (Typed_contract {arg_ty; destination; entrypoint}, stack)
+              =
+            stack
+          in
           transfer (ctxt, sc) gas amount loc arg_ty p destination entrypoint
           >>=? fun (accu, ctxt, gas) ->
           (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack
       | IImplicit_account (_, k) ->
           let key = accu in
           let arg_ty = unit_t in
-          let address =
-            {
-              destination = Contract (Contract.Implicit key);
-              entrypoint = Entrypoint.default;
-            }
+          let res =
+            Typed_contract
+              {
+                arg_ty;
+                destination = Contract (Contract.Implicit key);
+                entrypoint = Entrypoint.default;
+              }
           in
-          let res = Typed_contract {arg_ty; address} in
           (step [@ocaml.tailcall]) g gas k ks res stack
       | IView (_, view_signature, stack_ty, k) ->
           (iview [@ocaml.tailcall])
@@ -1222,8 +1226,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
           (step [@ocaml.tailcall]) g gas k ks res (accu, stack)
       | ISelf (_, ty, entrypoint, k) ->
           let destination : Destination.t = Contract (Originated sc.self) in
-          let address = {destination; entrypoint} in
-          let res = Typed_contract {arg_ty = ty; address} in
+          let res = Typed_contract {arg_ty = ty; destination; entrypoint} in
           (step [@ocaml.tailcall]) g gas k ks res (accu, stack)
       | ISelf_address (_, k) ->
           let destination : Destination.t = Contract (Originated sc.self) in
diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index 55868ea65001..ada21ff43b11 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml
@@ -373,7 +373,9 @@ let unparse_tx_rollup_l2_address ~loc ctxt mode
       let b58check = Tx_rollup_l2_address.to_b58check tx_address in
       (String (loc, b58check), ctxt)
 
-let unparse_contract ~loc ctxt mode (Typed_contract {arg_ty = _; address}) =
+let unparse_contract ~loc ctxt mode
+    (Typed_contract {arg_ty = _; destination; entrypoint}) =
+  let address = {destination; entrypoint} in
   unparse_address ~loc ctxt mode address
 
 let unparse_signature ~loc ctxt mode s =
@@ -4926,8 +4928,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
              >|? fun (eq, ctxt) ->
              ( ctxt,
                eq >|? fun Eq ->
-               let address = {destination; entrypoint} in
-               Typed_contract {arg_ty = arg; address} )
+               Typed_contract {arg_ty = arg; destination; entrypoint} )
             else
               (* An implicit account on any other entrypoint is not a valid contract. *)
               ok (error ctxt (fun _loc -> No_such_entrypoint entrypoint)))
@@ -4967,8 +4968,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
                     >|? fun (entrypoint_arg, ctxt) ->
                     ( ctxt,
                       entrypoint_arg >|? fun (entrypoint, arg_ty) ->
-                      let address = {destination; entrypoint} in
-                      Typed_contract {arg_ty; address} )) ))
+                      Typed_contract {arg_ty; destination; entrypoint} )) ))
   | Tx_rollup tx_rollup ->
       Tx_rollup_state.assert_exist ctxt tx_rollup >|=? fun ctxt ->
       if Entrypoint.(entrypoint = Tx_rollup.deposit_entrypoint) then
@@ -4976,8 +4976,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
            [parse_tx_rollup_deposit_parameters]. *)
         match arg with
         | Pair_t (Ticket_t (_, _), Tx_rollup_l2_address_t, _, _) ->
-            let address = {destination; entrypoint} in
-            (ctxt, ok @@ Typed_contract {arg_ty = arg; address})
+            (ctxt, ok @@ Typed_contract {arg_ty = arg; destination; entrypoint})
         | _ ->
             error ctxt (fun loc ->
                 Tx_rollup_bad_deposit_parameter (loc, serialize_ty_for_error arg))
@@ -5015,8 +5014,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
             >|? fun (entrypoint_arg, ctxt) ->
             ( ctxt,
               entrypoint_arg >|? fun (entrypoint, arg_ty) ->
-              let address = {destination; entrypoint} in
-              Typed_contract {arg_ty; address} ))
+              Typed_contract {arg_ty; destination; entrypoint} ))
 
 (* Same as [parse_contract], but does not fail when the contact is missing or
    if the expected type doesn't match the actual one. In that case None is
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml
index 9fed3fa4edf7..98928a30709b 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml
@@ -1121,7 +1121,8 @@ and 'arg typed_destination =
 and 'arg typed_contract =
   | Typed_contract : {
       arg_ty : ('arg, _) ty;
-      address : address;
+      destination : Destination.t;
+      entrypoint : Entrypoint.t;
     }
       -> 'arg typed_contract
 
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli
index 165078192c8c..ac52bb76e5e4 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli
@@ -1122,7 +1122,8 @@ and 'arg typed_destination =
 and 'arg typed_contract =
   | Typed_contract : {
       arg_ty : ('arg, _) ty;
-      address : address;
+      destination : Destination.t;
+      entrypoint : Entrypoint.t;
     }
       -> 'arg typed_contract
 
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
index 6a1fd023693f..d601dd0451ef 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
@@ -179,8 +179,10 @@ let comb_set_gadt_witness_size n (_w : (_, _, _) comb_set_gadt_witness) =
 let dup_n_gadt_witness_size n (_w : (_, _, _, _) dup_n_gadt_witness) =
   peano_shape_proof n
 
-let contract_size (Typed_contract {arg_ty; address}) =
-  ret_adding (ty_size arg_ty) (h2w +! address_size address)
+let contract_size (Typed_contract {arg_ty; destination; entrypoint}) =
+  ret_adding
+    (ty_size arg_ty)
+    (h3w +! destination_size destination +! Entrypoint.in_memory_size entrypoint)
 
 let sapling_state_size {Sapling.id; diff; memo_size} =
   h3w
diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
index f8b6638f0a07..9a2418fea892 100644
--- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
@@ -589,8 +589,8 @@ let check_value_size () =
        Contract_t
        =========
     *)
-    @ (let show fmt (Typed_contract {arg_ty = _; address}) =
-         show_address fmt address
+    @ (let show fmt (Typed_contract {arg_ty = _; destination; entrypoint}) =
+         show_address fmt {destination; entrypoint}
        in
        exs
          nsample
diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
index e1c7060734b0..ec8631996bc9 100644
--- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
@@ -795,10 +795,7 @@ let test_parse_contract_data_for_unit_rollup () =
   let ctxt = Incremental.alpha_ctxt incr in
   let* ( _ctxt,
          Typed_contract
-           {
-             arg_ty = Script_typed_ir.Unit_t;
-             address = {destination; entrypoint};
-           } ) =
+           {arg_ty = Script_typed_ir.Unit_t; destination; entrypoint} ) =
     wrap_error_lwt
     @@ Script_ir_translator.parse_contract_data
          ctxt
@@ -830,7 +827,7 @@ let test_parse_contract_data_for_rollup_with_entrypoints () =
   let rollup_destination = Sc_rollup.Address.to_b58check rollup in
   let* incr = Incremental.begin_construction block in
   let ctxt = Incremental.alpha_ctxt incr in
-  let* ctxt, Typed_contract {arg_ty = _; address = {destination; entrypoint}} =
+  let* ctxt, Typed_contract {arg_ty = _; destination; entrypoint} =
     let*? (Script_typed_ir.Ty_ex_c nat_pair) =
       Environment.wrap_tzresult Script_typed_ir.(pair_t (-1) nat_t nat_t)
     in
@@ -853,7 +850,7 @@ let test_parse_contract_data_for_rollup_with_entrypoints () =
   let* () =
     Assert.equal_string ~loc:__LOC__ (Entrypoint.to_string entrypoint) "add"
   in
-  let* _ctxt, Typed_contract {arg_ty = _; address = {destination; entrypoint}} =
+  let* _ctxt, Typed_contract {arg_ty = _; destination; entrypoint} =
     wrap_error_lwt
     @@ Script_ir_translator.parse_contract_data
          ctxt
-- 
GitLab


From 0df453499ef5af05f2fae430d30ee61e78172e72 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Mon, 13 Jun 2022 11:17:28 +0200
Subject: [PATCH 08/10] Proto/Michelson: use typed destination

---
 .../lib_benchmark/michelson_samplers.ml         | 12 ++++++++++++
 .../lib_protocol/script_interpreter.ml          |  6 ++++--
 .../lib_protocol/script_ir_translator.ml        | 17 +++++++++++++----
 src/proto_alpha/lib_protocol/script_typed_ir.ml |  2 +-
 .../lib_protocol/script_typed_ir.mli            |  2 +-
 .../lib_protocol/script_typed_ir_size.ml        | 10 +++++++++-
 .../michelson/test_script_typed_ir_size.ml      |  1 +
 .../integration/michelson/test_typechecking.ml  |  3 +++
 8 files changed, 44 insertions(+), 9 deletions(-)

diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
index e00bf8572ee4..b522cca91740 100644
--- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml
+++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
@@ -538,6 +538,9 @@ end)
       let* c = originated in
       let* entrypoint = entrypoint in
       let destination = Alpha_context.Destination.Contract (Originated c) in
+      let destination =
+        Typed_destination.Internal_for_tests.typed_exn arg_ty destination
+      in
       return (Typed_contract {arg_ty; destination; entrypoint})
 
     let generate_sc_rollup_contract :
@@ -549,6 +552,9 @@ end)
       let* ru = sc_rollup in
       let* entrypoint = entrypoint in
       let destination = Alpha_context.Destination.Sc_rollup ru in
+      let destination =
+        Typed_destination.Internal_for_tests.typed_exn arg_ty destination
+      in
       return (Typed_contract {arg_ty; destination; entrypoint})
 
     let generate_any_type_contract :
@@ -576,6 +582,9 @@ end)
               Alpha_context.Destination.Contract (Implicit pkh)
             in
             let entrypoint = Alpha_context.Entrypoint.default in
+            let destination =
+              Typed_destination.Internal_for_tests.typed_exn arg_ty destination
+            in
             return (Typed_contract {arg_ty; destination; entrypoint})
           else generate_any_type_contract arg_ty
       | Pair_t (Ticket_t _, Tx_rollup_l2_address_t, _, _) ->
@@ -584,6 +593,9 @@ end)
             let* tx_rollup = tx_rollup in
             let destination = Alpha_context.Destination.Tx_rollup tx_rollup in
             let entrypoint = Alpha_context.Tx_rollup.deposit_entrypoint in
+            let destination =
+              Typed_destination.Internal_for_tests.typed_exn arg_ty destination
+            in
             return (Typed_contract {arg_ty; destination; entrypoint})
           else generate_any_type_contract arg_ty
       | _ -> generate_any_type_contract arg_ty
diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml
index f4eeea798be8..791ed9d54f35 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter.ml
@@ -1102,6 +1102,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
           (step [@ocaml.tailcall]) (ctxt, sc) gas k ks opt stack
       | IAddress (_, k) ->
           let (Typed_contract {destination; entrypoint; _}) = accu in
+          let destination = Typed_destination.untyped destination in
           let address = {destination; entrypoint} in
           (step [@ocaml.tailcall]) g gas k ks address stack
       | IContract (loc, t, entrypoint, k) -> (
@@ -1131,6 +1132,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
               =
             stack
           in
+          let destination = Typed_destination.untyped destination in
           transfer (ctxt, sc) gas amount loc arg_ty p destination entrypoint
           >>=? fun (accu, ctxt, gas) ->
           (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack
@@ -1141,7 +1143,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
             Typed_contract
               {
                 arg_ty;
-                destination = Contract (Contract.Implicit key);
+                destination = Typed_implicit key;
                 entrypoint = Entrypoint.default;
               }
           in
@@ -1225,7 +1227,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
           let res = {destination; entrypoint = Entrypoint.default} in
           (step [@ocaml.tailcall]) g gas k ks res (accu, stack)
       | ISelf (_, ty, entrypoint, k) ->
-          let destination : Destination.t = Contract (Originated sc.self) in
+          let destination = Typed_originated sc.self in
           let res = Typed_contract {arg_ty = ty; destination; entrypoint} in
           (step [@ocaml.tailcall]) g gas k ks res (accu, stack)
       | ISelf_address (_, k) ->
diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index ada21ff43b11..60392a0046fb 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml
@@ -375,6 +375,7 @@ let unparse_tx_rollup_l2_address ~loc ctxt mode
 
 let unparse_contract ~loc ctxt mode
     (Typed_contract {arg_ty = _; destination; entrypoint}) =
+  let destination = Typed_destination.untyped destination in
   let address = {destination; entrypoint} in
   unparse_address ~loc ctxt mode address
 
@@ -4920,7 +4921,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
   match destination with
   | Contract contract -> (
       match contract with
-      | Implicit _ ->
+      | Implicit pkh ->
           Lwt.return
             (if Entrypoint.is_default entrypoint then
              (* An implicit account on the "default" entrypoint always exists and has type unit. *)
@@ -4928,11 +4929,13 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
              >|? fun (eq, ctxt) ->
              ( ctxt,
                eq >|? fun Eq ->
-               Typed_contract {arg_ty = arg; destination; entrypoint} )
+               let destination = Typed_implicit pkh in
+               (Typed_contract {arg_ty = arg; destination; entrypoint}
+                 : arg typed_contract) )
             else
               (* An implicit account on any other entrypoint is not a valid contract. *)
               ok (error ctxt (fun _loc -> No_such_entrypoint entrypoint)))
-      | Originated _ ->
+      | Originated contract_hash ->
           trace
             (Invalid_contract (loc, contract))
             ( Contract.get_script_code ctxt contract >>=? fun (ctxt, code) ->
@@ -4968,6 +4971,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
                     >|? fun (entrypoint_arg, ctxt) ->
                     ( ctxt,
                       entrypoint_arg >|? fun (entrypoint, arg_ty) ->
+                      let destination = Typed_originated contract_hash in
                       Typed_contract {arg_ty; destination; entrypoint} )) ))
   | Tx_rollup tx_rollup ->
       Tx_rollup_state.assert_exist ctxt tx_rollup >|=? fun ctxt ->
@@ -4976,7 +4980,11 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
            [parse_tx_rollup_deposit_parameters]. *)
         match arg with
         | Pair_t (Ticket_t (_, _), Tx_rollup_l2_address_t, _, _) ->
-            (ctxt, ok @@ Typed_contract {arg_ty = arg; destination; entrypoint})
+            let destination = Typed_tx_rollup tx_rollup in
+            ( ctxt,
+              ok
+              @@ (Typed_contract {arg_ty = arg; destination; entrypoint}
+                   : arg typed_contract) )
         | _ ->
             error ctxt (fun loc ->
                 Tx_rollup_bad_deposit_parameter (loc, serialize_ty_for_error arg))
@@ -5014,6 +5022,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
             >|? fun (entrypoint_arg, ctxt) ->
             ( ctxt,
               entrypoint_arg >|? fun (entrypoint, arg_ty) ->
+              let destination = Typed_sc_rollup sc_rollup in
               Typed_contract {arg_ty; destination; entrypoint} ))
 
 (* Same as [parse_contract], but does not fail when the contact is missing or
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml
index 98928a30709b..9cc3a94ac81b 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml
@@ -1121,7 +1121,7 @@ and 'arg typed_destination =
 and 'arg typed_contract =
   | Typed_contract : {
       arg_ty : ('arg, _) ty;
-      destination : Destination.t;
+      destination : 'arg typed_destination;
       entrypoint : Entrypoint.t;
     }
       -> 'arg typed_contract
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli
index ac52bb76e5e4..da95bffff5f1 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli
@@ -1122,7 +1122,7 @@ and 'arg typed_destination =
 and 'arg typed_contract =
   | Typed_contract : {
       arg_ty : ('arg, _) ty;
-      destination : Destination.t;
+      destination : 'arg typed_destination;
       entrypoint : Entrypoint.t;
     }
       -> 'arg typed_contract
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
index d601dd0451ef..10df0d4193ff 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
@@ -133,6 +133,12 @@ let address_size addr =
   +! destination_size addr.destination
   +! Entrypoint.in_memory_size addr.entrypoint
 
+let typed_destination_size : type a. a typed_destination -> sint = function
+  | Typed_implicit _ -> h1w +! public_key_hash_in_memory_size
+  | Typed_originated _ -> h1w +! blake2b_hash_size
+  | Typed_tx_rollup k -> h1w +! Tx_rollup.in_memory_size k
+  | Typed_sc_rollup k -> h1w +! Sc_rollup.in_memory_size k
+
 let tx_rollup_l2_address_size (tx : tx_rollup_l2_address) =
   Tx_rollup_l2_address.Indexable.in_memory_size @@ Indexable.forget tx
 
@@ -182,7 +188,9 @@ let dup_n_gadt_witness_size n (_w : (_, _, _, _) dup_n_gadt_witness) =
 let contract_size (Typed_contract {arg_ty; destination; entrypoint}) =
   ret_adding
     (ty_size arg_ty)
-    (h3w +! destination_size destination +! Entrypoint.in_memory_size entrypoint)
+    (h3w
+    +! typed_destination_size destination
+    +! Entrypoint.in_memory_size entrypoint)
 
 let sapling_state_size {Sapling.id; diff; memo_size} =
   h3w
diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
index 9a2418fea892..d7c2e129a24e 100644
--- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
@@ -590,6 +590,7 @@ let check_value_size () =
        =========
     *)
     @ (let show fmt (Typed_contract {arg_ty = _; destination; entrypoint}) =
+         let destination = Typed_destination.untyped destination in
          show_address fmt {destination; entrypoint}
        in
        exs
diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
index ec8631996bc9..4004172feb9f 100644
--- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
@@ -804,6 +804,7 @@ let test_parse_contract_data_for_unit_rollup () =
          (Destination.Sc_rollup rollup)
          ~entrypoint:Entrypoint.default
   in
+  let destination = Script_typed_ir.Typed_destination.untyped destination in
   (* Check that the destinations match. *)
   let* () =
     Assert.equal_string
@@ -839,6 +840,7 @@ let test_parse_contract_data_for_rollup_with_entrypoints () =
          (Destination.Sc_rollup rollup)
          ~entrypoint:(Entrypoint.of_string_strict_exn "add")
   in
+  let destination = Script_typed_ir.Typed_destination.untyped destination in
   (* Check that the destinations match. *)
   let* () =
     Assert.equal_string
@@ -859,6 +861,7 @@ let test_parse_contract_data_for_rollup_with_entrypoints () =
          (Destination.Sc_rollup rollup)
          ~entrypoint:(Entrypoint.of_string_strict_exn "reset")
   in
+  let destination = Script_typed_ir.Typed_destination.untyped destination in
   (* Check that the destinations match. *)
   let* () =
     Assert.equal_string
-- 
GitLab


From 11d2ba18a189cd445bc9d86e185f0969e60e78db Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Tue, 14 Jun 2022 22:55:58 +0200
Subject: [PATCH 09/10] Proto/Michelson: use typed destination in transfer

---
 src/proto_alpha/lib_protocol/script_interpreter.ml  |  1 -
 .../lib_protocol/script_interpreter_defs.ml         | 13 +++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml
index 791ed9d54f35..f57b42b8efea 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter.ml
@@ -1132,7 +1132,6 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type =
               =
             stack
           in
-          let destination = Typed_destination.untyped destination in
           transfer (ctxt, sc) gas amount loc arg_ty p destination entrypoint
           >>=? fun (accu, ctxt, gas) ->
           (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack
diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
index 99103b20a210..bab9c03e3f76 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
@@ -552,8 +552,9 @@ let emit_event (type t tc) (ctxt, sc) gas ~(event_type : (t, tc) ty)
    creates an operation that transfers an amount of [tez] to a destination and
    an entrypoint instantiated with argument [parameters] of type
    [parameters_ty]. *)
-let transfer (ctxt, sc) gas amount location parameters_ty parameters
-    (destination : Destination.t) entrypoint =
+let transfer (type t tc) (ctxt, sc) gas amount location
+    (parameters_ty : (t, tc) ty) (parameters : t)
+    (destination : t typed_destination) entrypoint =
   let ctxt = update_context gas ctxt in
   collect_lazy_storage ctxt parameters_ty parameters
   >>?= fun (to_duplicate, ctxt) ->
@@ -568,7 +569,7 @@ let transfer (ctxt, sc) gas amount location parameters_ty parameters
     ~temporary:true
   >>=? fun (parameters, lazy_storage_diff, ctxt) ->
   (match destination with
-  | Contract (Implicit destination) ->
+  | Typed_implicit destination ->
       unparse_data ctxt Optimized parameters_ty parameters
       >>=? fun (unparsed_parameters, ctxt) ->
       Lwt.return
@@ -588,7 +589,7 @@ let transfer (ctxt, sc) gas amount location parameters_ty parameters
                 unparsed_parameters;
               },
             ctxt ) )
-  | Contract (Originated destination) ->
+  | Typed_originated destination ->
       unparse_data ctxt Optimized parameters_ty parameters
       >>=? fun (unparsed_parameters, ctxt) ->
       Lwt.return
@@ -608,7 +609,7 @@ let transfer (ctxt, sc) gas amount location parameters_ty parameters
                 unparsed_parameters;
               },
             ctxt ) )
-  | Tx_rollup destination ->
+  | Typed_tx_rollup destination ->
       make_transaction_to_tx_rollup
         ctxt
         ~destination
@@ -616,7 +617,7 @@ let transfer (ctxt, sc) gas amount location parameters_ty parameters
         ~entrypoint
         ~parameters_ty
         ~parameters
-  | Sc_rollup destination ->
+  | Typed_sc_rollup destination ->
       make_transaction_to_sc_rollup
         ctxt
         ~destination
-- 
GitLab


From 1d54daa3f28933cc5dd450bced9b5b0bc187e40c Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mehdi.bouaziz@nomadic-labs.com>
Date: Tue, 14 Jun 2022 23:10:40 +0200
Subject: [PATCH 10/10] Proto/Michelson: remove dead assert false

Fix #2455
---
 .../lib_protocol/script_interpreter_defs.ml   | 46 ++++++++-----------
 1 file changed, 18 insertions(+), 28 deletions(-)

diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
index bab9c03e3f76..ff12b7e053ff 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
@@ -464,8 +464,9 @@ let apply ctxt gas capture_ty capture lam =
       let gas, ctxt = local_gas_counter_and_outdated_context ctxt in
       return (lam', ctxt, gas)
 
-let make_transaction_to_tx_rollup (type t tc) ctxt ~destination ~amount
-    ~entrypoint ~(parameters_ty : (t, tc) ty) ~parameters =
+let make_transaction_to_tx_rollup (type t) ctxt ~destination ~amount ~entrypoint
+    ~(parameters_ty : ((t ticket, tx_rollup_l2_address) pair, _) ty) ~parameters
+    =
   (* The entrypoints of a transaction rollup are polymorphic wrt. the
      tickets it can process. However, two Michelson values can have
      the same Micheline representation, but different types. What
@@ -483,32 +484,21 @@ let make_transaction_to_tx_rollup (type t tc) ctxt ~destination ~amount
     Entrypoint.(entrypoint = Tx_rollup.deposit_entrypoint)
     (Script_tc_errors.No_such_entrypoint entrypoint)
   >>?= fun () ->
-  match parameters_ty with
-  | Pair_t (Ticket_t (tp, _), _, _, _) ->
-      unparse_data ctxt Optimized parameters_ty parameters
-      >>=? fun (unparsed_parameters, ctxt) ->
-      Lwt.return
-        ( Script_ir_translator.unparse_ty ~loc:Micheline.dummy_location ctxt tp
-        >>? fun (ty, ctxt) ->
-          let unparsed_parameters =
-            Micheline.Seq (Micheline.dummy_location, [unparsed_parameters; ty])
-          in
-          Gas.consume ctxt (Script.strip_locations_cost unparsed_parameters)
-          >|? fun ctxt ->
-          let unparsed_parameters =
-            Micheline.strip_locations unparsed_parameters
-          in
-          ( Transaction_to_tx_rollup
-              {destination; parameters_ty; parameters; unparsed_parameters},
-            ctxt ) )
-  | _ ->
-      (* TODO: https://gitlab.com/tezos/tezos/-/issues/2455
-         Refute this branch thanks to the type system.
-         Thanks to the implementation of the [CONTRACT]
-         instruction, this branch is unreachable. But this is
-         not enforced by the type system, which means we are one
-         refactoring away to reach it. *)
-      assert false
+  let (Pair_t (Ticket_t (tp, _), _, _, _)) = parameters_ty in
+  unparse_data ctxt Optimized parameters_ty parameters
+  >>=? fun (unparsed_parameters, ctxt) ->
+  Lwt.return
+    ( Script_ir_translator.unparse_ty ~loc:Micheline.dummy_location ctxt tp
+    >>? fun (ty, ctxt) ->
+      let unparsed_parameters =
+        Micheline.Seq (Micheline.dummy_location, [unparsed_parameters; ty])
+      in
+      Gas.consume ctxt (Script.strip_locations_cost unparsed_parameters)
+      >|? fun ctxt ->
+      let unparsed_parameters = Micheline.strip_locations unparsed_parameters in
+      ( Transaction_to_tx_rollup
+          {destination; parameters_ty; parameters; unparsed_parameters},
+        ctxt ) )
 
 let make_transaction_to_sc_rollup ctxt ~destination ~amount ~entrypoint
     ~parameters_ty ~parameters =
-- 
GitLab