Skip to main content

🍬 Script_typed_ir_size.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_set.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.

Include Cache_memory_helpers.

Definition script_string_size (s_value : Script_string.t) : Saturation_repr.t :=
  string_size (Script_string.to_string s_value).

Definition ty_traverse_f : Script_typed_ir.ty_traverse nodes_and_size :=
  let base_basic := op_exclamationexclamation 0 in
  let base_compound_no_meta := header_size in
  let base_compound {A : Set} (_meta : A) : Saturation_repr.t :=
    h1w in
  let apply (accu_value : nodes_and_size) (ty_value : Script_typed_ir.ty)
    : nodes_and_size :=
    match ty_value with
    | Script_typed_ir.Unit_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Int_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Nat_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Signature_tret_succ_adding accu_value base_basic
    | Script_typed_ir.String_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Bytes_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Mutez_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Key_hash_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Key_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Timestamp_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Address_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Tx_rollup_l2_address_t
      ret_succ_adding accu_value base_basic
    | Script_typed_ir.Bool_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Operation_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Chain_id_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Never_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Bls12_381_g1_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Bls12_381_g2_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Bls12_381_fr_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Chest_key_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Chest_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Pair_t _ty1 _ty2 a_value _
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 3))
    | Script_typed_ir.Union_t _ty1 _ty2 a_value _
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 3))
    | Script_typed_ir.Lambda_t _ty1 _ty2 a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.Option_t _ty a_value _
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.List_t _ty a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value) word_size)
    | Script_typed_ir.Set_t _cty a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value) word_size)
    | Script_typed_ir.Map_t _cty _ty a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.Big_map_t _cty _ty a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.Contract_t _ty a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value) word_size)
    | Script_typed_ir.Sapling_transaction_t m_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation base_compound_no_meta
            (Alpha_context.Sapling.Memo_size.in_memory_size m_value)) word_size)
    | Script_typed_ir.Sapling_transaction_deprecated_t m_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation base_compound_no_meta
            (Alpha_context.Sapling.Memo_size.in_memory_size m_value)) word_size)
    | Script_typed_ir.Sapling_state_t m_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation base_compound_no_meta
            (Alpha_context.Sapling.Memo_size.in_memory_size m_value)) word_size)
    | Script_typed_ir.Ticket_t _cty a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value) word_size)
    end in
  {| Script_typed_ir.ty_traverse.apply := apply; |}.

Definition ty_size (ty_value : Script_typed_ir.ty) : nodes_and_size :=
  Script_typed_ir.ty_traverse_value ty_value zero ty_traverse_f.

Definition ty_for_logging_size (_ty : option Script_typed_ir.ty) : sint :=
  op_exclamationexclamation 0.

Definition stack_ty_size (s_value : Script_typed_ir.stack_ty)
  : nodes_and_size :=
  let apply (accu_value : nodes_and_size) (s_value : Script_typed_ir.stack_ty)
    : nodes_and_size :=
    match s_value with
    | Script_typed_ir.Bot_tret_succ accu_value
    | Script_typed_ir.Item_t ty_value _
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value)) h2w
    end in
  Script_typed_ir.stack_ty_traverse_value s_value zero
    {| Script_typed_ir.stack_ty_traverse.apply := apply; |}.

Definition stack_ty_for_logging_size
  (function_parameter : option Script_typed_ir.stack_ty) : sint :=
  let '_ := function_parameter in
  op_exclamationexclamation 0.

Definition script_nat_size (n_value : Script_int.num) : Saturation_repr.t :=
  z_size (Script_int.to_zint n_value).

Definition script_int_size (n_value : Script_int.num) : Saturation_repr.t :=
  z_size (Script_int.to_zint n_value).

Definition signature_size : Saturation_repr.t := op_exclamationexclamation 96.

Definition key_hash_size (_x : Signature.public_key_hash) : Saturation_repr.t :=
  op_exclamationexclamation 64.

Definition public_key_size (x_value : Alpha_context.public_key)
  : Saturation_repr.t :=
  op_plusquestion h1w
    match x_value with
    | Signature.Ed25519 _ ⇒ 64
    | Signature.Secp256k1 _ ⇒ 72
    | Signature.P256 _ ⇒ 96
    end.

Definition mutez_size : Saturation_repr.t := h2w.

Definition timestamp_size (x_value : Script_timestamp.t) : Saturation_repr.t :=
  z_size (Script_timestamp.to_zint x_value).

Definition destination_size
  : Alpha_context.Destination.t Cache_memory_helpers.sint :=
  Alpha_context.Destination.in_memory_size.

