Skip to main content

🍬 Script_typed_ir_size.v

Translated OCaml

Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
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_map.
Require TezosOfOCaml.Proto_alpha.Script_set.
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 : Alpha_context.Script_string.t)
  : Saturation_repr.t :=
  string_size (Alpha_context.Script_string.to_string s_value).

Definition sapling_memo_size_size : Saturation_repr.t :=
  op_exclamationexclamation 0.

Module Ty_size.
  Definition base_basic : Saturation_repr.t := op_exclamationexclamation 0.

  Definition base_compound_no_meta : Saturation_repr.t := header_size.

  Definition base_compound {A : Set} (_meta : A) : Saturation_repr.t := h1w.

  Definition apply_comparable
    (accu_value : nodes_and_size) (cty : Script_typed_ir.comparable_ty)
    : nodes_and_size :=
    match cty 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.Chain_id_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Never_tret_succ_adding accu_value base_basic
    | Script_typed_ir.Pair_t _ty1 _ty2 a_value Dependent_bool.YesYes
      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 Dependent_bool.YesYes
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 3))
    | Script_typed_ir.Option_t _ty a_value Dependent_bool.Yes
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value)
          (op_starquestion word_size 2))
    | _unreachable_gadt_branch
    end.

  Definition apply (accu_value : nodes_and_size) (ty : Script_typed_ir.ty)
    : nodes_and_size :=
    match ty 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
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation base_compound_no_meta sapling_memo_size_size)
          word_size)
    | Script_typed_ir.Sapling_transaction_deprecated_t _m
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation base_compound_no_meta sapling_memo_size_size)
          word_size)
    | Script_typed_ir.Sapling_state_t _m
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation base_compound_no_meta sapling_memo_size_size)
          word_size)
    | Script_typed_ir.Ticket_t _cty a_value
      ret_succ_adding accu_value
        (op_plusexclamation (base_compound a_value) word_size)
    end.

  Definition f_value : Script_typed_ir.ty_traverse nodes_and_size :=
    {| Script_typed_ir.ty_traverse.apply := apply;
      Script_typed_ir.ty_traverse.apply_comparable := apply_comparable; |}.
End Ty_size.

Definition comparable_ty_size (cty : Script_typed_ir.comparable_ty)
  : nodes_and_size :=
  Script_typed_ir.comparable_ty_traverse cty zero Ty_size.f_value.

Definition ty_size (ty : Script_typed_ir.ty) : nodes_and_size :=
  Script_typed_ir.ty_traverse_value ty zero Ty_size.f_value.

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 _
      ret_succ_adding (op_plusplus accu_value (ty_size ty)) h2w
    end in
  Script_typed_ir.stack_ty_traverse_value s_value zero
    {| Script_typed_ir.stack_ty_traverse.apply := apply; |}.

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

Definition script_int_size (n_value : Alpha_context.Script_int.num)
  : Saturation_repr.t := z_size (Alpha_context.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 : Alpha_context.Script_timestamp.t)
  : Saturation_repr.t :=
  z_size (Alpha_context.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.

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 stack_prefix_preservation_witness_size : int Saturation_repr.t :=
  let kinfo_size := h2w in
  let scale :=
    op_plusexclamation header_size (op_plusexclamation h2w kinfo_size) in
  fun (k_value : int) ⇒ op_starquestion scale k_value.

Definition comb_gadt_witness_size : int Saturation_repr.t :=
  peano_shape_proof.

Definition uncomb_gadt_witness_size : int Saturation_repr.t :=
  peano_shape_proof.

Definition comb_get_gadt_witness_size : int Saturation_repr.t :=
  peano_shape_proof.

Definition comb_set_gadt_witness_size : int Saturation_repr.t :=
  peano_shape_proof.

Definition dup_n_gadt_witness_size : int Saturation_repr.t :=
  peano_shape_proof.

Definition contract_size (function_parameter : Script_typed_ir.typed_contract)
  : int × Saturation_repr.t :=
  let
    'Script_typed_ir.Typed_contract {|
      Script_typed_ir.typed_contract.Typed_contract.arg_ty := arg_ty;
        Script_typed_ir.typed_contract.Typed_contract.address := address
        |} := function_parameter in
  ret_adding (ty_size arg_ty) (op_plusexclamation h2w (address_size address)).

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 := _
      |} := 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))
    sapling_memo_size_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).

