diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
index e45390cbba735b7bdcea382cbf4c0ba39f90726c..b522cca91740dc694785aff653a4cfabe123dc7c 100644
--- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml
+++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
@@ -538,8 +538,10 @@ 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})
+      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 :
         type arg argc.
@@ -550,8 +552,10 @@ 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})
+      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 :
         type arg argc.
@@ -578,8 +582,10 @@ 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})
+            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, _, _) ->
           let* b = Base_samplers.uniform_bool in
@@ -587,8 +593,10 @@ 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})
+            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/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli
index ec0a6a33a99216c02dcf15e01b82cba13e8f7f03..462b29885ef4c1580d13a3a298e73ce3f071e4af 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
 
diff --git a/src/proto_alpha/lib_protocol/cache_memory_helpers.ml b/src/proto_alpha/lib_protocol/cache_memory_helpers.ml
index 45c1ec4c1dfea94326a102fc8fe2f549602ec11e..137f19977931b5f69d09ab3c9cfad8aeac6d7bd4 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 20045646df690fe5c0afcf1436361b5434357fe2..e1073e1253d94346012a10dbd1fe14a8c360fa0f 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
diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml
index deeddb0b3e902ac39bbbbe1b303c3ab0b4942b39..f57b42b8efea904fdb56e0261f0a32a816380312 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter.ml
@@ -1101,7 +1101,9 @@ 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 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) -> (
           let addr = accu in
@@ -1126,21 +1128,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 = Typed_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])
@@ -1221,9 +1226,8 @@ 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 address = {destination; entrypoint} in
-          let res = Typed_contract {arg_ty = ty; address} 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) ->
           let destination : Destination.t = Contract (Originated sc.self) in
diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
index d18d1a8927e54903b43e0a8a66672975f3d1d033..ff12b7e053ffca060f7dd0d35c52ed5d79637c9f 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
@@ -464,42 +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_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 =
+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
@@ -517,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 =
@@ -586,8 +542,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) ->
@@ -602,16 +559,47 @@ 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
-  | Tx_rollup destination ->
+  | Typed_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 ) )
+  | Typed_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 ) )
+  | Typed_tx_rollup destination ->
       make_transaction_to_tx_rollup
         ctxt
         ~destination
@@ -619,7 +607,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
diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index 951bf1470c088cb6fd3616fc2b62d4a9e905b885..60392a0046fb0b335a6db30dfcc7b19be50e762e 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml
@@ -373,7 +373,10 @@ 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 destination = Typed_destination.untyped destination in
+  let address = {destination; entrypoint} in
   unparse_address ~loc ctxt mode address
 
 let unparse_signature ~loc ctxt mode s =
@@ -2480,7 +2483,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
@@ -4918,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. *)
@@ -4926,12 +4929,13 @@ 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} )
+               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) ->
@@ -4967,8 +4971,8 @@ 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} )) ))
+                      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 ->
       if Entrypoint.(entrypoint = Tx_rollup.deposit_entrypoint) then
@@ -4976,8 +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, _, _) ->
-            let address = {destination; entrypoint} in
-            (ctxt, ok @@ Typed_contract {arg_ty = arg; address})
+            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))
@@ -5015,8 +5022,8 @@ 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} ))
+              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
    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 66aa00a23b185e3be8579a88c7386d499e775800..9cc3a94ac81b429a89f943f2435f09e0242093df 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml
@@ -1110,10 +1110,19 @@ 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;
-      address : address;
+      destination : 'arg typed_destination;
+      entrypoint : Entrypoint.t;
     }
       -> 'arg typed_contract
 
@@ -2146,3 +2155,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 5dbff914eb23fd8966db96e24f8447142a93b449..da95bffff5f176f8a47c1d9cb0c2375874b116eb 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli
@@ -1111,10 +1111,19 @@ 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;
-      address : address;
+      destination : 'arg typed_destination;
+      entrypoint : Entrypoint.t;
     }
       -> 'arg typed_contract
 
@@ -1752,3 +1761,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
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 6a1fd023693fa50820fe161932eee1db22cc1026..10df0d4193ffbff44830fd3fece66cb1bfa1cddf 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
 
@@ -179,8 +185,12 @@ 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
+    +! 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 f8b6638f0a0798831a25d19d57679978bb83dc96..d7c2e129a24ec2b6d40112a61b5558ab7f64c842 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,9 @@ 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}) =
+         let destination = Typed_destination.untyped destination in
+         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 e1c7060734b0063674161adf2f4ba605c8aaf766..4004172feb9f49d5ee25eea0315bd91322adefc9 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
@@ -807,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
@@ -830,7 +828,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
@@ -842,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
@@ -853,7 +852,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
@@ -862,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