Definition address_size (addr : Script_typed_ir.address) : Saturation_repr.t :=
  op_plusexclamation
    (op_plusexclamation h2w
      (destination_size addr.(Script_typed_ir.address.destination)))
    (Alpha_context.Entrypoint.in_memory_size
      addr.(Script_typed_ir.address.entrypoint)).

Definition tx_rollup_l2_address_size (tx : Script_typed_ir.tx_rollup_l2_address)
  : Cache_memory_helpers.sint :=
  Tx_rollup_l2_address.Indexable.in_memory_size (Indexable.forget tx).

Definition view_signature_size
  (function_parameter : Script_typed_ir.view_signature)
  : int × Saturation_repr.t :=
  let
    'Script_typed_ir.View_signature {|
      Script_typed_ir.view_signature.View_signature.name := name;
        Script_typed_ir.view_signature.View_signature.input_ty := input_ty;
        Script_typed_ir.view_signature.View_signature.output_ty := output_ty
        |} := function_parameter in
  ret_adding (op_plusplus (ty_size input_ty) (ty_size output_ty))
    (op_plusexclamation h3w (script_string_size name)).

Definition script_expr_hash_size : Saturation_repr.t :=
  op_exclamationexclamation 64.

Fixpoint stack_prefix_preservation_witness_size_internal
  (function_parameter : Script_typed_ir.stack_prefix_preservation_witness)
  : nodes_and_size :=
  match function_parameter with
  | Script_typed_ir.KPrefix _loc ty_value w_value
    ret_succ_adding
      (op_plusplus (ty_size ty_value)
        (stack_prefix_preservation_witness_size_internal w_value)) h3w
  | Script_typed_ir.KRestzero
  end.

Definition stack_prefix_preservation_witness_size
  (_n : int) (w_value : Script_typed_ir.stack_prefix_preservation_witness)
  : nodes_and_size := stack_prefix_preservation_witness_size_internal w_value.

Definition peano_shape_proof : int Saturation_repr.t :=
  let scale := op_plusexclamation header_size h1w in
  fun (k_value : int) ⇒ op_starquestion scale k_value.

Definition comb_gadt_witness_size
  (n_value : int) (_w : Script_typed_ir.comb_gadt_witness)
  : Saturation_repr.t := peano_shape_proof n_value.

Definition uncomb_gadt_witness_size
  (n_value : int) (_w : Script_typed_ir.uncomb_gadt_witness)
  : Saturation_repr.t := peano_shape_proof n_value.

Definition comb_get_gadt_witness_size
  (n_value : int) (_w : Script_typed_ir.comb_get_gadt_witness)
  : Saturation_repr.t := peano_shape_proof n_value.

Definition comb_set_gadt_witness_size
  (n_value : int) (_w : Script_typed_ir.comb_set_gadt_witness)
  : Saturation_repr.t := peano_shape_proof n_value.

Definition dup_n_gadt_witness_size
  (n_value : int) (_w : Script_typed_ir.dup_n_gadt_witness)
  : Saturation_repr.t := peano_shape_proof n_value.

Definition contract_size (function_parameter : Script_typed_ir.typed_contract)
  : nodes_and_size :=
  match function_parameter with
  | Script_typed_ir.Typed_implicit _
    ret_adding zero (op_plusexclamation h1w public_key_hash_in_memory_size)
  |
    Script_typed_ir.Typed_originated {|
      Script_typed_ir.typed_contract.Typed_originated.arg_ty := arg_ty;
        Script_typed_ir.typed_contract.Typed_originated.contract_hash := _;
        Script_typed_ir.typed_contract.Typed_originated.entrypoint := entrypoint
        |} ⇒
    ret_adding (ty_size arg_ty)
      (op_plusexclamation (op_plusexclamation h3w blake2b_hash_size)
        (Alpha_context.Entrypoint.in_memory_size entrypoint))
  |
    Script_typed_ir.Typed_tx_rollup {|
      Script_typed_ir.typed_contract.Typed_tx_rollup.arg_ty := arg_ty;
        Script_typed_ir.typed_contract.Typed_tx_rollup.tx_rollup := tx_rollup
        |} ⇒
    ret_adding (ty_size arg_ty)
      (op_plusexclamation h2w (Alpha_context.Tx_rollup.in_memory_size tx_rollup))
  |
    Script_typed_ir.Typed_sc_rollup {|
      Script_typed_ir.typed_contract.Typed_sc_rollup.arg_ty := arg_ty;
        Script_typed_ir.typed_contract.Typed_sc_rollup.sc_rollup := sc_rollup;
        Script_typed_ir.typed_contract.Typed_sc_rollup.entrypoint := entrypoint
        |} ⇒
    ret_adding (ty_size arg_ty)
      (op_plusexclamation
        (op_plusexclamation h3w
          (Alpha_context.Sc_rollup.in_memory_size sc_rollup))
        (Alpha_context.Entrypoint.in_memory_size entrypoint))
  |
    Script_typed_ir.Typed_zk_rollup {|
      Script_typed_ir.typed_contract.Typed_zk_rollup.arg_ty := arg_ty;
        Script_typed_ir.typed_contract.Typed_zk_rollup.zk_rollup := zk_rollup
        |} ⇒
    ret_adding (ty_size arg_ty)
      (op_plusexclamation h2w (Alpha_context.Zk_rollup.in_memory_size zk_rollup))
  end.

