Skip to main content

🍬 Script_typed_ir.v

Translated OCaml

See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.

Module step_constants.
  Record record : Set := Build {
    source : Alpha_context.Contract.t;
    payer : Signature.public_key_hash;
    self : Contract_hash.t;
    amount : Alpha_context.Tez.t;
    balance : Alpha_context.Tez.t;
    chain_id : Chain_id.t;
    now : Script_timestamp.t;
    level : Script_int.num;
  }.
  Definition with_source source (r : record) :=
    Build source r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id) r.(now)
      r.(level).
  Definition with_payer payer (r : record) :=
    Build r.(source) payer r.(self) r.(amount) r.(balance) r.(chain_id) r.(now)
      r.(level).
  Definition with_self self (r : record) :=
    Build r.(source) r.(payer) self r.(amount) r.(balance) r.(chain_id) r.(now)
      r.(level).
  Definition with_amount amount (r : record) :=
    Build r.(source) r.(payer) r.(self) amount r.(balance) r.(chain_id) r.(now)
      r.(level).
  Definition with_balance balance (r : record) :=
    Build r.(source) r.(payer) r.(self) r.(amount) balance r.(chain_id) r.(now)
      r.(level).
  Definition with_chain_id chain_id (r : record) :=
    Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) chain_id r.(now)
      r.(level).
  Definition with_now now (r : record) :=
    Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id) now
      r.(level).
  Definition with_level level (r : record) :=
    Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id)
      r.(now) level.
End step_constants.
Definition step_constants := step_constants.record.

Inductive never : Set :=.

Module address.
  Record record : Set := Build {
    destination : Alpha_context.Destination.t;
    entrypoint : Alpha_context.Entrypoint.t;
  }.
  Definition with_destination destination (r : record) :=
    Build destination r.(entrypoint).
  Definition with_entrypoint entrypoint (r : record) :=
    Build r.(destination) entrypoint.
End address.
Definition address := address.record.

Module Script_signature.
  Inductive t : Set :=
  | Signature_tag : Alpha_context.signature t.

  Definition make (s_value : Alpha_context.signature) : t :=
    Signature_tag s_value.

  Definition get (function_parameter : t) : Alpha_context.signature :=
    let 'Signature_tag s_value := function_parameter in
    s_value.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let 'Signature_tag x_value := function_parameter in
        x_value)
      (fun (x_value : Alpha_context.signature) ⇒ Signature_tag x_value) None
      Signature.encoding.

  Definition of_b58check_opt (x_value : string) : option t :=
    Option.map make (Signature.of_b58check_opt x_value).

  Definition check
    (watermark : option Signature.watermark) (pub_key : Signature.public_key)
    (function_parameter : t) : bytes bool :=
    let 'Signature_tag s_value := function_parameter in
    fun (bytes_value : bytes) ⇒
      Signature.check watermark pub_key s_value bytes_value.

  Definition compare (function_parameter : t) : t int :=
    let 'Signature_tag x_value := function_parameter in
    fun (function_parameter : t) ⇒
      let 'Signature_tag y_value := function_parameter in
      Signature.compare x_value y_value.

  Definition size_value : int := Signature.size_value.
End Script_signature.

Definition signature : Set := Script_signature.t.

Definition tx_rollup_l2_address : Set := Tx_rollup_l2_address.Indexable.value.

Definition pair (a b : Set) : Set := a × b.

Inductive union (a b : Set) : Set :=
| L : a union a b
| R : b union a b.

Arguments L {_ _}.
Arguments R {_ _}.

Module Script_chain_id.
  Inductive t : Set :=
  | Chain_id_tag : Chain_id.t t.

  Definition make (x_value : Chain_id.t) : t := Chain_id_tag x_value.

  Definition compare (function_parameter : t) : t int :=
    let 'Chain_id_tag x_value := function_parameter in
    fun (function_parameter : t) ⇒
      let 'Chain_id_tag y_value := function_parameter in
      Chain_id.compare x_value y_value.

  Definition size_value : int := Chain_id.size_value.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let 'Chain_id_tag x_value := function_parameter in
        x_value) make None Chain_id.encoding.

  Definition to_b58check (function_parameter : t) : string :=
    let 'Chain_id_tag x_value := function_parameter in
    Chain_id.to_b58check x_value.

  Definition of_b58check_opt (x_value : string) : option t :=
    Option.map make (Chain_id.of_b58check_opt x_value).
End Script_chain_id.

Module Script_bls.
  Module S.
    Record signature {t fr : Set} : Set := {
      t := t;
      fr := fr;
      add : t t t;
      mul : t fr t;
      negate : t t;
      of_bytes_opt : Bytes.t option t;
      to_bytes : t Bytes.t;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_ _}.

  Module Fr.
    Inductive t : Set :=
    | Fr_tag : Bls.Primitive.Fr.(S.PRIME_FIELD.t) t.

    Definition add (function_parameter : t) : t t :=
      let 'Fr_tag x_value := function_parameter in
      fun (function_parameter : t) ⇒
        let 'Fr_tag y_value := function_parameter in
        Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.add) x_value y_value).

    Definition mul (function_parameter : t) : t t :=
      let 'Fr_tag x_value := function_parameter in
      fun (function_parameter : t) ⇒
        let 'Fr_tag y_value := function_parameter in
        Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.mul) x_value y_value).

    Definition negate (function_parameter : t) : t :=
      let 'Fr_tag x_value := function_parameter in
      Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.negate) x_value).

    Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
      Option.map
        (fun (x_value : Bls.Primitive.Fr.(S.PRIME_FIELD.t)) ⇒ Fr_tag x_value)
        (Bls.Primitive.Fr.(S.PRIME_FIELD.of_bytes_opt) bytes_value).

    Definition to_bytes (function_parameter : t) : Bytes.t :=
      let 'Fr_tag x_value := function_parameter in
      Bls.Primitive.Fr.(S.PRIME_FIELD.to_bytes) x_value.

    Definition of_z (z_value : Z.t) : t :=
      Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.of_z) z_value).

    Definition to_z (function_parameter : t) : Z.t :=
      let 'Fr_tag x_value := function_parameter in
      Bls.Primitive.Fr.(S.PRIME_FIELD.to_z) x_value.
  End Fr.

  Module G1.
    Inductive t : Set :=
    | G1_tag : Bls.Primitive.G1.(S.CURVE.t) t.

    Definition add (function_parameter : t) : t t :=
      let 'G1_tag x_value := function_parameter in
      fun (function_parameter : t) ⇒
        let 'G1_tag y_value := function_parameter in
        G1_tag (Bls.Primitive.G1.(S.CURVE.add) x_value y_value).

    Definition mul (function_parameter : t) : Fr.t t :=
      let 'G1_tag x_value := function_parameter in
      fun (function_parameter : Fr.t) ⇒
        let 'Fr.Fr_tag y_value := function_parameter in
        G1_tag (Bls.Primitive.G1.(S.CURVE.mul) x_value y_value).

    Definition negate (function_parameter : t) : t :=
      let 'G1_tag x_value := function_parameter in
      G1_tag (Bls.Primitive.G1.(S.CURVE.negate) x_value).

    Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
      Option.map
        (fun (x_value : Bls.Primitive.G1.(S.CURVE.t)) ⇒ G1_tag x_value)
        (Bls.Primitive.G1.(S.CURVE.of_bytes_opt) bytes_value).

    Definition to_bytes (function_parameter : t) : Bytes.t :=
      let 'G1_tag x_value := function_parameter in
      Bls.Primitive.G1.(S.CURVE.to_bytes) x_value.

    (* G1 *)
    Definition module :=
      {|
        S.add := add;
        S.mul := mul;
        S.negate := negate;
        S.of_bytes_opt := of_bytes_opt;
        S.to_bytes := to_bytes
      |}.
  End G1.
  Definition G1 := G1.module.

  Module G2.
    Inductive t : Set :=
    | G2_tag : Bls.Primitive.G2.(S.CURVE.t) t.

    Definition add (function_parameter : t) : t t :=
      let 'G2_tag x_value := function_parameter in
      fun (function_parameter : t) ⇒
        let 'G2_tag y_value := function_parameter in
        G2_tag (Bls.Primitive.G2.(S.CURVE.add) x_value y_value).

    Definition mul (function_parameter : t) : Fr.t t :=
      let 'G2_tag x_value := function_parameter in
      fun (function_parameter : Fr.t) ⇒
        let 'Fr.Fr_tag y_value := function_parameter in
        G2_tag (Bls.Primitive.G2.(S.CURVE.mul) x_value y_value).

    Definition negate (function_parameter : t) : t :=
      let 'G2_tag x_value := function_parameter in
      G2_tag (Bls.Primitive.G2.(S.CURVE.negate) x_value).

    Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
      Option.map
        (fun (x_value : Bls.Primitive.G2.(S.CURVE.t)) ⇒ G2_tag x_value)
        (Bls.Primitive.G2.(S.CURVE.of_bytes_opt) bytes_value).

    Definition to_bytes (function_parameter : t) : Bytes.t :=
      let 'G2_tag x_value := function_parameter in
      Bls.Primitive.G2.(S.CURVE.to_bytes) x_value.

    (* G2 *)
    Definition module :=
      {|
        S.add := add;
        S.mul := mul;
        S.negate := negate;
        S.of_bytes_opt := of_bytes_opt;
        S.to_bytes := to_bytes
      |}.
  End G2.
  Definition G2 := G2.module.

  Definition pairing_check (l_value : list (G1.(S.t) × G2.(S.t))) : bool :=
    let l_value :=
      List.map
        (fun (function_parameter : G1.(S.t) × G2.(S.t)) ⇒
          let '(G1.G1_tag x_value, G2.G2_tag y_value) := function_parameter in
          (x_value, y_value)) l_value in
    Bls.Primitive.pairing_check l_value.