Definition kinfo_size (function_parameter : Script_typed_ir.kinfo)
  : Saturation_repr.t :=
  let '{|
    Script_typed_ir.kinfo.iloc := _; Script_typed_ir.kinfo.kstack_ty := _ |} :=
    function_parameter in
  h2w.

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 : Script_typed_ir.union Script_typed_ir.ty Script_typed_ir.comparable_ty)
  (x_value : a) {struct ty} : nodes_and_size :=
  let big_map_size_aux := 'big_map_size_aux in
  let apply {a : Set}
    (accu_value : nodes_and_size) (ty : Script_typed_ir.ty) (x_value : a)
    : nodes_and_size :=
    match (ty, x_value) with
    | (Script_typed_ir.Unit_t, _)ret_succ accu_value
    | (Script_typed_ir.Int_t, x_value)
      let x_value := cast Alpha_context.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 Alpha_context.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 Alpha_context.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 Alpha_context.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_typed_ir.boxed_list __7)
          x_value in
      ret_succ_adding accu_value
        (op_plusexclamation h2w
          (op_starquestion h2w x_value.(Script_typed_ir.boxed_list.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 Bls12_381.G1.(S.CURVE.size_in_memory))
    | (Script_typed_ir.Bls12_381_g2_t, _)
      ret_succ_adding accu_value
        (op_exclamationexclamation Bls12_381.G2.(S.CURVE.size_in_memory))
    | (Script_typed_ir.Bls12_381_fr_t, _)
      ret_succ_adding accu_value
        (op_exclamationexclamation Bls12_381.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
  let apply_comparable {a : Set}
    (accu_value : nodes_and_size) (ty : Script_typed_ir.comparable_ty)
    (x_value : a) : nodes_and_size :=
    match (ty, x_value) with
    | (Script_typed_ir.Unit_t, _)ret_succ accu_value
    | (Script_typed_ir.Int_t, x_value)
      let x_value := cast Alpha_context.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 Alpha_context.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 Alpha_context.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 Alpha_context.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 _ _ _ Dependent_bool.YesYes, _)
      ret_succ_adding accu_value h1w
    | (Script_typed_ir.Option_t _ _ Dependent_bool.Yes, x_value)
      let 'existT _ __34 x_value :=
        cast_exists (Es := Set) (fun __34option __34) x_value in
      ret_succ_adding accu_value
        (option_size
          (fun (function_parameter : __34) ⇒
            let '_ := function_parameter in
            op_exclamationexclamation 0) x_value)
    | (Script_typed_ir.Chain_id_t, _)
      ret_succ_adding accu_value chain_id_size
    | _unreachable_gadt_branch
    end in
  Script_typed_ir.value_traverse_value ty x_value accu_value
    {| Script_typed_ir.value_traverse.apply _ := apply;
      Script_typed_ir.value_traverse.apply_comparable _ := apply_comparable; |}

with lambda_size_aux
  (count_lambda_nodes : bool) (accu_value : nodes_and_size)
  (function_parameter : Script_typed_ir.lambda) {struct function_parameter}
  : nodes_and_size :=
  let kdescr_size_aux := 'kdescr_size_aux in
  let 'Script_typed_ir.Lam kdescr node_value := function_parameter in
  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

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 base (kinfo_value : Script_typed_ir.kinfo) : Saturation_repr.t :=
    op_plusexclamation h2w (kinfo_size kinfo_value) 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 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IDup kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISwap kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IConst kinfo_value x_value k_value
      let accu_value :=
        ret_succ_adding accu_value
          (op_plusexclamation (base kinfo_value) word_size) in
      let 'Script_typed_ir.Ty_ex_c top_ty :=
        Script_typed_ir.stack_top_ty
          (Script_typed_ir.kinfo_of_kinstr k_value).(Script_typed_ir.kinfo.kstack_ty)
        in
      value_size_aux count_lambda_nodes accu_value (Script_typed_ir.L top_ty)
        x_value
    | Script_typed_ir.ICons_pair kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICar kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICdr kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IUnpair kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICons_some kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICons_none kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    |
      Script_typed_ir.IIf_none {|
        Script_typed_ir.kinstr.IIf_none.kinfo := kinfo_value |} ⇒
      ret_succ_adding accu_value (base kinfo_value)
    |
      Script_typed_ir.IOpt_map {|
        Script_typed_ir.kinstr.IOpt_map.kinfo := kinfo_value |} ⇒
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICons_left kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICons_right kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    |
      Script_typed_ir.IIf_left {|
        Script_typed_ir.kinstr.IIf_left.kinfo := kinfo_value |} ⇒
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICons_list kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INil kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    |
      Script_typed_ir.IIf_cons {|
        Script_typed_ir.kinstr.IIf_cons.kinfo := kinfo_value |} ⇒
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IList_map kinfo_value _ _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IList_iter kinfo_value _ _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IList_size kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IEmpty_set kinfo_value cty _
      ret_succ_adding (op_plusplus accu_value (comparable_ty_size cty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.ISet_iter kinfo_value _ _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISet_mem kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISet_update kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISet_size kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IEmpty_map kinfo_value cty _
      ret_succ_adding (op_plusplus accu_value (comparable_ty_size cty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IMap_map kinfo_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IMap_iter kinfo_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IMap_mem kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMap_get kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMap_update kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMap_get_and_update kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMap_size kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IEmpty_big_map kinfo_value cty ty _
      ret_succ_adding
        (op_plusplus (op_plusplus accu_value (comparable_ty_size cty))
          (ty_size ty))
        (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
    | Script_typed_ir.IBig_map_mem kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IBig_map_get kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IBig_map_update kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IBig_map_get_and_update kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IConcat_string kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IConcat_string_pair kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISlice_string kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IString_size kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IConcat_bytes kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IConcat_bytes_pair kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISlice_bytes kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IBytes_size kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_seconds_to_timestamp kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_timestamp_to_seconds kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISub_timestamp_seconds kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IDiff_timestamps kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_tez kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISub_tez kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISub_tez_legacy kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_teznat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_nattez kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IEdiv_teznat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IEdiv_tez kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IOr kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAnd kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IXor kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INot kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IIs_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INeg kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAbs_int kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IInt_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_int kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISub_int kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_int kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IEdiv_int kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IEdiv_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ILsl_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ILsr_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IOr_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAnd_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAnd_int_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IXor_nat kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INot_int kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IIf {| Script_typed_ir.kinstr.IIf.kinfo := kinfo_value |}
      ⇒ ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ILoop kinfo_value _ _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ILoop_left kinfo_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IDip kinfo_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IExec kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IApply kinfo_value ty _
      ret_succ_adding (op_plusplus accu_value (ty_size ty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.ILambda kinfo_value lambda _
      let accu_value :=
        ret_succ_adding accu_value
          (op_plusexclamation (base kinfo_value) word_size) in
      lambda_size_aux count_lambda_nodes accu_value lambda
    | Script_typed_ir.IFailwith kinfo_value _ ty
      ret_succ_adding (op_plusplus accu_value (ty_size ty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.ICompare kinfo_value cty _
      ret_succ_adding (op_plusplus accu_value (comparable_ty_size cty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IEq kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INeq kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ILt kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IGt kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ILe kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IGe kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAddress kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IContract kinfo_value ty s_value _
      ret_succ_adding (op_plusplus accu_value (ty_size ty))
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value)
            (Alpha_context.Entrypoint.in_memory_size s_value))
          (op_starquestion word_size 2))
    | Script_typed_ir.IView kinfo_value s_value _
      ret_succ_adding (op_plusplus accu_value (view_signature_size s_value))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.ITransfer_tokens kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IImplicit_account kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    |
      Script_typed_ir.ICreate_contract {|
        Script_typed_ir.kinstr.ICreate_contract.kinfo := kinfo_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 := _
          |} ⇒
      ret_succ_adding
        (op_plusplus (op_plusplus accu_value (ty_size storage_type))
          (expr_size code))
        (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
    | Script_typed_ir.ISet_delegate kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INow kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMin_block_time kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IBalance kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ILevel kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ICheck_signature kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IHash_key kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IPack kinfo_value ty _
      ret_succ_adding (op_plusplus accu_value (ty_size ty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IUnpack kinfo_value ty _
      ret_succ_adding (op_plusplus accu_value (ty_size ty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IBlake2b kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISha256 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISha512 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISource kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISender kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISelf kinfo_value ty s_value _
      ret_succ_adding (op_plusplus accu_value (ty_size ty))
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (Alpha_context.Entrypoint.in_memory_size s_value))
    | Script_typed_ir.ISelf_address kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAmount kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISapling_empty_state kinfo_value _m _
      ret_succ_adding accu_value
        (op_plusexclamation (op_plusexclamation (base kinfo_value) word_size)
          sapling_memo_size_size)
    | Script_typed_ir.ISapling_verify_update kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISapling_verify_update_deprecated kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IDig kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (stack_prefix_preservation_witness_size n_value))
    | Script_typed_ir.IDug kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (stack_prefix_preservation_witness_size n_value))
    | Script_typed_ir.IDipn kinfo_value n_value _ _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (stack_prefix_preservation_witness_size n_value))
    | Script_typed_ir.IDropn kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (stack_prefix_preservation_witness_size n_value))
    | Script_typed_ir.IChainId kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INever kinfo_value
      ret_succ_adding accu_value (kinfo_size kinfo_value)
    | Script_typed_ir.IVoting_power kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ITotal_voting_power kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IKeccak kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISha3 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_bls12_381_g1 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_bls12_381_g2 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IAdd_bls12_381_fr kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_bls12_381_g1 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_bls12_381_g2 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_bls12_381_fr kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_bls12_381_z_fr kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IMul_bls12_381_fr_z kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IInt_bls12_381_fr kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INeg_bls12_381_g1 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INeg_bls12_381_g2 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.INeg_bls12_381_fr kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IPairing_check_bls12_381 kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IComb kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (comb_gadt_witness_size n_value))
    | Script_typed_ir.IUncomb kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (uncomb_gadt_witness_size n_value))
    | Script_typed_ir.IComb_get kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (comb_get_gadt_witness_size n_value))
    | Script_typed_ir.IComb_set kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (comb_set_gadt_witness_size n_value))
    | Script_typed_ir.IDup_n kinfo_value n_value _ _
      ret_succ_adding accu_value
        (op_plusexclamation
          (op_plusexclamation (base kinfo_value) (op_starquestion word_size 2))
          (dup_n_gadt_witness_size n_value))
    | Script_typed_ir.ITicket kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IRead_ticket kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.ISplit_ticket kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IJoin_tickets kinfo_value cty _
      ret_succ_adding (op_plusplus accu_value (comparable_ty_size cty))
        (op_plusexclamation (base kinfo_value) word_size)
    | Script_typed_ir.IOpen_chest kinfo_value _
      ret_succ_adding accu_value (base kinfo_value)
    | Script_typed_ir.IHalt kinfo_value
      ret_succ_adding accu_value
        (op_plusexclamation h1w (kinfo_size kinfo_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
                    (Script_typed_ir.R 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
                    (Script_typed_ir.L 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 (comparable_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.

Fixpoint kinstr_extra_size (t_value : Script_typed_ir.kinstr)
  : nodes_and_size :=
  let ret_zero {A : Set} (x_value : A) : int × A :=
    (Nodes.(SNodes.zero), x_value) in
  let apply (accu_value : nodes_and_size) (t_value : Script_typed_ir.kinstr)
    : nodes_and_size :=
    let stack_prefix_preservation_witness_size (n_value : int)
      : int × Saturation_repr.t :=
      ret_zero (op_starquestion (op_exclamationexclamation 24) n_value) in
    let dup_n_gadt_witness_size (n_value : int) : int × Saturation_repr.t :=
      ret_zero (op_starquestion (op_exclamationexclamation 16) n_value) in
    let comb (n_value : int) : int × Saturation_repr.t :=
      ret_zero (op_starquestion (op_exclamationexclamation 16) n_value) in
    let self_size :=
      match t_value with
      | Script_typed_ir.IDig _ n_value _ _
        stack_prefix_preservation_witness_size n_value
      | Script_typed_ir.IDug _ n_value _ _
        stack_prefix_preservation_witness_size n_value
      | Script_typed_ir.IDipn _ n_value _ _ _
        stack_prefix_preservation_witness_size n_value
      | Script_typed_ir.IDropn _ n_value _ _
        stack_prefix_preservation_witness_size n_value
      | Script_typed_ir.IComb _ n_value _ _comb n_value
      | Script_typed_ir.IUncomb _ n_value _ _comb n_value
      | Script_typed_ir.IComb_get _ n_value _ _comb (n_value /i 2)
      | Script_typed_ir.IComb_set _ n_value _ _comb (n_value /i 2)
      | Script_typed_ir.IDup_n _ n_value _ _dup_n_gadt_witness_size n_value
      | Script_typed_ir.ITicket _ k_value
        let kinfo_value := Script_typed_ir.kinfo_of_kinstr k_value in
        match kinfo_value.(Script_typed_ir.kinfo.kstack_ty) with
        | Script_typed_ir.Item_t ty _ty_size ty
        | _unreachable_gadt_branch
        end
      | Script_typed_ir.IRead_ticket _ k_value
        let kinfo_value := Script_typed_ir.kinfo_of_kinstr k_value in
        match kinfo_value.(Script_typed_ir.kinfo.kstack_ty) with
        | Script_typed_ir.Item_t ty _ty_size ty
        | _unreachable_gadt_branch
        end
      | Script_typed_ir.ICompare _ ty _comparable_ty_size ty
      | Script_typed_ir.ISet_iter _ body _
        let kinfo_value := Script_typed_ir.kinfo_of_kinstr body in
        match kinfo_value.(Script_typed_ir.kinfo.kstack_ty) with
        | Script_typed_ir.Item_t ty _ty_size ty
        | _unreachable_gadt_branch
        end
      | Script_typed_ir.IMap_map _ body _
        let kinfo_value := Script_typed_ir.kinfo_of_kinstr body in
        match kinfo_value.(Script_typed_ir.kinfo.kstack_ty) with
        | Script_typed_ir.Item_t ty _ty_size ty
        | _unreachable_gadt_branch
        end
      | Script_typed_ir.IMap_iter _ body _
        let kinfo_value := Script_typed_ir.kinfo_of_kinstr body in
        match kinfo_value.(Script_typed_ir.kinfo.kstack_ty) with
        | Script_typed_ir.Item_t ty _ty_size ty
        | _unreachable_gadt_branch
        end
      | Script_typed_ir.ILambda _ lambda _lambda_extra_size lambda
      | _zero
      end in
    ret_succ (op_plusplus accu_value self_size) in
  Script_typed_ir.kinstr_traverse_value t_value zero
    {| Script_typed_ir.kinstr_traverse.apply := apply; |}

with lambda_extra_size (function_parameter : Script_typed_ir.lambda)
  : nodes_and_size :=
  let 'Script_typed_ir.Lam {| Script_typed_ir.kdescr.kinstr := kinstr |} _ :=
    function_parameter in
  kinstr_extra_size kinstr.

Definition lambda_size (lam : Script_typed_ir.lambda)
  : int × Saturation_repr.t :=
  let '(lambda_nodes, lambda_size) := lambda_size_aux true zero lam in
  let '(lambda_extra_size_nodes, lambda_extra_size) := lambda_extra_size lam in
  let size_value :=
    op_plusexclamation (op_divquestion (op_starquestion lambda_size 157) 100)
      (op_divquestion (op_starquestion lambda_extra_size 18) 100) in
  ((Nodes.(SNodes.add) lambda_nodes lambda_extra_size_nodes), size_value).

Definition kinstr_size (kinstr : Script_typed_ir.kinstr)
  : int × Saturation_repr.t :=
  let '(kinstr_extra_size_nodes, kinstr_extra_size) := kinstr_extra_size kinstr
    in
  let '(kinstr_nodes, kinstr_size) := kinstr_size_aux true zero kinstr in
  let size_value :=
    op_plusexclamation (op_divquestion (op_starquestion kinstr_size 157) 100)
      (op_divquestion (op_starquestion kinstr_extra_size 18) 100) in
  ((Nodes.(SNodes.add) kinstr_nodes kinstr_extra_size_nodes), size_value).

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