Definition sapling_state_size (function_parameter : Alpha_context.Sapling.state)
  : Saturation_repr.t :=
  let '{|
    Alpha_context.Sapling.state.id := id;
      Alpha_context.Sapling.state.diff := diff_value;
      Alpha_context.Sapling.state.memo_size := memo_size
      |} := function_parameter in
  op_plusexclamation
    (op_plusexclamation
      (op_plusexclamation h3w
        (option_size
          (fun (x_value : Alpha_context.Sapling.Id.t) ⇒
            z_size (Alpha_context.Sapling.Id.unparse_to_z x_value)) id))
      (Alpha_context.Sapling.diff_in_memory_size diff_value))
    (Alpha_context.Sapling.Memo_size.in_memory_size memo_size).

Definition chain_id_size : Saturation_repr.t := op_exclamationexclamation 16.

Definition ticket_size {A : Set} (function_parameter : Script_typed_ir.ticket A)
  : Saturation_repr.t :=
  let '{|
    Script_typed_ir.ticket.ticketer := ticketer;
      Script_typed_ir.ticket.contents := _;
      Script_typed_ir.ticket.amount := amount
      |} := function_parameter in
  op_plusexclamation
    (op_plusexclamation h3w (Alpha_context.Contract.in_memory_size ticketer))
    (script_nat_size amount).

Definition chest_size (chest_value : Script_typed_ir.Script_timelock.chest)
  : Saturation_repr.t :=
  let locked_value_size := 256 in
  let rsa_public_size := 256 in
  let ciphertext_size :=
    Script_typed_ir.Script_timelock.get_plaintext_size chest_value in
  op_plusquestion h3w
    ((locked_value_size +i rsa_public_size) +i ciphertext_size).

Definition chest_key_size {A : Set} (function_parameter : A)
  : Saturation_repr.t :=
  let '_ := function_parameter in
  let unlocked_value_size := 256 in
  let proof_size := 256 in
  op_plusquestion h2w (unlocked_value_size +i proof_size).

Reserved Notation "'big_map_size_aux".
Reserved Notation "'kdescr_size_aux".