End Script_bls.

Module Script_timelock.
  Inductive chest_key : Set :=
  | Chest_key_tag : Timelock.chest_key chest_key.

  Definition make_chest_key (chest_key_value : Timelock.chest_key)
    : chest_key := Chest_key_tag chest_key_value.

  Definition chest_key_encoding : Data_encoding.encoding chest_key :=
    Data_encoding.conv
      (fun (function_parameter : chest_key) ⇒
        let 'Chest_key_tag x_value := function_parameter in
        x_value) (fun (x_value : Timelock.chest_key) ⇒ Chest_key_tag x_value)
      None Timelock.chest_key_encoding.

  Inductive chest : Set :=
  | Chest_tag : Timelock.chest chest.

  Definition make_chest (chest_value : Timelock.chest) : chest :=
    Chest_tag chest_value.

  Definition chest_encoding : Data_encoding.encoding chest :=
    Data_encoding.conv
      (fun (function_parameter : chest) ⇒
        let 'Chest_tag x_value := function_parameter in
        x_value) (fun (x_value : Timelock.chest) ⇒ Chest_tag x_value) None
      Timelock.chest_encoding.

  Definition open_chest (function_parameter : chest)
    : chest_key int Timelock.opening_result :=
    let 'Chest_tag chest_value := function_parameter in
    fun (function_parameter : chest_key) ⇒
      let 'Chest_key_tag chest_key_value := function_parameter in
      fun (time : int) ⇒ Timelock.open_chest chest_value chest_key_value time.

  Definition get_plaintext_size (function_parameter : chest) : int :=
    let 'Chest_tag x_value := function_parameter in
    Timelock.get_plaintext_size x_value.
End Script_timelock.

Definition ticket_amount : Set := Ticket_amount.t.

Module ticket.
  Record record {a : Set} : Set := Build {
    ticketer : Alpha_context.Contract.t;
    contents : a;
    amount : ticket_amount;
  }.
  Arguments record : clear implicits.
  Definition with_ticketer {t_a} ticketer (r : record t_a) :=
    Build t_a ticketer r.(contents) r.(amount).
  Definition with_contents {t_a} contents (r : record t_a) :=
    Build t_a r.(ticketer) contents r.(amount).
  Definition with_amount {t_a} amount (r : record t_a) :=
    Build t_a r.(ticketer) r.(contents) amount.
End ticket.
Definition ticket := ticket.record.

Module TYPE_SIZE.
  Record signature {t : Set} : Set := {
    t := t;
    check_eq :
       {error_context error_trace : Set},
      Script_tc_errors.error_details error_context t t
      Pervasives.result unit error_trace;
    to_int : t Saturation_repr.t;
    one : t;
    two : t;
    three : t;
    four : t;
    compound1 : Alpha_context.Script.location t M? t;
    compound2 : Alpha_context.Script.location t t M? t;
  }.
End TYPE_SIZE.
Definition TYPE_SIZE := @TYPE_SIZE.signature.
Arguments TYPE_SIZE {_}.

Module Type_size.
  Definition t : Set := int.

Init function; without side-effects in Coq
  Definition init_module : unit :=
    let '_ :=
      Saturation_repr.mul_safe_of_int_exn
        Alpha_context.Constants.michelson_maximum_type_size in
    tt.

  Definition to_int : int Saturation_repr.t :=
    Saturation_repr.mul_safe_of_int_exn.

  Definition one : int := 1.

  Definition two : int := 2.

  Definition three : int := 3.

  Definition four : int := 4.

  Definition check_eq {A error_trace : Set}
    (error_details : Script_tc_errors.error_details A) (x_value : int)
    (y_value : int) : Pervasives.result unit error_trace :=
    if x_value =i y_value then
      Result.return_unit
    else
      Pervasives.Error
        match error_details with
        | Script_tc_errors.Fast
          cast error_trace Script_tc_errors.Inconsistent_types_fast
        | Script_tc_errors.Informative _
          cast error_trace
          (Error_monad.trace_of_error
            (Build_extensible "Inconsistent_type_sizes" (t × t)
              (x_value, y_value)))
        end.

  Definition of_int
    (loc_value : Alpha_context.Script.location) (size_value : int) : M? int :=
    let max_size := Alpha_context.Constants.michelson_maximum_type_size in
    if size_value i max_size then
      return? size_value
    else
      Error_monad.error_value
        (Build_extensible "Type_too_large" (Alpha_context.Script.location × int)
          (loc_value, max_size)).

  Definition compound1
    (loc_value : Alpha_context.Script.location) (size_value : int) : M? int :=
    of_int loc_value (1 +i size_value).

  Definition compound2
    (loc_value : Alpha_context.Script.location) (size1 : int) (size2 : int)
    : M? int := of_int loc_value ((1 +i size1) +i size2).

  (* Type_size *)
  Definition module :=
    {|
      TYPE_SIZE.check_eq _ _ := check_eq;
      TYPE_SIZE.to_int := to_int;
      TYPE_SIZE.one := one;
      TYPE_SIZE.two := two;
      TYPE_SIZE.three := three;
      TYPE_SIZE.four := four;
      TYPE_SIZE.compound1 := compound1;
      TYPE_SIZE.compound2 := compound2
    |}.
End Type_size.
Definition Type_size : TYPE_SIZE (t := _) := Type_size.module.

Inductive empty_cell : Set :=
| EmptyCell : empty_cell.

Definition end_of_stack : Set := empty_cell × empty_cell.

Module ty_metadata.
  Record record : Set := Build {
    size : Type_size.(TYPE_SIZE.t);
  }.
  Definition with_size size (r : record) :=
    Build size.
End ty_metadata.
Definition ty_metadata := ty_metadata.record.

Module Boxed_set_OPS.
  Record signature {t elt : Set} : Set := {
    t := t;
    elt := elt;
    elt_size : elt int;
    empty : t;
    add : elt t t;
    mem : elt t bool;
    remove : elt t t;
    fold : {a : Set}, (elt a a) t a a;
  }.
End Boxed_set_OPS.
Definition Boxed_set_OPS := @Boxed_set_OPS.signature.
Arguments Boxed_set_OPS {_ _}.

Module Boxed_set.
  Record signature {elt OPS_t : Set} : Set := {
    elt := elt;
    OPS : Boxed_set_OPS (t := OPS_t) (elt := elt);
    boxed : OPS.(Boxed_set_OPS.t);
    size_value : int;
  }.
End Boxed_set.
Definition Boxed_set := @Boxed_set.signature.
Arguments Boxed_set {_ _}.

Inductive set (elt : Set) : Set :=
| Set_tag : {OPS_t : Set @ Boxed_set (elt := elt) (OPS_t := OPS_t)} set elt.

Arguments Set_tag {_}.

Module Boxed_map_OPS.
  Record signature {t : Set Set} {key : Set} : Set := {
    t := t;
    key := key;
    key_size : key int;
    empty : {value : Set}, t value;
    add : {value : Set}, key value t value t value;
    remove : {value : Set}, key t value t value;
    find : {value : Set}, key t value option value;
    fold :
       {a value : Set}, (key value a a) t value a a;
    fold_es :
       {a value : Set},
      (key value a M? a) t value a M? a;
  }.
End Boxed_map_OPS.
Definition Boxed_map_OPS := @Boxed_map_OPS.signature.
Arguments Boxed_map_OPS {_ _}.

Module Boxed_map.
  Record signature {key value : Set} {OPS_t : Set Set} : Set := {
    key := key;
    value := value;
    OPS : Boxed_map_OPS (t := OPS_t) (key := key);
    boxed : OPS.(Boxed_map_OPS.t) value;
    size_value : int;
    boxed_map_tag : unit;
  }.
End Boxed_map.
Definition Boxed_map := @Boxed_map.signature.
Arguments Boxed_map {_ _ _}.

Inductive map (key value : Set) : Set :=
| Map_tag :
  {OPS_t : Set Set @
    Boxed_map (key := key) (value := value) (OPS_t := OPS_t)} map key value.

Arguments Map_tag {_ _}.

