🍬 Script_typed_ir_size.v
Translated 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_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Int_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Nat_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Signature_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.String_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bytes_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Mutez_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Key_hash_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Key_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Timestamp_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Address_t ⇒ ret_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_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Operation_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Chain_id_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Never_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bls12_381_g1_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bls12_381_g2_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bls12_381_fr_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Chest_key_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Chest_t ⇒ ret_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_t ⇒ ret_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.KRest ⇒ zero
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 __6 ⇒ option __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 __7 ⇒ Script_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 __8 ⇒ Script_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 __14 ⇒ Script_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_value ⇒ count_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
| None ⇒ accu_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.
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_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Int_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Nat_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Signature_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.String_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bytes_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Mutez_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Key_hash_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Key_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Timestamp_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Address_t ⇒ ret_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_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Operation_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Chain_id_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Never_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bls12_381_g1_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bls12_381_g2_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Bls12_381_fr_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Chest_key_t ⇒ ret_succ_adding accu_value base_basic
| Script_typed_ir.Chest_t ⇒ ret_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_t ⇒ ret_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.KRest ⇒ zero
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 __6 ⇒ option __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 __7 ⇒ Script_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 __8 ⇒ Script_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 __14 ⇒ Script_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_value ⇒ count_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
| None ⇒ accu_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.