#[bypass_check(guard)]
Fixpoint value_size_aux {a : Set}
  (count_lambda_nodes : bool) (accu_value : nodes_and_size)
  (ty_value : Script_typed_ir.ty) (x_value : a) {struct ty_value}
  : nodes_and_size :=
  let big_map_size_aux := 'big_map_size_aux in
  let apply {a : Set}
    (accu_value : nodes_and_size) (ty_value : Script_typed_ir.ty) (x_value : a)
    : nodes_and_size :=
    match (ty_value, x_value) with
    | (Script_typed_ir.Unit_t, _)ret_succ accu_value
    | (Script_typed_ir.Int_t, x_value)
      let x_value := cast Script_int.num x_value in
      ret_succ_adding accu_value (script_int_size x_value)
    | (Script_typed_ir.Nat_t, x_value)
      let x_value := cast Script_int.num x_value in
      ret_succ_adding accu_value (script_nat_size x_value)
    | (Script_typed_ir.Signature_t, _)
      ret_succ_adding accu_value signature_size
    | (Script_typed_ir.String_t, x_value)
      let x_value := cast Script_string.t x_value in
      ret_succ_adding accu_value (script_string_size x_value)
    | (Script_typed_ir.Bytes_t, x_value)
      let x_value := cast bytes x_value in
      ret_succ_adding accu_value (bytes_size x_value)
    | (Script_typed_ir.Mutez_t, _)ret_succ_adding accu_value mutez_size
    | (Script_typed_ir.Key_hash_t, x_value)
      let x_value := cast Alpha_context.public_key_hash x_value in
      ret_succ_adding accu_value (key_hash_size x_value)
    | (Script_typed_ir.Key_t, x_value)
      let x_value := cast Alpha_context.public_key x_value in
      ret_succ_adding accu_value (public_key_size x_value)
    | (Script_typed_ir.Timestamp_t, x_value)
      let x_value := cast Script_timestamp.t x_value in
      ret_succ_adding accu_value (timestamp_size x_value)
    | (Script_typed_ir.Address_t, x_value)
      let x_value := cast Script_typed_ir.address x_value in
      ret_succ_adding accu_value (address_size x_value)
    | (Script_typed_ir.Tx_rollup_l2_address_t, x_value)
      let x_value := cast Script_typed_ir.tx_rollup_l2_address x_value in
      ret_succ_adding accu_value (tx_rollup_l2_address_size x_value)
    | (Script_typed_ir.Bool_t, _)ret_succ accu_value
    | (Script_typed_ir.Pair_t _ _ _ _, _)ret_succ_adding accu_value h2w
    | (Script_typed_ir.Union_t _ _ _ _, _)ret_succ_adding accu_value h1w
    | (Script_typed_ir.Lambda_t _ _ _, x_value)
      let x_value := cast Script_typed_ir.lambda x_value in
      lambda_size_aux count_lambda_nodes (ret_succ accu_value) x_value
    | (Script_typed_ir.Option_t _ _ _, x_value)
      let 'existT _ __6 x_value :=
        cast_exists (Es := Set) (fun __6option __6) x_value in
      ret_succ_adding accu_value
        (option_size
          (fun (function_parameter : __6) ⇒
            let '_ := function_parameter in
            op_exclamationexclamation 0) x_value)
    | (Script_typed_ir.List_t _ _, x_value)
      let 'existT _ __7 x_value :=
        cast_exists (Es := Set) (fun __7Script_list.t __7) x_value in
      ret_succ_adding accu_value
        (op_plusexclamation h2w
          (op_starquestion h2w x_value.(Script_list.t.length)))
    | (Script_typed_ir.Set_t _ _, x_value)
      let 'existT _ __8 x_value :=
        cast_exists (Es := Set) (fun __8Script_typed_ir.set __8) x_value in
      let set := Script_set.get x_value in
      let 'existS _ _ M := set in
      let boxing_space := op_exclamationexclamation 536 in
      ret_succ_adding accu_value
        (op_plusexclamation boxing_space
          (op_starquestion h4w M.(Script_typed_ir.Boxed_set.size_value)))
    | (Script_typed_ir.Map_t _ _ _, x_value)
      let 'existT _ [__9, __10] x_value :=
        cast_exists (Es := [Set ** Set])
          (fun '[__9, __10]Script_typed_ir.map __9 __10) x_value in
      let map := Script_map.get_module x_value in
      let 'existS _ _ M := map in
      let boxing_space := op_exclamationexclamation 696 in
      ret_succ_adding accu_value
        (op_plusexclamation boxing_space
          (op_starquestion h5w M.(Script_typed_ir.Boxed_map.size_value)))
    | (Script_typed_ir.Big_map_t cty ty' _, x_value)
      let '[x_value, ty', cty] :=
        cast
          [Script_typed_ir.big_map ** Script_typed_ir.ty **
            Script_typed_ir.comparable_ty] [x_value, ty', cty] in
      big_map_size_aux count_lambda_nodes (ret_succ accu_value) cty ty' x_value
    | (Script_typed_ir.Contract_t _ _, x_value)
      let x_value := cast Script_typed_ir.typed_contract x_value in
      ret_succ (op_plusplus accu_value (contract_size x_value))
    | (Script_typed_ir.Sapling_transaction_t _, x_value)
      let x_value := cast Alpha_context.Sapling.transaction x_value in
      ret_succ_adding accu_value
        (Alpha_context.Sapling.transaction_in_memory_size x_value)
    | (Script_typed_ir.Sapling_transaction_deprecated_t _, x_value)
      let x_value := cast Sapling_repr.legacy_transaction x_value in
      ret_succ_adding accu_value
        (Alpha_context.Sapling.Legacy.transaction_in_memory_size x_value)
    | (Script_typed_ir.Sapling_state_t _, x_value)
      let x_value := cast Alpha_context.Sapling.state x_value in
      ret_succ_adding accu_value (sapling_state_size x_value)
    | (Script_typed_ir.Operation_t, _)
      (* ❌ Assert instruction is not handled. *)
      assert nodes_and_size false
    | (Script_typed_ir.Chain_id_t, _)
      ret_succ_adding accu_value chain_id_size
    | (Script_typed_ir.Bls12_381_g1_t, _)
      ret_succ_adding accu_value
        (op_exclamationexclamation Bls.Primitive.G1.(S.CURVE.size_in_memory))
    | (Script_typed_ir.Bls12_381_g2_t, _)
      ret_succ_adding accu_value
        (op_exclamationexclamation Bls.Primitive.G2.(S.CURVE.size_in_memory))
    | (Script_typed_ir.Bls12_381_fr_t, _)
      ret_succ_adding accu_value
        (op_exclamationexclamation
          Bls.Primitive.Fr.(S.PRIME_FIELD.size_in_memory))
    | (Script_typed_ir.Ticket_t _ _, x_value)
      let 'existT _ __14 x_value :=
        cast_exists (Es := Set) (fun __14Script_typed_ir.ticket __14)
          x_value in
      ret_succ_adding accu_value (ticket_size x_value)
    | (Script_typed_ir.Chest_key_t, x_value)
      let x_value := cast Script_typed_ir.Script_timelock.chest_key x_value in
      ret_succ_adding accu_value (chest_key_size x_value)
    | (Script_typed_ir.Chest_t, x_value)
      let x_value := cast Script_typed_ir.Script_timelock.chest x_value in
      ret_succ_adding accu_value (chest_size x_value)
    | _unreachable_gadt_branch
    end in
  Script_typed_ir.value_traverse_value ty_value x_value accu_value
    {| Script_typed_ir.value_traverse.apply _ := apply; |}

with lambda_size_aux
  (count_lambda_nodes : bool) (accu_value : nodes_and_size)
  (lam : Script_typed_ir.lambda) {struct lam} : nodes_and_size :=
  let kdescr_size_aux := 'kdescr_size_aux in
  let count_lambda_body {A B : Set}
    (kdescr : Script_typed_ir.kdescr) (node_value : Micheline.node A B)
    : nodes_and_size :=
    let accu_value :=
      ret_adding
        (op_plusplus accu_value
          (if count_lambda_nodes then
            node_size node_value
          else
            zero)) h2w in
    kdescr_size_aux false accu_value kdescr in
  match lam with
  | Script_typed_ir.Lam kdescr node_valuecount_lambda_body kdescr node_value
  | Script_typed_ir.LamRec kdescr node_value
    count_lambda_body kdescr node_value
  end

with kinstr_size_aux
  (count_lambda_nodes : bool) (accu_value : nodes_and_size)
  (t_value : Script_typed_ir.kinstr) {struct t_value} : nodes_and_size :=
  let base0 (_loc : Alpha_context.Script.location) : Saturation_repr.t :=
    h1w in
  let base1 (_loc : Alpha_context.Script.location) (_k : Script_typed_ir.kinstr)
    : Saturation_repr.t :=
    h2w in
  let base2
    (_loc : Alpha_context.Script.location) (_k1 : Script_typed_ir.kinstr)
    (_k2 : Script_typed_ir.kinstr) : Saturation_repr.t :=
    h3w in
  let base3
    (_loc : Alpha_context.Script.location) (_k1 : Script_typed_ir.kinstr)
    (_k2 : Script_typed_ir.kinstr) (_k3 : Script_typed_ir.kinstr)
    : Saturation_repr.t :=
    h4w in
  let apply (accu_value : nodes_and_size) (t_value : Script_typed_ir.kinstr)
    : nodes_and_size :=
    match t_value with
    | Script_typed_ir.IDrop loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IDup loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISwap loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IConst loc_value ty_value x_value k_value
      let accu_value :=
        ret_succ_adding accu_value
          (op_plusexclamation (base1 loc_value k_value)
            (op_starquestion word_size 2)) in
      value_size_aux count_lambda_nodes
        (op_plusplus accu_value (ty_size ty_value)) ty_value x_value
    | Script_typed_ir.ICons_pair loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ICar loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ICdr loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IUnpair loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ICons_some loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ICons_none loc_value ty_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    |
      Script_typed_ir.IIf_none {|
        Script_typed_ir.kinstr.IIf_none.loc := loc_value;
          Script_typed_ir.kinstr.IIf_none.branch_if_none := k1;
          Script_typed_ir.kinstr.IIf_none.branch_if_some := k2;
          Script_typed_ir.kinstr.IIf_none.k := k3
          |} ⇒ ret_succ_adding accu_value (base3 loc_value k1 k2 k3)
    |
      Script_typed_ir.IOpt_map {|
        Script_typed_ir.kinstr.IOpt_map.loc := loc_value;
          Script_typed_ir.kinstr.IOpt_map.body := k1;
          Script_typed_ir.kinstr.IOpt_map.k := k2
          |} ⇒ ret_succ_adding accu_value (base2 loc_value k1 k2)
    | Script_typed_ir.ICons_left loc_value ty_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    | Script_typed_ir.ICons_right loc_value ty_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    |
      Script_typed_ir.IIf_left {|
        Script_typed_ir.kinstr.IIf_left.loc := loc_value;
          Script_typed_ir.kinstr.IIf_left.branch_if_left := k1;
          Script_typed_ir.kinstr.IIf_left.branch_if_right := k2;
          Script_typed_ir.kinstr.IIf_left.k := k3
          |} ⇒ ret_succ_adding accu_value (base3 loc_value k1 k2 k3)
    | Script_typed_ir.ICons_list loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INil loc_value ty_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    |
      Script_typed_ir.IIf_cons {|
        Script_typed_ir.kinstr.IIf_cons.loc := loc_value;
          Script_typed_ir.kinstr.IIf_cons.branch_if_cons := k2;
          Script_typed_ir.kinstr.IIf_cons.branch_if_nil := k1;
          Script_typed_ir.kinstr.IIf_cons.k := k3
          |} ⇒ ret_succ_adding accu_value (base3 loc_value k1 k2 k3)
    | Script_typed_ir.IList_map loc_value k1 ty_value k2
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base2 loc_value k1 k2)
            (ty_for_logging_size ty_value)) word_size)
    | Script_typed_ir.IList_iter loc_value ty_value k1 k2
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base2 loc_value k1 k2)
            (ty_for_logging_size ty_value)) word_size)
    | Script_typed_ir.IList_size loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IEmpty_set loc_value cty k_value
      ret_succ_adding (op_plusplus accu_value (ty_size cty))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    | Script_typed_ir.ISet_iter loc_value ty_value k1 k2
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base2 loc_value k1 k2)
            (ty_for_logging_size ty_value)) word_size)
    | Script_typed_ir.ISet_mem loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISet_update loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISet_size loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IEmpty_map loc_value cty vty k_value
      ret_succ_adding (op_plusplus accu_value (ty_size cty))
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (ty_for_logging_size vty)) (op_starquestion word_size 2))
    | Script_typed_ir.IMap_map loc_value ty_value k1 k2
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base2 loc_value k1 k2)
            (ty_for_logging_size ty_value)) word_size)
    | Script_typed_ir.IMap_iter loc_value kvty k1 k2
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base2 loc_value k1 k2) (ty_for_logging_size kvty))
          word_size)
    | Script_typed_ir.IMap_mem loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMap_get loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMap_update loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMap_get_and_update loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMap_size loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IEmpty_big_map loc_value cty ty_value k_value
      ret_succ_adding
        (op_plusplus (op_plusplus accu_value (ty_size cty)) (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.IBig_map_mem loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IBig_map_get loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IBig_map_update loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IBig_map_get_and_update loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IConcat_string loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IConcat_string_pair loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISlice_string loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IString_size loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IConcat_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IConcat_bytes_pair loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISlice_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IBytes_size loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ILsl_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ILsr_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IOr_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAnd_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IXor_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INot_bytes loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_seconds_to_timestamp loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_timestamp_to_seconds loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISub_timestamp_seconds loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IDiff_timestamps loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_tez loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISub_tez loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISub_tez_legacy loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_teznat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_nattez loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IEdiv_teznat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IEdiv_tez loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IOr loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAnd loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IXor loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INot loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IIs_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INeg loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAbs_int loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IInt_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_int loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISub_int loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_int loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IEdiv_int loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IEdiv_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ILsl_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ILsr_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IOr_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAnd_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAnd_int_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IXor_nat loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INot_int loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    |
      Script_typed_ir.IIf {|
        Script_typed_ir.kinstr.IIf.loc := loc_value;
          Script_typed_ir.kinstr.IIf.branch_if_true := k1;
          Script_typed_ir.kinstr.IIf.branch_if_false := k2;
          Script_typed_ir.kinstr.IIf.k := k3
          |} ⇒ ret_succ_adding accu_value (base3 loc_value k1 k2 k3)
    | Script_typed_ir.ILoop loc_value k1 k2
      ret_succ_adding accu_value (base2 loc_value k1 k2)
    | Script_typed_ir.ILoop_left loc_value k1 k2
      ret_succ_adding accu_value (base2 loc_value k1 k2)
    | Script_typed_ir.IDip loc_value k1 ty_value k2
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base2 loc_value k1 k2)
            (ty_for_logging_size ty_value)) word_size)
    | Script_typed_ir.IExec loc_value sty k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (stack_ty_for_logging_size sty)) word_size)
    | Script_typed_ir.IApply loc_value ty_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    | Script_typed_ir.ILambda loc_value lambda k_value
      let accu_value :=
        ret_succ_adding accu_value
          (op_plusexclamation (base1 loc_value k_value) word_size) in
      lambda_size_aux count_lambda_nodes accu_value lambda
    | Script_typed_ir.IFailwith loc_value ty_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base0 loc_value) word_size)
    | Script_typed_ir.ICompare loc_value cty k_value
      ret_succ_adding (op_plusplus accu_value (ty_size cty))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    | Script_typed_ir.IEq loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INeq loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ILt loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IGt loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ILe loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IGe loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAddress loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IContract loc_value ty_value s_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (Alpha_context.Entrypoint.in_memory_size s_value))
          (op_starquestion word_size 2))
    | Script_typed_ir.IView loc_value s_value sty k_value
      ret_succ_adding (op_plusplus accu_value (view_signature_size s_value))
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (stack_ty_for_logging_size sty)) (op_starquestion word_size 2))
    | Script_typed_ir.ITransfer_tokens loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IImplicit_account loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    |
      Script_typed_ir.ICreate_contract {|
        Script_typed_ir.kinstr.ICreate_contract.loc := loc_value;
          Script_typed_ir.kinstr.ICreate_contract.storage_type := storage_type;
          Script_typed_ir.kinstr.ICreate_contract.code := code;
          Script_typed_ir.kinstr.ICreate_contract.k := k_value
          |} ⇒
      ret_succ_adding
        (op_plusplus (op_plusplus accu_value (ty_size storage_type))
          (expr_size code))
        (op_plusexclamation (base1 loc_value k_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.ISet_delegate loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INow loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMin_block_time loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IBalance loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ILevel loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ICheck_signature loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IHash_key loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IPack loc_value ty_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    | Script_typed_ir.IUnpack loc_value ty_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    | Script_typed_ir.IBlake2b loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISha256 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISha512 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISource loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISender loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISelf loc_value ty_value s_value k_value
      ret_succ_adding (op_plusplus accu_value (ty_size ty_value))
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (op_starquestion word_size 2))
          (Alpha_context.Entrypoint.in_memory_size s_value))
    | Script_typed_ir.ISelf_address loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAmount loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISapling_empty_state loc_value m_value k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value) word_size)
          (Alpha_context.Sapling.Memo_size.in_memory_size m_value))
    | Script_typed_ir.ISapling_verify_update loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISapling_verify_update_deprecated loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IDig loc_value n_value w_value k_value
      ret_succ_adding
        (op_plusplus accu_value
          (stack_prefix_preservation_witness_size n_value w_value))
        (op_plusexclamation (base1 loc_value k_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.IDug loc_value n_value w_value k_value
      ret_succ_adding
        (op_plusplus accu_value
          (stack_prefix_preservation_witness_size n_value w_value))
        (op_plusexclamation (base1 loc_value k_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.IDipn loc_value n_value w_value k1 k2
      ret_succ_adding
        (op_plusplus accu_value
          (stack_prefix_preservation_witness_size n_value w_value))
        (op_plusexclamation (base2 loc_value k1 k2)
          (op_starquestion word_size 2))
    | Script_typed_ir.IDropn loc_value n_value w_value k_value
      ret_succ_adding
        (op_plusplus accu_value
          (stack_prefix_preservation_witness_size n_value w_value))
        (op_plusexclamation (base1 loc_value k_value)
          (op_starquestion word_size 2))
    | Script_typed_ir.IChainId loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INever loc_value
      ret_succ_adding accu_value (base0 loc_value)
    | Script_typed_ir.IVoting_power loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ITotal_voting_power loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IKeccak loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.ISha3 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_bls12_381_g1 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_bls12_381_g2 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IAdd_bls12_381_fr loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_bls12_381_g1 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_bls12_381_g2 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_bls12_381_fr loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_bls12_381_z_fr loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IMul_bls12_381_fr_z loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IInt_bls12_381_fr loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INeg_bls12_381_g1 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INeg_bls12_381_g2 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.INeg_bls12_381_fr loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IPairing_check_bls12_381 loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IComb loc_value n_value w_value k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (op_starquestion word_size 2))
          (comb_gadt_witness_size n_value w_value))
    | Script_typed_ir.IUncomb loc_value n_value w_value k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (op_starquestion word_size 2))
          (uncomb_gadt_witness_size n_value w_value))
    | Script_typed_ir.IComb_get loc_value n_value w_value k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (op_starquestion word_size 2))
          (comb_get_gadt_witness_size n_value w_value))
    | Script_typed_ir.IComb_set loc_value n_value w_value k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (op_starquestion word_size 2))
          (comb_set_gadt_witness_size n_value w_value))
    | Script_typed_ir.IDup_n loc_value n_value w_value k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (op_starquestion word_size 2))
          (dup_n_gadt_witness_size n_value w_value))
    | Script_typed_ir.ITicket loc_value cty k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (ty_for_logging_size cty)) word_size)
    | Script_typed_ir.ITicket_deprecated loc_value cty k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (ty_for_logging_size cty)) word_size)
    | Script_typed_ir.IRead_ticket loc_value ty_value k_value
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (ty_for_logging_size ty_value)) word_size)
    | Script_typed_ir.ISplit_ticket loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    | Script_typed_ir.IJoin_tickets loc_value cty k_value
      ret_succ_adding (op_plusplus accu_value (ty_size cty))
        (op_plusexclamation (base1 loc_value k_value) word_size)
    | Script_typed_ir.IOpen_chest loc_value k_value
      ret_succ_adding accu_value (base1 loc_value k_value)
    |
      Script_typed_ir.IEmit {|
        Script_typed_ir.kinstr.IEmit.loc := loc_value;
          Script_typed_ir.kinstr.IEmit.tag := tag;
          Script_typed_ir.kinstr.IEmit.ty := ty_value;
          Script_typed_ir.kinstr.IEmit.unparsed_ty := unparsed_ty;
          Script_typed_ir.kinstr.IEmit.k := k_value
          |} ⇒
      ret_succ_adding
        (op_plusplus (op_plusplus accu_value (ty_size ty_value))
          (expr_size unparsed_ty))
        (op_plusexclamation
          (op_plusexclamation (base1 loc_value k_value)
            (Alpha_context.Entrypoint.in_memory_size tag))
          (op_starquestion word_size 3))
    | Script_typed_ir.IHalt loc_value
      ret_succ_adding accu_value (base0 loc_value)
    | Script_typed_ir.ILog _ _ _ _ _accu_value
    end in
  Script_typed_ir.kinstr_traverse_value t_value accu_value
    {| Script_typed_ir.kinstr_traverse.apply := apply; |}