Definition Big_map_overlay :=
  Map.Make
    (let t : Set := Script_expr_hash.t in
    let compare := Script_expr_hash.compare in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Module big_map_overlay.
  Record record {key value : Set} : Set := Build {
    map : Big_map_overlay.(Map.S.t) (key × option value);
    size : int;
  }.
  Arguments record : clear implicits.
  Definition with_map {t_key t_value} map (r : record t_key t_value) :=
    Build t_key t_value map r.(size).
  Definition with_size {t_key t_value} size (r : record t_key t_value) :=
    Build t_key t_value r.(map) size.
End big_map_overlay.
Definition big_map_overlay := big_map_overlay.record.

Module boxed_list.
  Record record {elt : Set} : Set := Build {
    elements : list elt;
    length : int;
  }.
  Arguments record : clear implicits.
  Definition with_elements {t_elt} elements (r : record t_elt) :=
    Build t_elt elements r.(length).
  Definition with_length {t_elt} length (r : record t_elt) :=
    Build t_elt r.(elements) length.
End boxed_list.
Definition boxed_list := boxed_list.record.

Module view.
  Record record : Set := Build {
    input_ty : Alpha_context.Script.node;
    output_ty : Alpha_context.Script.node;
    view_code : Alpha_context.Script.node;
  }.
  Definition with_input_ty input_ty (r : record) :=
    Build input_ty r.(output_ty) r.(view_code).
  Definition with_output_ty output_ty (r : record) :=
    Build r.(input_ty) output_ty r.(view_code).
  Definition with_view_code view_code (r : record) :=
    Build r.(input_ty) r.(output_ty) view_code.
End view.
Definition view := view.record.

Definition view_map : Set := map Script_string.t view.

Module entrypoint_info.
  Record record : Set := Build {
    name : Alpha_context.Entrypoint.t;
    original_type_expr : Alpha_context.Script.node;
  }.
  Definition with_name name (r : record) :=
    Build name r.(original_type_expr).
  Definition with_original_type_expr original_type_expr (r : record) :=
    Build r.(name) original_type_expr.
End entrypoint_info.
Definition entrypoint_info := entrypoint_info.record.

Records for the constructor parameters
Module ConstructorRecords_nested_entrypoints.
  Module nested_entrypoints.
    Module Entrypoints_Union.
      Record record {_left _right : Set} : Set := Build {
        _left : _left;
        _right : _right;
      }.
      Arguments record : clear implicits.
      Definition with__left {t__left t__right} _left
        (r : record t__left t__right) :=
        Build t__left t__right _left r.(_right).
      Definition with__right {t__left t__right} _right
        (r : record t__left t__right) :=
        Build t__left t__right r.(_left) _right.
    End Entrypoints_Union.
    Definition Entrypoints_Union_skeleton := Entrypoints_Union.record.
  End nested_entrypoints.
End ConstructorRecords_nested_entrypoints.
Import ConstructorRecords_nested_entrypoints.

Module entrypoints_node.
  Record record {at_node nested : Set} : Set := Build {
    at_node : at_node;
    nested : nested;
  }.
  Arguments record : clear implicits.
  Definition with_at_node {t_at_node t_nested} at_node
    (r : record t_at_node t_nested) :=
    Build t_at_node t_nested at_node r.(nested).
  Definition with_nested {t_at_node t_nested} nested
    (r : record t_at_node t_nested) :=
    Build t_at_node t_nested r.(at_node) nested.
End entrypoints_node.
Definition entrypoints_node_skeleton := entrypoints_node.record.

Reserved Notation "'nested_entrypoints.Entrypoints_Union".
Reserved Notation "'entrypoints_node".

Inductive nested_entrypoints : Set :=
| Entrypoints_Union :
  'nested_entrypoints.Entrypoints_Union nested_entrypoints
| Entrypoints_None : nested_entrypoints

where "'entrypoints_node" :=
  (entrypoints_node_skeleton (option entrypoint_info) nested_entrypoints)
and "'nested_entrypoints.Entrypoints_Union" :=
  (nested_entrypoints.Entrypoints_Union_skeleton 'entrypoints_node
    'entrypoints_node).

Module nested_entrypoints.
  Include ConstructorRecords_nested_entrypoints.nested_entrypoints.
  Definition Entrypoints_Union := 'nested_entrypoints.Entrypoints_Union.
End nested_entrypoints.

Definition entrypoints_node := 'entrypoints_node.

Definition no_entrypoints : entrypoints_node :=
  {| entrypoints_node.at_node := None;
    entrypoints_node.nested := Entrypoints_None; |}.

Inductive logging_event : Set :=
| LogEntry : logging_event
| LogExit : Alpha_context.Script.location logging_event.

Records for the constructor parameters
Module
  ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
  Module kinstr.
    Module IIf_none.
      Record record {loc branch_if_none branch_if_some k : Set} : Set := Build {
        loc : loc;
        branch_if_none : branch_if_none;
        branch_if_some : branch_if_some;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_loc {t_loc t_branch_if_none t_branch_if_some t_k} loc
        (r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
        Build t_loc t_branch_if_none t_branch_if_some t_k loc r.(branch_if_none)
          r.(branch_if_some) r.(k).
      Definition with_branch_if_none
        {t_loc t_branch_if_none t_branch_if_some t_k} branch_if_none
        (r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
        Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc) branch_if_none
          r.(branch_if_some) r.(k).
      Definition with_branch_if_some
        {t_loc t_branch_if_none t_branch_if_some t_k} branch_if_some
        (r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
        Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc)
          r.(branch_if_none) branch_if_some r.(k).
      Definition with_k {t_loc t_branch_if_none t_branch_if_some t_k} k
        (r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
        Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc)
          r.(branch_if_none) r.(branch_if_some) k.
    End IIf_none.
    Definition IIf_none_skeleton := IIf_none.record.

    Module IOpt_map.
      Record record {loc body k : Set} : Set := Build {
        loc : loc;
        body : body;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_loc {t_loc t_body t_k} loc
        (r : record t_loc t_body t_k) :=
        Build t_loc t_body t_k loc r.(body) r.(k).
      Definition with_body {t_loc t_body t_k} body
        (r : record t_loc t_body t_k) :=
        Build t_loc t_body t_k r.(loc) body r.(k).
      Definition with_k {t_loc t_body t_k} k (r : record t_loc t_body t_k) :=
        Build t_loc t_body t_k r.(loc) r.(body) k.
    End IOpt_map.
    Definition IOpt_map_skeleton := IOpt_map.record.

    Module IIf_left.
      Record record {loc branch_if_left branch_if_right k : Set} : Set := Build {
        loc : loc;
        branch_if_left : branch_if_left;
        branch_if_right : branch_if_right;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_loc {t_loc t_branch_if_left t_branch_if_right t_k} loc
        (r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
        Build t_loc t_branch_if_left t_branch_if_right t_k loc
          r.(branch_if_left) r.(branch_if_right) r.(k).
      Definition with_branch_if_left
        {t_loc t_branch_if_left t_branch_if_right t_k} branch_if_left
        (r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
        Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
          branch_if_left r.(branch_if_right) r.(k).
      Definition with_branch_if_right
        {t_loc t_branch_if_left t_branch_if_right t_k} branch_if_right
        (r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
        Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
          r.(branch_if_left) branch_if_right r.(k).
      Definition with_k {t_loc t_branch_if_left t_branch_if_right t_k} k
        (r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
        Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
          r.(branch_if_left) r.(branch_if_right) k.
    End IIf_left.
    Definition IIf_left_skeleton := IIf_left.record.

    Module IIf_cons.
      Record record {loc branch_if_cons branch_if_nil k : Set} : Set := Build {
        loc : loc;
        branch_if_cons : branch_if_cons;
        branch_if_nil : branch_if_nil;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_loc {t_loc t_branch_if_cons t_branch_if_nil t_k} loc
        (r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
        Build t_loc t_branch_if_cons t_branch_if_nil t_k loc r.(branch_if_cons)
          r.(branch_if_nil) r.(k).
      Definition with_branch_if_cons
        {t_loc t_branch_if_cons t_branch_if_nil t_k} branch_if_cons
        (r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
        Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc) branch_if_cons
          r.(branch_if_nil) r.(k).
      Definition with_branch_if_nil {t_loc t_branch_if_cons t_branch_if_nil t_k}
        branch_if_nil (r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
        Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc)
          r.(branch_if_cons) branch_if_nil r.(k).
      Definition with_k {t_loc t_branch_if_cons t_branch_if_nil t_k} k
        (r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
        Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc)
          r.(branch_if_cons) r.(branch_if_nil) k.
    End IIf_cons.
    Definition IIf_cons_skeleton := IIf_cons.record.

    Module IIf.
      Record record {loc branch_if_true branch_if_false k : Set} : Set := Build {
        loc : loc;
        branch_if_true : branch_if_true;
        branch_if_false : branch_if_false;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_loc {t_loc t_branch_if_true t_branch_if_false t_k} loc
        (r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
        Build t_loc t_branch_if_true t_branch_if_false t_k loc
          r.(branch_if_true) r.(branch_if_false) r.(k).
      Definition with_branch_if_true
        {t_loc t_branch_if_true t_branch_if_false t_k} branch_if_true
        (r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
        Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
          branch_if_true r.(branch_if_false) r.(k).
      Definition with_branch_if_false
        {t_loc t_branch_if_true t_branch_if_false t_k} branch_if_false
        (r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
        Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
          r.(branch_if_true) branch_if_false r.(k).
      Definition with_k {t_loc t_branch_if_true t_branch_if_false t_k} k
        (r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
        Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
          r.(branch_if_true) r.(branch_if_false) k.
    End IIf.
    Definition IIf_skeleton := IIf.record.

    Module ICreate_contract.
      Record record {loc storage_type code k : Set} : Set := Build {
        loc : loc;
        storage_type : storage_type;
        code : code;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_loc {t_loc t_storage_type t_code t_k} loc
        (r : record t_loc t_storage_type t_code t_k) :=
        Build t_loc t_storage_type t_code t_k loc r.(storage_type) r.(code)
          r.(k).
      Definition with_storage_type {t_loc t_storage_type t_code t_k}
        storage_type (r : record t_loc t_storage_type t_code t_k) :=
        Build t_loc t_storage_type t_code t_k r.(loc) storage_type r.(code)
          r.(k).
      Definition with_code {t_loc t_storage_type t_code t_k} code
        (r : record t_loc t_storage_type t_code t_k) :=
        Build t_loc t_storage_type t_code t_k r.(loc) r.(storage_type) code
          r.(k).
      Definition with_k {t_loc t_storage_type t_code t_k} k
        (r : record t_loc t_storage_type t_code t_k) :=
        Build t_loc t_storage_type t_code t_k r.(loc) r.(storage_type) r.(code)
          k.
    End ICreate_contract.
    Definition ICreate_contract_skeleton := ICreate_contract.record.

    Module IEmit.
      Record record {loc tag ty unparsed_ty k : Set} : Set := Build {
        loc : loc;
        tag : tag;
        ty : ty;
        unparsed_ty : unparsed_ty;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_loc {t_loc t_tag t_ty t_unparsed_ty t_k} loc
        (r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
        Build t_loc t_tag t_ty t_unparsed_ty t_k loc r.(tag) r.(ty)
          r.(unparsed_ty) r.(k).
      Definition with_tag {t_loc t_tag t_ty t_unparsed_ty t_k} tag
        (r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
        Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) tag r.(ty)
          r.(unparsed_ty) r.(k).
      Definition with_ty {t_loc t_tag t_ty t_unparsed_ty t_k} ty
        (r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
        Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) ty
          r.(unparsed_ty) r.(k).
      Definition with_unparsed_ty {t_loc t_tag t_ty t_unparsed_ty t_k}
        unparsed_ty (r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
        Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) r.(ty)
          unparsed_ty r.(k).
      Definition with_k {t_loc t_tag t_ty t_unparsed_ty t_k} k
        (r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
        Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) r.(ty)
          r.(unparsed_ty) k.
    End IEmit.
    Definition IEmit_skeleton := IEmit.record.
  End kinstr.
  Module typed_contract.
    Module Typed_originated.
      Record record {arg_ty contract_hash entrypoint : Set} : Set := Build {
        arg_ty : arg_ty;
        contract_hash : contract_hash;
        entrypoint : entrypoint;
      }.
      Arguments record : clear implicits.
      Definition with_arg_ty {t_arg_ty t_contract_hash t_entrypoint} arg_ty
        (r : record t_arg_ty t_contract_hash t_entrypoint) :=
        Build t_arg_ty t_contract_hash t_entrypoint arg_ty r.(contract_hash)
          r.(entrypoint).
      Definition with_contract_hash {t_arg_ty t_contract_hash t_entrypoint}
        contract_hash (r : record t_arg_ty t_contract_hash t_entrypoint) :=
        Build t_arg_ty t_contract_hash t_entrypoint r.(arg_ty) contract_hash
          r.(entrypoint).
      Definition with_entrypoint {t_arg_ty t_contract_hash t_entrypoint}
        entrypoint (r : record t_arg_ty t_contract_hash t_entrypoint) :=
        Build t_arg_ty t_contract_hash t_entrypoint r.(arg_ty) r.(contract_hash)
          entrypoint.
    End Typed_originated.
    Definition Typed_originated_skeleton := Typed_originated.record.

    Module Typed_tx_rollup.
      Record record {arg_ty tx_rollup : Set} : Set := Build {
        arg_ty : arg_ty;
        tx_rollup : tx_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_arg_ty {t_arg_ty t_tx_rollup} arg_ty
        (r : record t_arg_ty t_tx_rollup) :=
        Build t_arg_ty t_tx_rollup arg_ty r.(tx_rollup).
      Definition with_tx_rollup {t_arg_ty t_tx_rollup} tx_rollup
        (r : record t_arg_ty t_tx_rollup) :=
        Build t_arg_ty t_tx_rollup r.(arg_ty) tx_rollup.
    End Typed_tx_rollup.
    Definition Typed_tx_rollup_skeleton := Typed_tx_rollup.record.

    Module Typed_sc_rollup.
      Record record {arg_ty sc_rollup entrypoint : Set} : Set := Build {
        arg_ty : arg_ty;
        sc_rollup : sc_rollup;
        entrypoint : entrypoint;
      }.
      Arguments record : clear implicits.
      Definition with_arg_ty {t_arg_ty t_sc_rollup t_entrypoint} arg_ty
        (r : record t_arg_ty t_sc_rollup t_entrypoint) :=
        Build t_arg_ty t_sc_rollup t_entrypoint arg_ty r.(sc_rollup)
          r.(entrypoint).
      Definition with_sc_rollup {t_arg_ty t_sc_rollup t_entrypoint} sc_rollup
        (r : record t_arg_ty t_sc_rollup t_entrypoint) :=
        Build t_arg_ty t_sc_rollup t_entrypoint r.(arg_ty) sc_rollup
          r.(entrypoint).
      Definition with_entrypoint {t_arg_ty t_sc_rollup t_entrypoint} entrypoint
        (r : record t_arg_ty t_sc_rollup t_entrypoint) :=
        Build t_arg_ty t_sc_rollup t_entrypoint r.(arg_ty) r.(sc_rollup)
          entrypoint.
    End Typed_sc_rollup.
    Definition Typed_sc_rollup_skeleton := Typed_sc_rollup.record.

    Module Typed_zk_rollup.
      Record record {arg_ty zk_rollup : Set} : Set := Build {
        arg_ty : arg_ty;
        zk_rollup : zk_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_arg_ty {t_arg_ty t_zk_rollup} arg_ty
        (r : record t_arg_ty t_zk_rollup) :=
        Build t_arg_ty t_zk_rollup arg_ty r.(zk_rollup).
      Definition with_zk_rollup {t_arg_ty t_zk_rollup} zk_rollup
        (r : record t_arg_ty t_zk_rollup) :=
        Build t_arg_ty t_zk_rollup r.(arg_ty) zk_rollup.
    End Typed_zk_rollup.
    Definition Typed_zk_rollup_skeleton := Typed_zk_rollup.record.
  End typed_contract.
  Module big_map.
    Module Big_map.
      Record record {id diff key_type value_type : Set} : Set := Build {
        id : id;
        diff : diff;
        key_type : key_type;
        value_type : value_type;
      }.
      Arguments record : clear implicits.
      Definition with_id {t_id t_diff t_key_type t_value_type} id
        (r : record t_id t_diff t_key_type t_value_type) :=
        Build t_id t_diff t_key_type t_value_type id r.(diff) r.(key_type)
          r.(value_type).
      Definition with_diff {t_id t_diff t_key_type t_value_type} diff
        (r : record t_id t_diff t_key_type t_value_type) :=
        Build t_id t_diff t_key_type t_value_type r.(id) diff r.(key_type)
          r.(value_type).
      Definition with_key_type {t_id t_diff t_key_type t_value_type} key_type
        (r : record t_id t_diff t_key_type t_value_type) :=
        Build t_id t_diff t_key_type t_value_type r.(id) r.(diff) key_type
          r.(value_type).
      Definition with_value_type {t_id t_diff t_key_type t_value_type}
        value_type (r : record t_id t_diff t_key_type t_value_type) :=
        Build t_id t_diff t_key_type t_value_type r.(id) r.(diff) r.(key_type)
          value_type.
    End Big_map.
    Definition Big_map_skeleton := Big_map.record.
  End big_map.
  Module view_signature.
    Module View_signature.
      Record record {name input_ty output_ty : Set} : Set := Build {
        name : name;
        input_ty : input_ty;
        output_ty : output_ty;
      }.
      Arguments record : clear implicits.
      Definition with_name {t_name t_input_ty t_output_ty} name
        (r : record t_name t_input_ty t_output_ty) :=
        Build t_name t_input_ty t_output_ty name r.(input_ty) r.(output_ty).
      Definition with_input_ty {t_name t_input_ty t_output_ty} input_ty
        (r : record t_name t_input_ty t_output_ty) :=
        Build t_name t_input_ty t_output_ty r.(name) input_ty r.(output_ty).
      Definition with_output_ty {t_name t_input_ty t_output_ty} output_ty
        (r : record t_name t_input_ty t_output_ty) :=
        Build t_name t_input_ty t_output_ty r.(name) r.(input_ty) output_ty.
    End View_signature.
    Definition View_signature_skeleton := View_signature.record.
  End view_signature.
  Module internal_operation_contents.
    Module Transaction_to_implicit.
      Record record {destination amount : Set} : Set := Build {
        destination : destination;
        amount : amount;
      }.
      Arguments record : clear implicits.
      Definition with_destination {t_destination t_amount} destination
        (r : record t_destination t_amount) :=
        Build t_destination t_amount destination r.(amount).
      Definition with_amount {t_destination t_amount} amount
        (r : record t_destination t_amount) :=
        Build t_destination t_amount r.(destination) amount.
    End Transaction_to_implicit.
    Definition Transaction_to_implicit_skeleton :=
      Transaction_to_implicit.record.

    Module Transaction_to_smart_contract.
      Record record {destination amount entrypoint location parameters_ty
        parameters unparsed_parameters : Set} : Set := Build {
        destination : destination;
        amount : amount;
        entrypoint : entrypoint;
        location : location;
        parameters_ty : parameters_ty;
        parameters : parameters;
        unparsed_parameters : unparsed_parameters;
      }.
      Arguments record : clear implicits.
      Definition with_destination
        {t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters} destination
        (r :
          record t_destination t_amount t_entrypoint t_location t_parameters_ty
            t_parameters t_unparsed_parameters) :=
        Build t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters destination r.(amount)
          r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
          r.(unparsed_parameters).
      Definition with_amount
        {t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters} amount
        (r :
          record t_destination t_amount t_entrypoint t_location t_parameters_ty
            t_parameters t_unparsed_parameters) :=
        Build t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters r.(destination) amount
          r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
          r.(unparsed_parameters).
      Definition with_entrypoint
        {t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters} entrypoint
        (r :
          record t_destination t_amount t_entrypoint t_location t_parameters_ty
            t_parameters t_unparsed_parameters) :=
        Build t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters r.(destination) r.(amount)
          entrypoint r.(location) r.(parameters_ty) r.(parameters)
          r.(unparsed_parameters).
      Definition with_location
        {t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters} location
        (r :
          record t_destination t_amount t_entrypoint t_location t_parameters_ty
            t_parameters t_unparsed_parameters) :=
        Build t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters r.(destination) r.(amount)
          r.(entrypoint) location r.(parameters_ty) r.(parameters)
          r.(unparsed_parameters).
      Definition with_parameters_ty
        {t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters} parameters_ty
        (r :
          record t_destination t_amount t_entrypoint t_location t_parameters_ty
            t_parameters t_unparsed_parameters) :=
        Build t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters r.(destination) r.(amount)
          r.(entrypoint) r.(location) parameters_ty r.(parameters)
          r.(unparsed_parameters).
      Definition with_parameters
        {t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters} parameters
        (r :
          record t_destination t_amount t_entrypoint t_location t_parameters_ty
            t_parameters t_unparsed_parameters) :=
        Build t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters r.(destination) r.(amount)
          r.(entrypoint) r.(location) r.(parameters_ty) parameters
          r.(unparsed_parameters).
      Definition with_unparsed_parameters
        {t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters} unparsed_parameters
        (r :
          record t_destination t_amount t_entrypoint t_location t_parameters_ty
            t_parameters t_unparsed_parameters) :=
        Build t_destination t_amount t_entrypoint t_location t_parameters_ty
          t_parameters t_unparsed_parameters r.(destination) r.(amount)
          r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
          unparsed_parameters.
    End Transaction_to_smart_contract.
    Definition Transaction_to_smart_contract_skeleton :=
      Transaction_to_smart_contract.record.

    Module Transaction_to_tx_rollup.
      Record record {destination parameters_ty parameters unparsed_parameters :
        Set} : Set := Build {
        destination : destination;
        parameters_ty : parameters_ty;
        parameters : parameters;
        unparsed_parameters : unparsed_parameters;
      }.
      Arguments record : clear implicits.
      Definition with_destination
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        destination
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          destination r.(parameters_ty) r.(parameters) r.(unparsed_parameters).
      Definition with_parameters_ty
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        parameters_ty
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          r.(destination) parameters_ty r.(parameters) r.(unparsed_parameters).
      Definition with_parameters
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        parameters
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          r.(destination) r.(parameters_ty) parameters r.(unparsed_parameters).
      Definition with_unparsed_parameters
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        unparsed_parameters
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          r.(destination) r.(parameters_ty) r.(parameters) unparsed_parameters.
    End Transaction_to_tx_rollup.
    Definition Transaction_to_tx_rollup_skeleton :=
      Transaction_to_tx_rollup.record.

    Module Transaction_to_sc_rollup.
      Record record {destination entrypoint parameters_ty parameters
        unparsed_parameters : Set} : Set := Build {
        destination : destination;
        entrypoint : entrypoint;
        parameters_ty : parameters_ty;
        parameters : parameters;
        unparsed_parameters : unparsed_parameters;
      }.
      Arguments record : clear implicits.
      Definition with_destination
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} destination
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters destination r.(entrypoint) r.(parameters_ty)
          r.(parameters) r.(unparsed_parameters).
      Definition with_entrypoint
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} entrypoint
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) entrypoint r.(parameters_ty)
          r.(parameters) r.(unparsed_parameters).
      Definition with_parameters_ty
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} parameters_ty
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) r.(entrypoint) parameters_ty
          r.(parameters) r.(unparsed_parameters).
      Definition with_parameters
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} parameters
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
          parameters r.(unparsed_parameters).
      Definition with_unparsed_parameters
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} unparsed_parameters
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
          r.(parameters) unparsed_parameters.
    End Transaction_to_sc_rollup.
    Definition Transaction_to_sc_rollup_skeleton :=
      Transaction_to_sc_rollup.record.

    Module Event.
      Record record {ty tag unparsed_data : Set} : Set := Build {
        ty : ty;
        tag : tag;
        unparsed_data : unparsed_data;
      }.
      Arguments record : clear implicits.
      Definition with_ty {t_ty t_tag t_unparsed_data} ty
        (r : record t_ty t_tag t_unparsed_data) :=
        Build t_ty t_tag t_unparsed_data ty r.(tag) r.(unparsed_data).
      Definition with_tag {t_ty t_tag t_unparsed_data} tag
        (r : record t_ty t_tag t_unparsed_data) :=
        Build t_ty t_tag t_unparsed_data r.(ty) tag r.(unparsed_data).
      Definition with_unparsed_data {t_ty t_tag t_unparsed_data} unparsed_data
        (r : record t_ty t_tag t_unparsed_data) :=
        Build t_ty t_tag t_unparsed_data r.(ty) r.(tag) unparsed_data.
    End Event.
    Definition Event_skeleton := Event.record.

    Module Transaction_to_zk_rollup.
      Record record {destination parameters_ty parameters unparsed_parameters :
        Set} : Set := Build {
        destination : destination;
        parameters_ty : parameters_ty;
        parameters : parameters;
        unparsed_parameters : unparsed_parameters;
      }.
      Arguments record : clear implicits.
      Definition with_destination
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        destination
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          destination r.(parameters_ty) r.(parameters) r.(unparsed_parameters).
      Definition with_parameters_ty
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        parameters_ty
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          r.(destination) parameters_ty r.(parameters) r.(unparsed_parameters).
      Definition with_parameters
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        parameters
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          r.(destination) r.(parameters_ty) parameters r.(unparsed_parameters).
      Definition with_unparsed_parameters
        {t_destination t_parameters_ty t_parameters t_unparsed_parameters}
        unparsed_parameters
        (r :
          record t_destination t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
          r.(destination) r.(parameters_ty) r.(parameters) unparsed_parameters.
    End Transaction_to_zk_rollup.
    Definition Transaction_to_zk_rollup_skeleton :=
      Transaction_to_zk_rollup.record.

    Module Origination.
      Record record {delegate code unparsed_storage credit preorigination
        storage_type storage : Set} : Set := Build {
        delegate : delegate;
        code : code;
        unparsed_storage : unparsed_storage;
        credit : credit;
        preorigination : preorigination;
        storage_type : storage_type;
        storage : storage;
      }.
      Arguments record : clear implicits.
      Definition with_delegate
        {t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage} delegate
        (r :
          record t_delegate t_code t_unparsed_storage t_credit t_preorigination
            t_storage_type t_storage) :=
        Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage delegate r.(code) r.(unparsed_storage)
          r.(credit) r.(preorigination) r.(storage_type) r.(storage).
      Definition with_code
        {t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage} code
        (r :
          record t_delegate t_code t_unparsed_storage t_credit t_preorigination
            t_storage_type t_storage) :=
        Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage r.(delegate) code r.(unparsed_storage)
          r.(credit) r.(preorigination) r.(storage_type) r.(storage).
      Definition with_unparsed_storage
        {t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage} unparsed_storage
        (r :
          record t_delegate t_code t_unparsed_storage t_credit t_preorigination
            t_storage_type t_storage) :=
        Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage r.(delegate) r.(code) unparsed_storage
          r.(credit) r.(preorigination) r.(storage_type) r.(storage).
      Definition with_credit
        {t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage} credit
        (r :
          record t_delegate t_code t_unparsed_storage t_credit t_preorigination
            t_storage_type t_storage) :=
        Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
          credit r.(preorigination) r.(storage_type) r.(storage).
      Definition with_preorigination
        {t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage} preorigination
        (r :
          record t_delegate t_code t_unparsed_storage t_credit t_preorigination
            t_storage_type t_storage) :=
        Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
          r.(credit) preorigination r.(storage_type) r.(storage).
      Definition with_storage_type
        {t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage} storage_type
        (r :
          record t_delegate t_code t_unparsed_storage t_credit t_preorigination
            t_storage_type t_storage) :=
        Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
          r.(credit) r.(preorigination) storage_type r.(storage).
      Definition with_storage
        {t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage} storage
        (r :
          record t_delegate t_code t_unparsed_storage t_credit t_preorigination
            t_storage_type t_storage) :=
        Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
          t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
          r.(credit) r.(preorigination) r.(storage_type) storage.
    End Origination.
    Definition Origination_skeleton := Origination.record.
  End internal_operation_contents.
End
  ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
Import
  ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.

Module operation.
  Record record {piop lazy_storage_diff : Set} : Set := Build {
    piop : piop;
    lazy_storage_diff : lazy_storage_diff;
  }.
  Arguments record : clear implicits.
  Definition with_piop {t_piop t_lazy_storage_diff} piop
    (r : record t_piop t_lazy_storage_diff) :=
    Build t_piop t_lazy_storage_diff piop r.(lazy_storage_diff).
  Definition with_lazy_storage_diff {t_piop t_lazy_storage_diff}
    lazy_storage_diff (r : record t_piop t_lazy_storage_diff) :=
    Build t_piop t_lazy_storage_diff r.(piop) lazy_storage_diff.
End operation.
Definition operation_skeleton := operation.record.

Module internal_operation.
  Record record {source operation nonce : Set} : Set := Build {
    source : source;
    operation : operation;
    nonce : nonce;
  }.
  Arguments record : clear implicits.
  Definition with_source {t_source t_operation t_nonce} source
    (r : record t_source t_operation t_nonce) :=
    Build t_source t_operation t_nonce source r.(operation) r.(nonce).
  Definition with_operation {t_source t_operation t_nonce} operation
    (r : record t_source t_operation t_nonce) :=
    Build t_source t_operation t_nonce r.(source) operation r.(nonce).
  Definition with_nonce {t_source t_operation t_nonce} nonce
    (r : record t_source t_operation t_nonce) :=
    Build t_source t_operation t_nonce r.(source) r.(operation) nonce.
End internal_operation.
Definition internal_operation_skeleton := internal_operation.record.

Module kdescr.
  Record record {kloc kbef kaft kinstr : Set} : Set := Build {
    kloc : kloc;
    kbef : kbef;
    kaft : kaft;
    kinstr : kinstr;
  }.
  Arguments record : clear implicits.
  Definition with_kloc {t_kloc t_kbef t_kaft t_kinstr} kloc
    (r : record t_kloc t_kbef t_kaft t_kinstr) :=
    Build t_kloc t_kbef t_kaft t_kinstr kloc r.(kbef) r.(kaft) r.(kinstr).
  Definition with_kbef {t_kloc t_kbef t_kaft t_kinstr} kbef
    (r : record t_kloc t_kbef t_kaft t_kinstr) :=
    Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) kbef r.(kaft) r.(kinstr).
  Definition with_kaft {t_kloc t_kbef t_kaft t_kinstr} kaft
    (r : record t_kloc t_kbef t_kaft t_kinstr) :=
    Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) r.(kbef) kaft r.(kinstr).
  Definition with_kinstr {t_kloc t_kbef t_kaft t_kinstr} kinstr
    (r : record t_kloc t_kbef t_kaft t_kinstr) :=
    Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) r.(kbef) r.(kaft) kinstr.
End kdescr.
Definition kdescr_skeleton := kdescr.record.

Module logger.
  Record record {log_interp log_entry log_control log_exit get_log : Set} : Set := Build {
    log_interp : log_interp;
    log_entry : log_entry;
    log_control : log_control;
    log_exit : log_exit;
    get_log : get_log;
  }.
  Arguments record : clear implicits.
  Definition with_log_interp
    {t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_interp
    (r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
    Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log log_interp
      r.(log_entry) r.(log_control) r.(log_exit) r.(get_log).
  Definition with_log_entry
    {t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_entry
    (r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
    Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
      r.(log_interp) log_entry r.(log_control) r.(log_exit) r.(get_log).
  Definition with_log_control
    {t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_control
    (r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
    Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
      r.(log_interp) r.(log_entry) log_control r.(log_exit) r.(get_log).
  Definition with_log_exit
    {t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_exit
    (r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
    Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
      r.(log_interp) r.(log_entry) r.(log_control) log_exit r.(get_log).
  Definition with_get_log
    {t_log_interp t_log_entry t_log_control t_log_exit t_get_log} get_log
    (r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
    Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
      r.(log_interp) r.(log_entry) r.(log_control) r.(log_exit) get_log.
End logger.
Definition logger_skeleton := logger.record.

Module entrypoints.
  Record record {root original_type_expr : Set} : Set := Build {
    root : root;
    original_type_expr : original_type_expr;
  }.
  Arguments record : clear implicits.
  Definition with_root {t_root t_original_type_expr} root
    (r : record t_root t_original_type_expr) :=
    Build t_root t_original_type_expr root r.(original_type_expr).
  Definition with_original_type_expr {t_root t_original_type_expr}
    original_type_expr (r : record t_root t_original_type_expr) :=
    Build t_root t_original_type_expr r.(root) original_type_expr.
End entrypoints.
Definition entrypoints_skeleton := entrypoints.record.

Reserved Notation "'kinstr.IIf_none".
Reserved Notation "'kinstr.IOpt_map".
Reserved Notation "'kinstr.IIf_left".
Reserved Notation "'kinstr.IIf_cons".
Reserved Notation "'kinstr.IIf".
Reserved Notation "'kinstr.ICreate_contract".
Reserved Notation "'kinstr.IEmit".
Reserved Notation "'typed_contract.Typed_originated".
Reserved Notation "'typed_contract.Typed_tx_rollup".
Reserved Notation "'typed_contract.Typed_sc_rollup".
Reserved Notation "'typed_contract.Typed_zk_rollup".
Reserved Notation "'big_map.Big_map".
Reserved Notation "'view_signature.View_signature".
Reserved Notation "'internal_operation_contents.Transaction_to_implicit".
Reserved Notation "'internal_operation_contents.Transaction_to_smart_contract".
Reserved Notation "'internal_operation_contents.Transaction_to_tx_rollup".
Reserved Notation "'internal_operation_contents.Transaction_to_sc_rollup".
Reserved Notation "'internal_operation_contents.Event".
Reserved Notation "'internal_operation_contents.Transaction_to_zk_rollup".
Reserved Notation "'internal_operation_contents.Origination".
Reserved Notation "'entrypoints".
Reserved Notation "'logging_function".
Reserved Notation "'execution_trace".
Reserved Notation "'logger".
Reserved Notation "'comparable_ty".
Reserved Notation "'kdescr".
Reserved Notation "'internal_operation".
Reserved Notation "'operation".

Inductive kinstr : Set :=
| IDrop : Alpha_context.Script.location kinstr kinstr
| IDup : Alpha_context.Script.location kinstr kinstr
| ISwap : Alpha_context.Script.location kinstr kinstr
| IConst : {t : Set},
  Alpha_context.Script.location ty t kinstr kinstr
| ICons_pair : Alpha_context.Script.location kinstr kinstr
| ICar : Alpha_context.Script.location kinstr kinstr
| ICdr : Alpha_context.Script.location kinstr kinstr
| IUnpair : Alpha_context.Script.location kinstr kinstr
| ICons_some : Alpha_context.Script.location kinstr kinstr
| ICons_none : Alpha_context.Script.location ty kinstr kinstr
| IIf_none : 'kinstr.IIf_none kinstr
| IOpt_map : 'kinstr.IOpt_map kinstr
| ICons_left : Alpha_context.Script.location ty kinstr kinstr
| ICons_right : Alpha_context.Script.location ty kinstr kinstr
| IIf_left : 'kinstr.IIf_left kinstr
| ICons_list : Alpha_context.Script.location kinstr kinstr
| INil : Alpha_context.Script.location ty kinstr kinstr
| IIf_cons : 'kinstr.IIf_cons kinstr
| IList_map :
  Alpha_context.Script.location kinstr option ty kinstr kinstr
| IList_iter :
  Alpha_context.Script.location option ty kinstr kinstr kinstr
| IList_size : Alpha_context.Script.location kinstr kinstr
| IEmpty_set :
  Alpha_context.Script.location 'comparable_ty kinstr kinstr
| ISet_iter :
  Alpha_context.Script.location option 'comparable_ty kinstr kinstr
  kinstr
| ISet_mem : Alpha_context.Script.location kinstr kinstr
| ISet_update : Alpha_context.Script.location kinstr kinstr
| ISet_size : Alpha_context.Script.location kinstr kinstr
| IEmpty_map :
  Alpha_context.Script.location 'comparable_ty option ty kinstr
  kinstr
| IMap_map :
  Alpha_context.Script.location option ty kinstr kinstr kinstr
| IMap_iter :
  Alpha_context.Script.location option ty kinstr kinstr kinstr
| IMap_mem : Alpha_context.Script.location kinstr kinstr
| IMap_get : Alpha_context.Script.location kinstr kinstr
| IMap_update : Alpha_context.Script.location kinstr kinstr
| IMap_get_and_update : Alpha_context.Script.location kinstr kinstr
| IMap_size : Alpha_context.Script.location kinstr kinstr
| IEmpty_big_map :
  Alpha_context.Script.location 'comparable_ty ty kinstr kinstr
| IBig_map_mem : Alpha_context.Script.location kinstr kinstr
| IBig_map_get : Alpha_context.Script.location kinstr kinstr
| IBig_map_update : Alpha_context.Script.location kinstr kinstr
| IBig_map_get_and_update : Alpha_context.Script.location kinstr kinstr
| IConcat_string : Alpha_context.Script.location kinstr kinstr
| IConcat_string_pair : Alpha_context.Script.location kinstr kinstr
| ISlice_string : Alpha_context.Script.location kinstr kinstr
| IString_size : Alpha_context.Script.location kinstr kinstr
| IConcat_bytes : Alpha_context.Script.location kinstr kinstr
| IConcat_bytes_pair : Alpha_context.Script.location kinstr kinstr
| ISlice_bytes : Alpha_context.Script.location kinstr kinstr
| IBytes_size : Alpha_context.Script.location kinstr kinstr
| IAdd_seconds_to_timestamp : Alpha_context.Script.location kinstr kinstr
| IAdd_timestamp_to_seconds : Alpha_context.Script.location kinstr kinstr
| ISub_timestamp_seconds : Alpha_context.Script.location kinstr kinstr
| IDiff_timestamps : Alpha_context.Script.location kinstr kinstr
| IAdd_tez : Alpha_context.Script.location kinstr kinstr
| ISub_tez : Alpha_context.Script.location kinstr kinstr
| ISub_tez_legacy : Alpha_context.Script.location kinstr kinstr
| IMul_teznat : Alpha_context.Script.location kinstr kinstr
| IMul_nattez : Alpha_context.Script.location kinstr kinstr
| IEdiv_teznat : Alpha_context.Script.location kinstr kinstr
| IEdiv_tez : Alpha_context.Script.location kinstr kinstr
| IOr : Alpha_context.Script.location kinstr kinstr
| IAnd : Alpha_context.Script.location kinstr kinstr
| IXor : Alpha_context.Script.location kinstr kinstr
| INot : Alpha_context.Script.location kinstr kinstr
| IIs_nat : Alpha_context.Script.location kinstr kinstr
| INeg : Alpha_context.Script.location kinstr kinstr
| IAbs_int : Alpha_context.Script.location kinstr kinstr
| IInt_nat : Alpha_context.Script.location kinstr kinstr
| IAdd_int : Alpha_context.Script.location kinstr kinstr
| IAdd_nat : Alpha_context.Script.location kinstr kinstr
| ISub_int : Alpha_context.Script.location kinstr kinstr
| IMul_int : Alpha_context.Script.location kinstr kinstr
| IMul_nat : Alpha_context.Script.location kinstr kinstr
| IEdiv_int : Alpha_context.Script.location kinstr kinstr
| IEdiv_nat : Alpha_context.Script.location kinstr kinstr
| ILsl_nat : Alpha_context.Script.location kinstr kinstr
| ILsr_nat : Alpha_context.Script.location kinstr kinstr
| IOr_nat : Alpha_context.Script.location kinstr kinstr
| IAnd_nat : Alpha_context.Script.location kinstr kinstr
| IAnd_int_nat : Alpha_context.Script.location kinstr kinstr
| IXor_nat : Alpha_context.Script.location kinstr kinstr
| INot_int : Alpha_context.Script.location kinstr kinstr
| IIf : 'kinstr.IIf kinstr
| ILoop : Alpha_context.Script.location kinstr kinstr kinstr
| ILoop_left : Alpha_context.Script.location kinstr kinstr kinstr
| IDip :
  Alpha_context.Script.location kinstr option ty kinstr kinstr
| IExec : Alpha_context.Script.location option stack_ty kinstr kinstr
| IApply : Alpha_context.Script.location ty kinstr kinstr
| ILambda : Alpha_context.Script.location lambda kinstr kinstr
| IFailwith : Alpha_context.Script.location ty kinstr
| ICompare : Alpha_context.Script.location 'comparable_ty kinstr kinstr
| IEq : Alpha_context.Script.location kinstr kinstr
| INeq : Alpha_context.Script.location kinstr kinstr
| ILt : Alpha_context.Script.location kinstr kinstr
| IGt : Alpha_context.Script.location kinstr kinstr
| ILe : Alpha_context.Script.location kinstr kinstr
| IGe : Alpha_context.Script.location kinstr kinstr
| IAddress : Alpha_context.Script.location kinstr kinstr
| IContract :
  Alpha_context.Script.location ty Alpha_context.Entrypoint.t kinstr
  kinstr
| IView :
  Alpha_context.Script.location view_signature option stack_ty
  kinstr kinstr
| ITransfer_tokens : Alpha_context.Script.location kinstr kinstr
| IImplicit_account : Alpha_context.Script.location kinstr kinstr
| ICreate_contract : 'kinstr.ICreate_contract kinstr
| ISet_delegate : Alpha_context.Script.location kinstr kinstr
| INow : Alpha_context.Script.location kinstr kinstr
| IMin_block_time : Alpha_context.Script.location kinstr kinstr
| IBalance : Alpha_context.Script.location kinstr kinstr
| ILevel : Alpha_context.Script.location kinstr kinstr
| ICheck_signature : Alpha_context.Script.location kinstr kinstr
| IHash_key : Alpha_context.Script.location kinstr kinstr
| IPack : Alpha_context.Script.location ty kinstr kinstr
| IUnpack : Alpha_context.Script.location ty kinstr kinstr
| IBlake2b : Alpha_context.Script.location kinstr kinstr
| ISha256 : Alpha_context.Script.location kinstr kinstr
| ISha512 : Alpha_context.Script.location kinstr kinstr
| ISource : Alpha_context.Script.location kinstr kinstr
| ISender : Alpha_context.Script.location kinstr kinstr
| ISelf :
  Alpha_context.Script.location ty Alpha_context.Entrypoint.t kinstr
  kinstr
| ISelf_address : Alpha_context.Script.location kinstr kinstr
| IAmount : Alpha_context.Script.location kinstr kinstr
| ISapling_empty_state :
  Alpha_context.Script.location Alpha_context.Sapling.Memo_size.t
  kinstr kinstr
| ISapling_verify_update : Alpha_context.Script.location kinstr kinstr
| ISapling_verify_update_deprecated :
  Alpha_context.Script.location kinstr kinstr
| IDig :
  Alpha_context.Script.location int stack_prefix_preservation_witness
  kinstr kinstr
| IDug :
  Alpha_context.Script.location int stack_prefix_preservation_witness
  kinstr kinstr
| IDipn :
  Alpha_context.Script.location int stack_prefix_preservation_witness
  kinstr kinstr kinstr
| IDropn :
  Alpha_context.Script.location int stack_prefix_preservation_witness
  kinstr kinstr
| IChainId : Alpha_context.Script.location kinstr kinstr
| INever : Alpha_context.Script.location kinstr
| IVoting_power : Alpha_context.Script.location kinstr kinstr
| ITotal_voting_power : Alpha_context.Script.location kinstr kinstr
| IKeccak : Alpha_context.Script.location kinstr kinstr
| ISha3 : Alpha_context.Script.location kinstr kinstr
| IAdd_bls12_381_g1 : Alpha_context.Script.location kinstr kinstr
| IAdd_bls12_381_g2 : Alpha_context.Script.location kinstr kinstr
| IAdd_bls12_381_fr : Alpha_context.Script.location kinstr kinstr
| IMul_bls12_381_g1 : Alpha_context.Script.location kinstr kinstr
| IMul_bls12_381_g2 : Alpha_context.Script.location kinstr kinstr
| IMul_bls12_381_fr : Alpha_context.Script.location kinstr kinstr
| IMul_bls12_381_z_fr : Alpha_context.Script.location kinstr kinstr
| IMul_bls12_381_fr_z : Alpha_context.Script.location kinstr kinstr
| IInt_bls12_381_fr : Alpha_context.Script.location kinstr kinstr
| INeg_bls12_381_g1 : Alpha_context.Script.location kinstr kinstr
| INeg_bls12_381_g2 : Alpha_context.Script.location kinstr kinstr
| INeg_bls12_381_fr : Alpha_context.Script.location kinstr kinstr
| IPairing_check_bls12_381 : Alpha_context.Script.location kinstr kinstr
| IComb :
  Alpha_context.Script.location int comb_gadt_witness kinstr kinstr
| IUncomb :
  Alpha_context.Script.location int uncomb_gadt_witness kinstr
  kinstr
| IComb_get :
  Alpha_context.Script.location int comb_get_gadt_witness kinstr
  kinstr
| IComb_set :
  Alpha_context.Script.location int comb_set_gadt_witness kinstr
  kinstr
| IDup_n :
  Alpha_context.Script.location int dup_n_gadt_witness kinstr kinstr
| ITicket :
  Alpha_context.Script.location option 'comparable_ty kinstr kinstr
| ITicket_deprecated :
  Alpha_context.Script.location option 'comparable_ty kinstr kinstr
| IRead_ticket :
  Alpha_context.Script.location option 'comparable_ty kinstr kinstr
| ISplit_ticket : Alpha_context.Script.location kinstr kinstr
| IJoin_tickets :
  Alpha_context.Script.location 'comparable_ty kinstr kinstr
| IOpen_chest : Alpha_context.Script.location kinstr kinstr
| IEmit : 'kinstr.IEmit kinstr
| IHalt : Alpha_context.Script.location kinstr
| ILog :
  Alpha_context.Script.location stack_ty logging_event 'logger
  kinstr kinstr

with lambda : Set :=
| Lam : 'kdescr Alpha_context.Script.node lambda
| LamRec : 'kdescr Alpha_context.Script.node lambda

with typed_contract : Set :=
| Typed_implicit : Alpha_context.public_key_hash typed_contract
| Typed_originated : 'typed_contract.Typed_originated typed_contract
| Typed_tx_rollup : 'typed_contract.Typed_tx_rollup typed_contract
| Typed_sc_rollup : 'typed_contract.Typed_sc_rollup typed_contract
| Typed_zk_rollup : 'typed_contract.Typed_zk_rollup typed_contract

with continuation : Set :=
| KNil : continuation
| KCons : kinstr continuation continuation
| KReturn : {s : Set},
  s option stack_ty continuation continuation
| KMap_head : {a b : Set}, (a b) continuation continuation
| KUndip : {b : Set}, b option ty continuation continuation
| KLoop_in : kinstr continuation continuation
| KLoop_in_left : kinstr continuation continuation
| KIter : {a : Set},
  kinstr option ty list a continuation continuation
| KList_enter_body : {a b : Set},
  kinstr list a list b option ty int continuation continuation
| KList_exit_body : {a b : Set},
  kinstr list a list b option ty int continuation continuation
| KMap_enter_body : {a b c : Set},
  kinstr list (a × b) map a c option ty continuation continuation
| KMap_exit_body : {a b c : Set},
  kinstr list (a × b) map a c a option ty continuation
  continuation
| KView_exit : step_constants continuation continuation
| KLog : continuation stack_ty 'logger continuation

with ty : Set :=
| Unit_t : ty
| Int_t : ty
| Nat_t : ty
| Signature_t : ty
| String_t : ty
| Bytes_t : ty
| Mutez_t : ty
| Key_hash_t : ty
| Key_t : ty
| Timestamp_t : ty
| Address_t : ty
| Tx_rollup_l2_address_t : ty
| Bool_t : ty
| Pair_t : ty ty ty_metadata Dependent_bool.dand ty
| Union_t : ty ty ty_metadata Dependent_bool.dand ty
| Lambda_t : ty ty ty_metadata ty
| Option_t : ty ty_metadata Dependent_bool.dbool ty
| List_t : ty ty_metadata ty
| Set_t : 'comparable_ty ty_metadata ty
| Map_t : 'comparable_ty ty ty_metadata ty
| Big_map_t : 'comparable_ty ty ty_metadata ty
| Contract_t : ty ty_metadata ty
| Sapling_transaction_t : Alpha_context.Sapling.Memo_size.t ty
| Sapling_transaction_deprecated_t : Alpha_context.Sapling.Memo_size.t ty
| Sapling_state_t : Alpha_context.Sapling.Memo_size.t ty
| Operation_t : ty
| Chain_id_t : ty
| Never_t : ty
| Bls12_381_g1_t : ty
| Bls12_381_g2_t : ty
| Bls12_381_fr_t : ty
| Ticket_t : 'comparable_ty ty_metadata ty
| Chest_key_t : ty
| Chest_t : ty

with stack_ty : Set :=
| Item_t : ty stack_ty stack_ty
| Bot_t : stack_ty

with big_map : Set :=
| Big_map : {key value : Set}, 'big_map.Big_map key value big_map

with stack_prefix_preservation_witness : Set :=
| KPrefix :
  Alpha_context.Script.location ty stack_prefix_preservation_witness
  stack_prefix_preservation_witness
| KRest : stack_prefix_preservation_witness

with comb_gadt_witness : Set :=
| Comb_one : comb_gadt_witness
| Comb_succ : comb_gadt_witness comb_gadt_witness

with uncomb_gadt_witness : Set :=
| Uncomb_one : uncomb_gadt_witness
| Uncomb_succ : uncomb_gadt_witness uncomb_gadt_witness

with comb_get_gadt_witness : Set :=
| Comb_get_zero : comb_get_gadt_witness
| Comb_get_one : comb_get_gadt_witness
| Comb_get_plus_two : comb_get_gadt_witness comb_get_gadt_witness

with comb_set_gadt_witness : Set :=
| Comb_set_zero : comb_set_gadt_witness
| Comb_set_one : comb_set_gadt_witness
| Comb_set_plus_two : comb_set_gadt_witness comb_set_gadt_witness

with dup_n_gadt_witness : Set :=
| Dup_n_zero : dup_n_gadt_witness
| Dup_n_succ : dup_n_gadt_witness dup_n_gadt_witness

with view_signature : Set :=
| View_signature : 'view_signature.View_signature view_signature

with internal_operation_contents : Set :=
| Transaction_to_implicit :
  'internal_operation_contents.Transaction_to_implicit
  internal_operation_contents
| Transaction_to_smart_contract : {a : Set},
  'internal_operation_contents.Transaction_to_smart_contract a
  internal_operation_contents
| Transaction_to_tx_rollup : {a : Set},
  'internal_operation_contents.Transaction_to_tx_rollup a
  internal_operation_contents
| Transaction_to_sc_rollup : {a : Set},
  'internal_operation_contents.Transaction_to_sc_rollup a
  internal_operation_contents
| Event : 'internal_operation_contents.Event internal_operation_contents
| Transaction_to_zk_rollup : {a : Set},
  'internal_operation_contents.Transaction_to_zk_rollup a
  internal_operation_contents
| Origination : {storage : Set},
  'internal_operation_contents.Origination storage
  internal_operation_contents
| Delegation : option Signature.public_key_hash internal_operation_contents

with packed_internal_operation : Set :=
| Internal_operation : 'internal_operation packed_internal_operation

where "'entrypoints" :=
  (entrypoints_skeleton entrypoints_node Alpha_context.Script.node)
and "'logging_function" :=
  (fun (t_c t_u : Set) ⇒ kinstr Alpha_context.context
  Alpha_context.Script.location stack_ty t_c × t_u unit)
and "'execution_trace" :=
  (list
    (Alpha_context.Script.location × Alpha_context.Gas.t ×
      list Alpha_context.Script.expr))
and "'comparable_ty" := ((fun _ty) tt)
and "'kdescr" :=
  (kdescr_skeleton Alpha_context.Script.location stack_ty stack_ty kinstr)
and "'internal_operation" :=
  (internal_operation_skeleton Alpha_context.Contract.t
    internal_operation_contents int)
and "'operation" :=
  (operation_skeleton packed_internal_operation
    (option Alpha_context.Lazy_storage.diffs))
and "'logger" :=
  (logger_skeleton ( {c u : Set}, 'logging_function c u)
    ( {a s : Set}, 'logging_function a s) (continuation unit)
    ( {c u : Set}, 'logging_function c u)
    (unit M? (option 'execution_trace)))
and "'kinstr.IIf_none" :=
  (kinstr.IIf_none_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IOpt_map" :=
  (kinstr.IOpt_map_skeleton Alpha_context.Script.location kinstr kinstr)
and "'kinstr.IIf_left" :=
  (kinstr.IIf_left_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IIf_cons" :=
  (kinstr.IIf_cons_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IIf" :=
  (kinstr.IIf_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.ICreate_contract" :=
  (kinstr.ICreate_contract_skeleton Alpha_context.Script.location ty
    Alpha_context.Script.expr kinstr)
and "'kinstr.IEmit" :=
  (kinstr.IEmit_skeleton Alpha_context.Script.location
    Alpha_context.Entrypoint.t ty Alpha_context.Script.expr kinstr)
and "'typed_contract.Typed_originated" :=
  (typed_contract.Typed_originated_skeleton ty Contract_hash.t
    Alpha_context.Entrypoint.t)
and "'typed_contract.Typed_tx_rollup" :=
  (typed_contract.Typed_tx_rollup_skeleton ty Alpha_context.Tx_rollup.t)
and "'typed_contract.Typed_sc_rollup" :=
  (typed_contract.Typed_sc_rollup_skeleton ty Alpha_context.Sc_rollup.t
    Alpha_context.Entrypoint.t)
and "'typed_contract.Typed_zk_rollup" :=
  (typed_contract.Typed_zk_rollup_skeleton ty Alpha_context.Zk_rollup.t)
and "'big_map.Big_map" :=
  (fun (t_key t_value : Set) ⇒ big_map.Big_map_skeleton
    (option Alpha_context.Big_map.Id.t) (big_map_overlay t_key t_value)
    'comparable_ty ty)
and "'view_signature.View_signature" :=
  (view_signature.View_signature_skeleton Script_string.t ty ty)
and "'internal_operation_contents.Transaction_to_implicit" :=
  (internal_operation_contents.Transaction_to_implicit_skeleton
    Signature.public_key_hash Alpha_context.Tez.tez)
and "'internal_operation_contents.Transaction_to_smart_contract" :=
  (fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_smart_contract_skeleton