where "'big_map_size_aux" :=
  (fun
    (count_lambda_nodes : bool) (accu_value : nodes_and_size)
    (cty : Script_typed_ir.comparable_ty) (ty' : Script_typed_ir.ty)
    (function_parameter : Script_typed_ir.big_map) ⇒
    let
      'Script_typed_ir.Big_map {|
        Script_typed_ir.big_map.Big_map.id := id;
          Script_typed_ir.big_map.Big_map.diff := diff_value;
          Script_typed_ir.big_map.Big_map.key_type := key_type;
          Script_typed_ir.big_map.Big_map.value_type := value_type
          |} := function_parameter in
    let diff_size :=
      let map_size :=
        Script_typed_ir.Big_map_overlay.(Map.S.fold)
          (fun (_key_hash : Script_expr_hash.t) ⇒
            fun function_parameter
              let '(key_value, value_value) := function_parameter in
              fun (accu_value : nodes_and_size) ⇒
                let base :=
                  op_plusexclamation
                    (op_plusexclamation h5w (op_starquestion word_size 3))
                    script_expr_hash_size in
                let accu_value := ret_succ_adding accu_value base in
                let accu_value :=
                  value_size_aux count_lambda_nodes accu_value cty key_value in
                match value_value with
                | Noneaccu_value
                | Some value_value
                  let accu_value := ret_succ_adding accu_value h1w in
                  value_size_aux count_lambda_nodes accu_value ty' value_value
                end) diff_value.(Script_typed_ir.big_map_overlay.map) accu_value
        in
      ret_adding map_size h2w in
    let big_map_id_size (s_value : Alpha_context.Big_map.Id.t)
      : Saturation_repr.t :=
      z_size (Alpha_context.Big_map.Id.unparse_to_z s_value) in
    let id_size := option_size big_map_id_size id in
    ret_adding
      (op_plusplus (op_plusplus (ty_size key_type) (ty_size value_type))
        diff_size) (op_plusexclamation h4w id_size))

and "'kdescr_size_aux" :=
  (fun
    (count_lambda_nodes : bool) (accu_value : nodes_and_size)
    (function_parameter : Script_typed_ir.kdescr) ⇒
    let '{|
      Script_typed_ir.kdescr.kloc := _;
        Script_typed_ir.kdescr.kbef := kbef;
        Script_typed_ir.kdescr.kaft := kaft;
        Script_typed_ir.kdescr.kinstr := kinstr
        |} := function_parameter in
    let accu_value :=
      ret_adding
        (op_plusplus (op_plusplus accu_value (stack_ty_size kbef))
          (stack_ty_size kaft)) h4w in
    kinstr_size_aux count_lambda_nodes accu_value kinstr).

Definition big_map_size_aux := 'big_map_size_aux.
Definition kdescr_size_aux := 'kdescr_size_aux.

Definition lambda_size (lam : Script_typed_ir.lambda) : nodes_and_size :=
  lambda_size_aux true zero lam.

Definition kinstr_size (kinstr : Script_typed_ir.kinstr) : nodes_and_size :=
  kinstr_size_aux true zero kinstr.

Definition value_size {A : Set} (ty_value : Script_typed_ir.ty) (x_value : A)
  : nodes_and_size := value_size_aux true zero ty_value x_value.