Skip to main content

๐Ÿฌย Script_typed_ir.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.

Module step_constants.
  Record record : Set := Build {
    source : Alpha_context.Contract.t;
    payer : Alpha_context.Contract.t;
    self : Alpha_context.Contract.t;
    amount : Alpha_context.Tez.t;
    balance : Alpha_context.Tez.t;
    chain_id : Chain_id.t;
    now : Alpha_context.Script_timestamp.t;
    level : Alpha_context.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 : Bls12_381.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 (Bls12_381.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 (Bls12_381.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 (Bls12_381.Fr.(S.PRIME_FIELD.negate) x_value).

    Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
      Option.map
        (fun (x_value : Bls12_381.Fr.(S.PRIME_FIELD.t)) โ‡’ Fr_tag x_value)
        (Bls12_381.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
      Bls12_381.Fr.(S.PRIME_FIELD.to_bytes) x_value.

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

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

  Module G1.
    Inductive t : Set :=
    | G1_tag : Bls12_381.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 (Bls12_381.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 (Bls12_381.G1.(S.CURVE.mul) x_value y_value).

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

    Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
      Option.map (fun (x_value : Bls12_381.G1.(S.CURVE.t)) โ‡’ G1_tag x_value)
        (Bls12_381.G1.(S.CURVE.of_bytes_opt) bytes_value).

    Definition to_bytes (function_parameter : t) : Bytes.t :=
      let 'G1_tag x_value := function_parameter in
      Bls12_381.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 : Bls12_381.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 (Bls12_381.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 (Bls12_381.G2.(S.CURVE.mul) x_value y_value).

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

    Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
      Option.map (fun (x_value : Bls12_381.G2.(S.CURVE.t)) โ‡’ G2_tag x_value)
        (Bls12_381.G2.(S.CURVE.of_bytes_opt) bytes_value).

    Definition to_bytes (function_parameter : t) : Bytes.t :=
      let 'G2_tag x_value := function_parameter in
      Bls12_381.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
    Bls12_381.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.

Module ticket.
  Record record {a : Set} : Set := Build {
    ticketer : Alpha_context.Contract.t;
    contents : a;
    amount : Alpha_context.Script_int.num;
  }.
  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_trace : Set},
      Script_tc_errors.error_details โ†’ 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 {error_trace : Set}
    (error_details : Script_tc_errors.error_details) (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 Alpha_context.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; |}.

Module entrypoints.
  Record record : Set := Build {
    root : entrypoints_node;
    original_type_expr : Alpha_context.Script.node;
  }.
  Definition with_root root (r : record) :=
    Build root r.(original_type_expr).
  Definition with_original_type_expr original_type_expr (r : record) :=
    Build r.(root) original_type_expr.
End entrypoints.
Definition entrypoints := entrypoints.record.

Records for the constructor parameters
Module
  ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
  Module script.
    Module Script.
      Record record {code arg_type storage storage_type views entrypoints
        code_size : Set} : Set := Build {
        code : code;
        arg_type : arg_type;
        storage : storage;
        storage_type : storage_type;
        views : views;
        entrypoints : entrypoints;
        code_size : code_size;
      }.
      Arguments record : clear implicits.
      Definition with_code
        {t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size} code
        (r :
          record t_code t_arg_type t_storage t_storage_type t_views
            t_entrypoints t_code_size) :=
        Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size code r.(arg_type) r.(storage) r.(storage_type) r.(views)
          r.(entrypoints) r.(code_size).
      Definition with_arg_type
        {t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size} arg_type
        (r :
          record t_code t_arg_type t_storage t_storage_type t_views
            t_entrypoints t_code_size) :=
        Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size r.(code) arg_type r.(storage) r.(storage_type) r.(views)
          r.(entrypoints) r.(code_size).
      Definition with_storage
        {t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size} storage
        (r :
          record t_code t_arg_type t_storage t_storage_type t_views
            t_entrypoints t_code_size) :=
        Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size r.(code) r.(arg_type) storage r.(storage_type) r.(views)
          r.(entrypoints) r.(code_size).
      Definition with_storage_type
        {t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size} storage_type
        (r :
          record t_code t_arg_type t_storage t_storage_type t_views
            t_entrypoints t_code_size) :=
        Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size r.(code) r.(arg_type) r.(storage) storage_type r.(views)
          r.(entrypoints) r.(code_size).
      Definition with_views
        {t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size} views
        (r :
          record t_code t_arg_type t_storage t_storage_type t_views
            t_entrypoints t_code_size) :=
        Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type) views
          r.(entrypoints) r.(code_size).
      Definition with_entrypoints
        {t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size} entrypoints
        (r :
          record t_code t_arg_type t_storage t_storage_type t_views
            t_entrypoints t_code_size) :=
        Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
          r.(views) entrypoints r.(code_size).
      Definition with_code_size
        {t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size} code_size
        (r :
          record t_code t_arg_type t_storage t_storage_type t_views
            t_entrypoints t_code_size) :=
        Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
          t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
          r.(views) r.(entrypoints) code_size.
    End Script.
    Definition Script_skeleton := Script.record.
  End script.
  Module kinstr.
    Module IIf_none.
      Record record {kinfo branch_if_none branch_if_some k : Set} : Set := Build {
        kinfo : kinfo;
        branch_if_none : branch_if_none;
        branch_if_some : branch_if_some;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_kinfo {t_kinfo t_branch_if_none t_branch_if_some t_k}
        kinfo (r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
        Build t_kinfo t_branch_if_none t_branch_if_some t_k kinfo
          r.(branch_if_none) r.(branch_if_some) r.(k).
      Definition with_branch_if_none
        {t_kinfo t_branch_if_none t_branch_if_some t_k} branch_if_none
        (r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
        Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
          branch_if_none r.(branch_if_some) r.(k).
      Definition with_branch_if_some
        {t_kinfo t_branch_if_none t_branch_if_some t_k} branch_if_some
        (r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
        Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
          r.(branch_if_none) branch_if_some r.(k).
      Definition with_k {t_kinfo t_branch_if_none t_branch_if_some t_k} k
        (r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
        Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
          r.(branch_if_none) r.(branch_if_some) k.
    End IIf_none.
    Definition IIf_none_skeleton := IIf_none.record.

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

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

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

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

    Module ICreate_contract.
      Record record {kinfo storage_type code k : Set} : Set := Build {
        kinfo : kinfo;
        storage_type : storage_type;
        code : code;
        k : k;
      }.
      Arguments record : clear implicits.
      Definition with_kinfo {t_kinfo t_storage_type t_code t_k} kinfo
        (r : record t_kinfo t_storage_type t_code t_k) :=
        Build t_kinfo t_storage_type t_code t_k kinfo r.(storage_type) r.(code)
          r.(k).
      Definition with_storage_type {t_kinfo t_storage_type t_code t_k}
        storage_type (r : record t_kinfo t_storage_type t_code t_k) :=
        Build t_kinfo t_storage_type t_code t_k r.(kinfo) storage_type r.(code)
          r.(k).
      Definition with_code {t_kinfo t_storage_type t_code t_k} code
        (r : record t_kinfo t_storage_type t_code t_k) :=
        Build t_kinfo t_storage_type t_code t_k r.(kinfo) r.(storage_type) code
          r.(k).
      Definition with_k {t_kinfo t_storage_type t_code t_k} k
        (r : record t_kinfo t_storage_type t_code t_k) :=
        Build t_kinfo t_storage_type t_code t_k r.(kinfo) r.(storage_type)
          r.(code) k.
    End ICreate_contract.
    Definition ICreate_contract_skeleton := ICreate_contract.record.
  End kinstr.
  Module typed_contract.
    Module Typed_contract.
      Record record {arg_ty address : Set} : Set := Build {
        arg_ty : arg_ty;
        address : address;
      }.
      Arguments record : clear implicits.
      Definition with_arg_ty {t_arg_ty t_address} arg_ty
        (r : record t_arg_ty t_address) :=
        Build t_arg_ty t_address arg_ty r.(address).
      Definition with_address {t_arg_ty t_address} address
        (r : record t_arg_ty t_address) :=
        Build t_arg_ty t_address r.(arg_ty) address.
    End Typed_contract.
    Definition Typed_contract_skeleton := Typed_contract.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 manager_operation.
    Module Transaction.
      Record record {transaction location parameters_ty parameters : Set} : Set := Build {
        transaction : transaction;
        location : location;
        parameters_ty : parameters_ty;
        parameters : parameters;
      }.
      Arguments record : clear implicits.
      Definition with_transaction
        {t_transaction t_location t_parameters_ty t_parameters} transaction
        (r : record t_transaction t_location t_parameters_ty t_parameters) :=
        Build t_transaction t_location t_parameters_ty t_parameters transaction
          r.(location) r.(parameters_ty) r.(parameters).
      Definition with_location
        {t_transaction t_location t_parameters_ty t_parameters} location
        (r : record t_transaction t_location t_parameters_ty t_parameters) :=
        Build t_transaction t_location t_parameters_ty t_parameters
          r.(transaction) location r.(parameters_ty) r.(parameters).
      Definition with_parameters_ty
        {t_transaction t_location t_parameters_ty t_parameters} parameters_ty
        (r : record t_transaction t_location t_parameters_ty t_parameters) :=
        Build t_transaction t_location t_parameters_ty t_parameters
          r.(transaction) r.(location) parameters_ty r.(parameters).
      Definition with_parameters
        {t_transaction t_location t_parameters_ty t_parameters} parameters
        (r : record t_transaction t_location t_parameters_ty t_parameters) :=
        Build t_transaction t_location t_parameters_ty t_parameters
          r.(transaction) r.(location) r.(parameters_ty) parameters.
    End Transaction.
    Definition Transaction_skeleton := Transaction.record.

    Module Origination.
      Record record {origination preorigination storage_type storage : Set} :
        Set := Build {
        origination : origination;
        preorigination : preorigination;
        storage_type : storage_type;
        storage : storage;
      }.
      Arguments record : clear implicits.
      Definition with_origination
        {t_origination t_preorigination t_storage_type t_storage} origination
        (r : record t_origination t_preorigination t_storage_type t_storage) :=
        Build t_origination t_preorigination t_storage_type t_storage
          origination r.(preorigination) r.(storage_type) r.(storage).
      Definition with_preorigination
        {t_origination t_preorigination t_storage_type t_storage} preorigination
        (r : record t_origination t_preorigination t_storage_type t_storage) :=
        Build t_origination t_preorigination t_storage_type t_storage
          r.(origination) preorigination r.(storage_type) r.(storage).
      Definition with_storage_type
        {t_origination t_preorigination t_storage_type t_storage} storage_type
        (r : record t_origination t_preorigination t_storage_type t_storage) :=
        Build t_origination t_preorigination t_storage_type t_storage
          r.(origination) r.(preorigination) storage_type r.(storage).
      Definition with_storage
        {t_origination t_preorigination t_storage_type t_storage} storage
        (r : record t_origination t_preorigination t_storage_type t_storage) :=
        Build t_origination t_preorigination t_storage_type t_storage
          r.(origination) r.(preorigination) r.(storage_type) storage.
    End Origination.
    Definition Origination_skeleton := Origination.record.
  End manager_operation.
End
  ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
Import
  ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.

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 kinfo.
  Record record {iloc kstack_ty : Set} : Set := Build {
    iloc : iloc;
    kstack_ty : kstack_ty;
  }.
  Arguments record : clear implicits.
  Definition with_iloc {t_iloc t_kstack_ty} iloc
    (r : record t_iloc t_kstack_ty) :=
    Build t_iloc t_kstack_ty iloc r.(kstack_ty).
  Definition with_kstack_ty {t_iloc t_kstack_ty} kstack_ty
    (r : record t_iloc t_kstack_ty) :=
    Build t_iloc t_kstack_ty r.(iloc) kstack_ty.
End kinfo.
Definition kinfo_skeleton := kinfo.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.

Reserved Notation "'script.Script".
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 "'typed_contract.Typed_contract".
Reserved Notation "'big_map.Big_map".
Reserved Notation "'view_signature.View_signature".
Reserved Notation "'manager_operation.Transaction".
Reserved Notation "'manager_operation.Origination".
Reserved Notation "'logging_function".
Reserved Notation "'execution_trace".
Reserved Notation "'logger".
Reserved Notation "'comparable_ty".
Reserved Notation "'kdescr".
Reserved Notation "'kinfo".
Reserved Notation "'internal_operation".
Reserved Notation "'operation".

Inductive script : Set :=
| Script : โˆ€ {storage : Set}, 'script.Script storage โ†’ script

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

with logging_event : Set :=
| LogEntry : logging_event
| LogExit : 'kinfo โ†’ logging_event

with lambda : Set :=
| Lam : 'kdescr โ†’ Alpha_context.Script.node โ†’ lambda

with typed_contract : Set :=
| Typed_contract : 'typed_contract.Typed_contract โ†’ typed_contract

with continuation : Set :=
| KNil : continuation
| KCons : kinstr โ†’ continuation โ†’ continuation
| KReturn : โˆ€ {s : Set}, s โ†’ continuation โ†’ continuation
| KMap_head : โˆ€ {a b : Set}, (a โ†’ b) โ†’ continuation โ†’ continuation
| KUndip : โˆ€ {b : Set}, b โ†’ continuation โ†’ continuation
| KLoop_in : kinstr โ†’ continuation โ†’ continuation
| KLoop_in_left : kinstr โ†’ continuation โ†’ continuation
| KIter : โˆ€ {a : Set}, kinstr โ†’ list a โ†’ continuation โ†’ continuation
| KList_enter_body : โˆ€ {a b : Set},
  kinstr โ†’ list a โ†’ list b โ†’ int โ†’ continuation โ†’ continuation
| KList_exit_body : โˆ€ {a b : Set},
  kinstr โ†’ list a โ†’ list b โ†’ int โ†’ continuation โ†’ continuation
| KMap_enter_body : โˆ€ {a b c : Set},
  kinstr โ†’ list (a ร— b) โ†’ map a c โ†’ continuation โ†’ continuation
| KMap_exit_body : โˆ€ {a b c : Set},
  kinstr โ†’ list (a ร— b) โ†’ map a c โ†’ a โ†’ continuation โ†’ continuation
| KView_exit : step_constants โ†’ continuation โ†’ continuation
| KLog : continuation โ†’ '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 :
  'kinfo โ†’ 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 manager_operation : Set :=
| Transaction : โˆ€ {a : Set},
  'manager_operation.Transaction a โ†’ manager_operation
| Origination : โˆ€ {storage : Set},
  'manager_operation.Origination storage โ†’ manager_operation
| Delegation : option Signature.public_key_hash โ†’ manager_operation

with packed_internal_operation : Set :=
| Internal_operation : 'internal_operation โ†’ packed_internal_operation

where "'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 "'kinfo" := (kinfo_skeleton Alpha_context.Script.location stack_ty)
and "'internal_operation" :=
  (internal_operation_skeleton Alpha_context.Contract.contract manager_operation
    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 "'script.Script" :=
  (fun (t_storage : Set) โ‡’ script.Script_skeleton lambda ty t_storage ty
    view_map entrypoints Cache_memory_helpers.sint)
and "'kinstr.IIf_none" := (kinstr.IIf_none_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IOpt_map" := (kinstr.IOpt_map_skeleton 'kinfo kinstr kinstr)
and "'kinstr.IIf_left" := (kinstr.IIf_left_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IIf_cons" := (kinstr.IIf_cons_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IIf" := (kinstr.IIf_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.ICreate_contract" :=
  (kinstr.ICreate_contract_skeleton 'kinfo ty Alpha_context.Script.expr kinstr)
and "'typed_contract.Typed_contract" :=
  (typed_contract.Typed_contract_skeleton ty address)
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 Alpha_context.Script_string.t ty ty)
and "'manager_operation.Transaction" :=
  (fun (t_a : Set) โ‡’ manager_operation.Transaction_skeleton
    Alpha_context.transaction Alpha_context.Script.location ty t_a)
and "'manager_operation.Origination" :=
  (fun (t_storage : Set) โ‡’ manager_operation.Origination_skeleton
    Alpha_context.origination Alpha_context.Contract.t ty t_storage).

Module script.
  Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.script.
  Definition Script := 'script.Script.
End script.
Module kinstr.
  Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.kinstr.
  Definition IIf_none := 'kinstr.IIf_none.
  Definition IOpt_map := 'kinstr.IOpt_map.
  Definition IIf_left := 'kinstr.IIf_left.
  Definition IIf_cons := 'kinstr.IIf_cons.
  Definition IIf := 'kinstr.IIf.
  Definition ICreate_contract := 'kinstr.ICreate_contract.
End kinstr.
Module typed_contract.
  Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.typed_contract.
  Definition Typed_contract := 'typed_contract.Typed_contract.
End typed_contract.
Module big_map.
  Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.big_map.
  Definition Big_map := 'big_map.Big_map.
End big_map.
Module view_signature.
  Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.view_signature.
  Definition View_signature := 'view_signature.View_signature.
End view_signature.
Module manager_operation.
  Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.manager_operation.
  Definition Transaction := 'manager_operation.Transaction.
  Definition Origination := 'manager_operation.Origination.
End manager_operation.

Definition logging_function := 'logging_function.
Definition execution_trace := 'execution_trace.
Definition logger := 'logger.
Definition comparable_ty := 'comparable_ty.
Definition kdescr := 'kdescr.
Definition kinfo := 'kinfo.
Definition internal_operation := 'internal_operation.
Definition operation := 'operation.

Inductive packed_manager_operation : Set :=
| Manager : manager_operation โ†’ packed_manager_operation.

Definition manager_kind (function_parameter : manager_operation)
  : Alpha_context.Kind.manager :=
  match function_parameter with
  | Transaction _ โ‡’ Alpha_context.Kind.Transaction_manager_kind
  | Origination _ โ‡’ Alpha_context.Kind.Origination_manager_kind
  | Delegation _ โ‡’ Alpha_context.Kind.Delegation_manager_kind
  end.

Definition kinfo_of_kinstr (i_value : kinstr) : kinfo :=
  match i_value with
  | IDrop kinfo_value _ โ‡’ kinfo_value
  | IDup kinfo_value _ โ‡’ kinfo_value
  | ISwap kinfo_value _ โ‡’ kinfo_value
  | IConst kinfo_value _ _ โ‡’ kinfo_value
  | ICons_pair kinfo_value _ โ‡’ kinfo_value
  | ICar kinfo_value _ โ‡’ kinfo_value
  | ICdr kinfo_value _ โ‡’ kinfo_value
  | IUnpair kinfo_value _ โ‡’ kinfo_value
  | ICons_some kinfo_value _ โ‡’ kinfo_value
  | ICons_none kinfo_value _ โ‡’ kinfo_value
  | IIf_none {| kinstr.IIf_none.kinfo := kinfo_value |} โ‡’ kinfo_value
  | IOpt_map {| kinstr.IOpt_map.kinfo := kinfo_value |} โ‡’ kinfo_value
  | ICons_left kinfo_value _ โ‡’ kinfo_value
  | ICons_right kinfo_value _ โ‡’ kinfo_value
  | IIf_left {| kinstr.IIf_left.kinfo := kinfo_value |} โ‡’ kinfo_value
  | ICons_list kinfo_value _ โ‡’ kinfo_value
  | INil kinfo_value _ โ‡’ kinfo_value
  | IIf_cons {| kinstr.IIf_cons.kinfo := kinfo_value |} โ‡’ kinfo_value
  | IList_map kinfo_value _ _ โ‡’ kinfo_value
  | IList_iter kinfo_value _ _ โ‡’ kinfo_value
  | IList_size kinfo_value _ โ‡’ kinfo_value
  | IEmpty_set kinfo_value _ _ โ‡’ kinfo_value
  | ISet_iter kinfo_value _ _ โ‡’ kinfo_value
  | ISet_mem kinfo_value _ โ‡’ kinfo_value
  | ISet_update kinfo_value _ โ‡’ kinfo_value
  | ISet_size kinfo_value _ โ‡’ kinfo_value
  | IEmpty_map kinfo_value _ _ โ‡’ kinfo_value
  | IMap_map kinfo_value _ _ โ‡’ kinfo_value
  | IMap_iter kinfo_value _ _ โ‡’ kinfo_value
  | IMap_mem kinfo_value _ โ‡’ kinfo_value
  | IMap_get kinfo_value _ โ‡’ kinfo_value
  | IMap_update kinfo_value _ โ‡’ kinfo_value
  | IMap_get_and_update kinfo_value _ โ‡’ kinfo_value
  | IMap_size kinfo_value _ โ‡’ kinfo_value
  | IEmpty_big_map kinfo_value _ _ _ โ‡’ kinfo_value
  | IBig_map_mem kinfo_value _ โ‡’ kinfo_value
  | IBig_map_get kinfo_value _ โ‡’ kinfo_value
  | IBig_map_update kinfo_value _ โ‡’ kinfo_value
  | IBig_map_get_and_update kinfo_value _ โ‡’ kinfo_value
  | IConcat_string kinfo_value _ โ‡’ kinfo_value
  | IConcat_string_pair kinfo_value _ โ‡’ kinfo_value
  | ISlice_string kinfo_value _ โ‡’ kinfo_value
  | IString_size kinfo_value _ โ‡’ kinfo_value
  | IConcat_bytes kinfo_value _ โ‡’ kinfo_value
  | IConcat_bytes_pair kinfo_value _ โ‡’ kinfo_value
  | ISlice_bytes kinfo_value _ โ‡’ kinfo_value
  | IBytes_size kinfo_value _ โ‡’ kinfo_value
  | IAdd_seconds_to_timestamp kinfo_value _ โ‡’ kinfo_value
  | IAdd_timestamp_to_seconds kinfo_value _ โ‡’ kinfo_value
  | ISub_timestamp_seconds kinfo_value _ โ‡’ kinfo_value
  | IDiff_timestamps kinfo_value _ โ‡’ kinfo_value
  | IAdd_tez kinfo_value _ โ‡’ kinfo_value
  | ISub_tez kinfo_value _ โ‡’ kinfo_value
  | ISub_tez_legacy kinfo_value _ โ‡’ kinfo_value
  | IMul_teznat kinfo_value _ โ‡’ kinfo_value
  | IMul_nattez kinfo_value _ โ‡’ kinfo_value
  | IEdiv_teznat kinfo_value _ โ‡’ kinfo_value
  | IEdiv_tez kinfo_value _ โ‡’ kinfo_value
  | IOr kinfo_value _ โ‡’ kinfo_value
  | IAnd kinfo_value _ โ‡’ kinfo_value
  | IXor kinfo_value _ โ‡’ kinfo_value
  | INot kinfo_value _ โ‡’ kinfo_value
  | IIs_nat kinfo_value _ โ‡’ kinfo_value
  | INeg kinfo_value _ โ‡’ kinfo_value
  | IAbs_int kinfo_value _ โ‡’ kinfo_value
  | IInt_nat kinfo_value _ โ‡’ kinfo_value
  | IAdd_int kinfo_value _ โ‡’ kinfo_value
  | IAdd_nat kinfo_value _ โ‡’ kinfo_value
  | ISub_int kinfo_value _ โ‡’ kinfo_value
  | IMul_int kinfo_value _ โ‡’ kinfo_value
  | IMul_nat kinfo_value _ โ‡’ kinfo_value
  | IEdiv_int kinfo_value _ โ‡’ kinfo_value
  | IEdiv_nat kinfo_value _ โ‡’ kinfo_value
  | ILsl_nat kinfo_value _ โ‡’ kinfo_value
  | ILsr_nat kinfo_value _ โ‡’ kinfo_value
  | IOr_nat kinfo_value _ โ‡’ kinfo_value
  | IAnd_nat kinfo_value _ โ‡’ kinfo_value
  | IAnd_int_nat kinfo_value _ โ‡’ kinfo_value
  | IXor_nat kinfo_value _ โ‡’ kinfo_value
  | INot_int kinfo_value _ โ‡’ kinfo_value
  | IIf {| kinstr.IIf.kinfo := kinfo_value |} โ‡’ kinfo_value
  | ILoop kinfo_value _ _ โ‡’ kinfo_value
  | ILoop_left kinfo_value _ _ โ‡’ kinfo_value
  | IDip kinfo_value _ _ โ‡’ kinfo_value
  | IExec kinfo_value _ โ‡’ kinfo_value
  | IApply kinfo_value _ _ โ‡’ kinfo_value
  | ILambda kinfo_value _ _ โ‡’ kinfo_value
  | IFailwith kinfo_value _ _ โ‡’ kinfo_value
  | ICompare kinfo_value _ _ โ‡’ kinfo_value
  | IEq kinfo_value _ โ‡’ kinfo_value
  | INeq kinfo_value _ โ‡’ kinfo_value
  | ILt kinfo_value _ โ‡’ kinfo_value
  | IGt kinfo_value _ โ‡’ kinfo_value
  | ILe kinfo_value _ โ‡’ kinfo_value
  | IGe kinfo_value _ โ‡’ kinfo_value
  | IAddress kinfo_value _ โ‡’ kinfo_value
  | IContract kinfo_value _ _ _ โ‡’ kinfo_value
  | ITransfer_tokens kinfo_value _ โ‡’ kinfo_value
  | IView kinfo_value _ _ โ‡’ kinfo_value
  | IImplicit_account kinfo_value _ โ‡’ kinfo_value
  | ICreate_contract {| kinstr.ICreate_contract.kinfo := kinfo_value |} โ‡’
    kinfo_value
  | ISet_delegate kinfo_value _ โ‡’ kinfo_value
  | INow kinfo_value _ โ‡’ kinfo_value
  | IMin_block_time kinfo_value _ โ‡’ kinfo_value
  | IBalance kinfo_value _ โ‡’ kinfo_value
  | ILevel kinfo_value _ โ‡’ kinfo_value
  | ICheck_signature kinfo_value _ โ‡’ kinfo_value
  | IHash_key kinfo_value _ โ‡’ kinfo_value
  | IPack kinfo_value _ _ โ‡’ kinfo_value
  | IUnpack kinfo_value _ _ โ‡’ kinfo_value
  | IBlake2b kinfo_value _ โ‡’ kinfo_value
  | ISha256 kinfo_value _ โ‡’ kinfo_value
  | ISha512 kinfo_value _ โ‡’ kinfo_value
  | ISource kinfo_value _ โ‡’ kinfo_value
  | ISender kinfo_value _ โ‡’ kinfo_value
  | ISelf kinfo_value _ _ _ โ‡’ kinfo_value
  | ISelf_address kinfo_value _ โ‡’ kinfo_value
  | IAmount kinfo_value _ โ‡’ kinfo_value
  | ISapling_empty_state kinfo_value _ _ โ‡’ kinfo_value
  | ISapling_verify_update kinfo_value _ โ‡’ kinfo_value
  | ISapling_verify_update_deprecated kinfo_value _ โ‡’ kinfo_value
  | IDig kinfo_value _ _ _ โ‡’ kinfo_value
  | IDug kinfo_value _ _ _ โ‡’ kinfo_value
  | IDipn kinfo_value _ _ _ _ โ‡’ kinfo_value
  | IDropn kinfo_value _ _ _ โ‡’ kinfo_value
  | IChainId kinfo_value _ โ‡’ kinfo_value
  | INever kinfo_value โ‡’ kinfo_value
  | IVoting_power kinfo_value _ โ‡’ kinfo_value
  | ITotal_voting_power kinfo_value _ โ‡’ kinfo_value
  | IKeccak kinfo_value _ โ‡’ kinfo_value
  | ISha3 kinfo_value _ โ‡’ kinfo_value
  | IAdd_bls12_381_g1 kinfo_value _ โ‡’ kinfo_value
  | IAdd_bls12_381_g2 kinfo_value _ โ‡’ kinfo_value
  | IAdd_bls12_381_fr kinfo_value _ โ‡’ kinfo_value
  | IMul_bls12_381_g1 kinfo_value _ โ‡’ kinfo_value
  | IMul_bls12_381_g2 kinfo_value _ โ‡’ kinfo_value
  | IMul_bls12_381_fr kinfo_value _ โ‡’ kinfo_value
  | IMul_bls12_381_z_fr kinfo_value _ โ‡’ kinfo_value
  | IMul_bls12_381_fr_z kinfo_value _ โ‡’ kinfo_value
  | IInt_bls12_381_fr kinfo_value _ โ‡’ kinfo_value
  | INeg_bls12_381_g1 kinfo_value _ โ‡’ kinfo_value
  | INeg_bls12_381_g2 kinfo_value _ โ‡’ kinfo_value
  | INeg_bls12_381_fr kinfo_value _ โ‡’ kinfo_value
  | IPairing_check_bls12_381 kinfo_value _ โ‡’ kinfo_value
  | IComb kinfo_value _ _ _ โ‡’ kinfo_value
  | IUncomb kinfo_value _ _ _ โ‡’ kinfo_value
  | IComb_get kinfo_value _ _ _ โ‡’ kinfo_value
  | IComb_set kinfo_value _ _ _ โ‡’ kinfo_value
  | IDup_n kinfo_value _ _ _ โ‡’ kinfo_value
  | ITicket kinfo_value _ โ‡’ kinfo_value
  | IRead_ticket kinfo_value _ โ‡’ kinfo_value
  | ISplit_ticket kinfo_value _ โ‡’ kinfo_value
  | IJoin_tickets kinfo_value _ _ โ‡’ kinfo_value
  | IHalt kinfo_value โ‡’ kinfo_value
  | ILog kinfo_value _ _ _ โ‡’ kinfo_value
  | IOpen_chest kinfo_value _ โ‡’ kinfo_value
  end.

Module kinstr_rewritek.
  Record record : Set := Build {
    apply : kinstr โ†’ kinstr;
  }.
  Definition with_apply apply (r : record) :=
    Build apply.
End kinstr_rewritek.
Definition kinstr_rewritek := kinstr_rewritek.record.

Definition kinstr_rewritek_value (i_value : kinstr) (f_value : kinstr_rewritek)
  : kinstr :=
  match i_value with
  | IDrop kinfo_value k_value โ‡’
    IDrop kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IDup kinfo_value k_value โ‡’
    IDup kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISwap kinfo_value k_value โ‡’
    ISwap kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IConst kinfo_value x_value k_value โ‡’
    IConst kinfo_value x_value (f_value.(kinstr_rewritek.apply) k_value)
  | ICons_pair kinfo_value k_value โ‡’
    ICons_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ICar kinfo_value k_value โ‡’
    ICar kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ICdr kinfo_value k_value โ‡’
    ICdr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IUnpair kinfo_value k_value โ‡’
    IUnpair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ICons_some kinfo_value k_value โ‡’
    ICons_some kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ICons_none kinfo_value k_value โ‡’
    ICons_none kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  |
    IIf_none {|
      kinstr.IIf_none.kinfo := kinfo_value;
        kinstr.IIf_none.branch_if_none := branch_if_none;
        kinstr.IIf_none.branch_if_some := branch_if_some;
        kinstr.IIf_none.k := k_value
        |} โ‡’
    IIf_none
      {| kinstr.IIf_none.kinfo := kinfo_value;
        kinstr.IIf_none.branch_if_none :=
          f_value.(kinstr_rewritek.apply) branch_if_none;
        kinstr.IIf_none.branch_if_some :=
          f_value.(kinstr_rewritek.apply) branch_if_some;
        kinstr.IIf_none.k := f_value.(kinstr_rewritek.apply) k_value; |}
  |
    IOpt_map {|
      kinstr.IOpt_map.kinfo := kinfo_value;
        kinstr.IOpt_map.body := body;
        kinstr.IOpt_map.k := k_value
        |} โ‡’
    let body := f_value.(kinstr_rewritek.apply) body in
    let k_value := f_value.(kinstr_rewritek.apply) k_value in
    IOpt_map
      {| kinstr.IOpt_map.kinfo := kinfo_value; kinstr.IOpt_map.body := body;
        kinstr.IOpt_map.k := k_value; |}
  | ICons_left kinfo_value k_value โ‡’
    ICons_left kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ICons_right kinfo_value k_value โ‡’
    ICons_right kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  |
    IIf_left {|
      kinstr.IIf_left.kinfo := kinfo_value;
        kinstr.IIf_left.branch_if_left := branch_if_left;
        kinstr.IIf_left.branch_if_right := branch_if_right;
        kinstr.IIf_left.k := k_value
        |} โ‡’
    IIf_left
      {| kinstr.IIf_left.kinfo := kinfo_value;
        kinstr.IIf_left.branch_if_left :=
          f_value.(kinstr_rewritek.apply) branch_if_left;
        kinstr.IIf_left.branch_if_right :=
          f_value.(kinstr_rewritek.apply) branch_if_right;
        kinstr.IIf_left.k := f_value.(kinstr_rewritek.apply) k_value; |}
  | ICons_list kinfo_value k_value โ‡’
    ICons_list kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INil kinfo_value k_value โ‡’
    INil kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  |
    IIf_cons {|
      kinstr.IIf_cons.kinfo := kinfo_value;
        kinstr.IIf_cons.branch_if_cons := branch_if_cons;
        kinstr.IIf_cons.branch_if_nil := branch_if_nil;
        kinstr.IIf_cons.k := k_value
        |} โ‡’
    IIf_cons
      {| kinstr.IIf_cons.kinfo := kinfo_value;
        kinstr.IIf_cons.branch_if_cons :=
          f_value.(kinstr_rewritek.apply) branch_if_cons;
        kinstr.IIf_cons.branch_if_nil :=
          f_value.(kinstr_rewritek.apply) branch_if_nil;
        kinstr.IIf_cons.k := f_value.(kinstr_rewritek.apply) k_value; |}
  | IList_map kinfo_value body k_value โ‡’
    IList_map kinfo_value (f_value.(kinstr_rewritek.apply) body)
      (f_value.(kinstr_rewritek.apply) k_value)
  | IList_iter kinfo_value body k_value โ‡’
    IList_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
      (f_value.(kinstr_rewritek.apply) k_value)
  | IList_size kinfo_value k_value โ‡’
    IList_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IEmpty_set kinfo_value ty k_value โ‡’
    IEmpty_set kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
  | ISet_iter kinfo_value body k_value โ‡’
    ISet_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
      (f_value.(kinstr_rewritek.apply) k_value)
  | ISet_mem kinfo_value k_value โ‡’
    ISet_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISet_update kinfo_value k_value โ‡’
    ISet_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISet_size kinfo_value k_value โ‡’
    ISet_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IEmpty_map kinfo_value cty k_value โ‡’
    IEmpty_map kinfo_value cty (f_value.(kinstr_rewritek.apply) k_value)
  | IMap_map kinfo_value body k_value โ‡’
    IMap_map kinfo_value (f_value.(kinstr_rewritek.apply) body)
      (f_value.(kinstr_rewritek.apply) k_value)
  | IMap_iter kinfo_value body k_value โ‡’
    IMap_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
      (f_value.(kinstr_rewritek.apply) k_value)
  | IMap_mem kinfo_value k_value โ‡’
    IMap_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMap_get kinfo_value k_value โ‡’
    IMap_get kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMap_update kinfo_value k_value โ‡’
    IMap_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMap_get_and_update kinfo_value k_value โ‡’
    IMap_get_and_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMap_size kinfo_value k_value โ‡’
    IMap_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IEmpty_big_map kinfo_value cty ty k_value โ‡’
    IEmpty_big_map kinfo_value cty ty (f_value.(kinstr_rewritek.apply) k_value)
  | IBig_map_mem kinfo_value k_value โ‡’
    IBig_map_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IBig_map_get kinfo_value k_value โ‡’
    IBig_map_get kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IBig_map_update kinfo_value k_value โ‡’
    IBig_map_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IBig_map_get_and_update kinfo_value k_value โ‡’
    IBig_map_get_and_update kinfo_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | IConcat_string kinfo_value k_value โ‡’
    IConcat_string kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IConcat_string_pair kinfo_value k_value โ‡’
    IConcat_string_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISlice_string kinfo_value k_value โ‡’
    ISlice_string kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IString_size kinfo_value k_value โ‡’
    IString_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IConcat_bytes kinfo_value k_value โ‡’
    IConcat_bytes kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IConcat_bytes_pair kinfo_value k_value โ‡’
    IConcat_bytes_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISlice_bytes kinfo_value k_value โ‡’
    ISlice_bytes kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IBytes_size kinfo_value k_value โ‡’
    IBytes_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_seconds_to_timestamp kinfo_value k_value โ‡’
    IAdd_seconds_to_timestamp kinfo_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_timestamp_to_seconds kinfo_value k_value โ‡’
    IAdd_timestamp_to_seconds kinfo_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | ISub_timestamp_seconds kinfo_value k_value โ‡’
    ISub_timestamp_seconds kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IDiff_timestamps kinfo_value k_value โ‡’
    IDiff_timestamps kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_tez kinfo_value k_value โ‡’
    IAdd_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISub_tez kinfo_value k_value โ‡’
    ISub_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISub_tez_legacy kinfo_value k_value โ‡’
    ISub_tez_legacy kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_teznat kinfo_value k_value โ‡’
    IMul_teznat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_nattez kinfo_value k_value โ‡’
    IMul_nattez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IEdiv_teznat kinfo_value k_value โ‡’
    IEdiv_teznat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IEdiv_tez kinfo_value k_value โ‡’
    IEdiv_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IOr kinfo_value k_value โ‡’
    IOr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAnd kinfo_value k_value โ‡’
    IAnd kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IXor kinfo_value k_value โ‡’
    IXor kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INot kinfo_value k_value โ‡’
    INot kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IIs_nat kinfo_value k_value โ‡’
    IIs_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INeg kinfo_value k_value โ‡’
    INeg kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAbs_int kinfo_value k_value โ‡’
    IAbs_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IInt_nat kinfo_value k_value โ‡’
    IInt_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_int kinfo_value k_value โ‡’
    IAdd_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_nat kinfo_value k_value โ‡’
    IAdd_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISub_int kinfo_value k_value โ‡’
    ISub_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_int kinfo_value k_value โ‡’
    IMul_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_nat kinfo_value k_value โ‡’
    IMul_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IEdiv_int kinfo_value k_value โ‡’
    IEdiv_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IEdiv_nat kinfo_value k_value โ‡’
    IEdiv_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ILsl_nat kinfo_value k_value โ‡’
    ILsl_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ILsr_nat kinfo_value k_value โ‡’
    ILsr_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IOr_nat kinfo_value k_value โ‡’
    IOr_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAnd_nat kinfo_value k_value โ‡’
    IAnd_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAnd_int_nat kinfo_value k_value โ‡’
    IAnd_int_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IXor_nat kinfo_value k_value โ‡’
    IXor_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INot_int kinfo_value k_value โ‡’
    INot_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  |
    IIf {|
      kinstr.IIf.kinfo := kinfo_value;
        kinstr.IIf.branch_if_true := branch_if_true;
        kinstr.IIf.branch_if_false := branch_if_false;
        kinstr.IIf.k := k_value
        |} โ‡’
    IIf
      {| kinstr.IIf.kinfo := kinfo_value;
        kinstr.IIf.branch_if_true :=
          f_value.(kinstr_rewritek.apply) branch_if_true;
        kinstr.IIf.branch_if_false :=
          f_value.(kinstr_rewritek.apply) branch_if_false;
        kinstr.IIf.k := f_value.(kinstr_rewritek.apply) k_value; |}
  | ILoop kinfo_value kbody k_value โ‡’
    ILoop kinfo_value (f_value.(kinstr_rewritek.apply) kbody)
      (f_value.(kinstr_rewritek.apply) k_value)
  | ILoop_left kinfo_value kl kr โ‡’
    ILoop_left kinfo_value (f_value.(kinstr_rewritek.apply) kl)
      (f_value.(kinstr_rewritek.apply) kr)
  | IDip kinfo_value body k_value โ‡’
    IDip kinfo_value (f_value.(kinstr_rewritek.apply) body)
      (f_value.(kinstr_rewritek.apply) k_value)
  | IExec kinfo_value k_value โ‡’
    IExec kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IApply kinfo_value ty k_value โ‡’
    IApply kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
  | ILambda kinfo_value l_value k_value โ‡’
    ILambda kinfo_value l_value (f_value.(kinstr_rewritek.apply) k_value)
  | IFailwith kinfo_value i_value ty โ‡’ IFailwith kinfo_value i_value ty
  | ICompare kinfo_value ty k_value โ‡’
    ICompare kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
  | IEq kinfo_value k_value โ‡’
    IEq kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INeq kinfo_value k_value โ‡’
    INeq kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ILt kinfo_value k_value โ‡’
    ILt kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IGt kinfo_value k_value โ‡’
    IGt kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ILe kinfo_value k_value โ‡’
    ILe kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IGe kinfo_value k_value โ‡’
    IGe kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAddress kinfo_value k_value โ‡’
    IAddress kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IContract kinfo_value ty code k_value โ‡’
    IContract kinfo_value ty code (f_value.(kinstr_rewritek.apply) k_value)
  | ITransfer_tokens kinfo_value k_value โ‡’
    ITransfer_tokens kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IView kinfo_value view_signature k_value โ‡’
    IView kinfo_value view_signature (f_value.(kinstr_rewritek.apply) k_value)
  | IImplicit_account kinfo_value k_value โ‡’
    IImplicit_account kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  |
    ICreate_contract {|
      kinstr.ICreate_contract.kinfo := kinfo_value;
        kinstr.ICreate_contract.storage_type := storage_type;
        kinstr.ICreate_contract.code := code;
        kinstr.ICreate_contract.k := k_value
        |} โ‡’
    let k_value := f_value.(kinstr_rewritek.apply) k_value in
    ICreate_contract
      {| kinstr.ICreate_contract.kinfo := kinfo_value;
        kinstr.ICreate_contract.storage_type := storage_type;
        kinstr.ICreate_contract.code := code;
        kinstr.ICreate_contract.k := k_value; |}
  | ISet_delegate kinfo_value k_value โ‡’
    ISet_delegate kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INow kinfo_value k_value โ‡’
    INow kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMin_block_time kinfo_value k_value โ‡’
    IMin_block_time kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IBalance kinfo_value k_value โ‡’
    IBalance kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ILevel kinfo_value k_value โ‡’
    ILevel kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ICheck_signature kinfo_value k_value โ‡’
    ICheck_signature kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IHash_key kinfo_value k_value โ‡’
    IHash_key kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IPack kinfo_value ty k_value โ‡’
    IPack kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
  | IUnpack kinfo_value ty k_value โ‡’
    IUnpack kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
  | IBlake2b kinfo_value k_value โ‡’
    IBlake2b kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISha256 kinfo_value k_value โ‡’
    ISha256 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISha512 kinfo_value k_value โ‡’
    ISha512 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISource kinfo_value k_value โ‡’
    ISource kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISender kinfo_value k_value โ‡’
    ISender kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISelf kinfo_value ty s_value k_value โ‡’
    ISelf kinfo_value ty s_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISelf_address kinfo_value k_value โ‡’
    ISelf_address kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAmount kinfo_value k_value โ‡’
    IAmount kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISapling_empty_state kinfo_value s_value k_value โ‡’
    ISapling_empty_state kinfo_value s_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | ISapling_verify_update kinfo_value k_value โ‡’
    ISapling_verify_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISapling_verify_update_deprecated kinfo_value k_value โ‡’
    ISapling_verify_update_deprecated kinfo_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | IDig kinfo_value n_value p_value k_value โ‡’
    IDig kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
  | IDug kinfo_value n_value p_value k_value โ‡’
    IDug kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
  | IDipn kinfo_value n_value p_value k1 k2 โ‡’
    IDipn kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k1)
      (f_value.(kinstr_rewritek.apply) k2)
  | IDropn kinfo_value n_value p_value k_value โ‡’
    IDropn kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
  | IChainId kinfo_value k_value โ‡’
    IChainId kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INever kinfo_value โ‡’ INever kinfo_value
  | IVoting_power kinfo_value k_value โ‡’
    IVoting_power kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ITotal_voting_power kinfo_value k_value โ‡’
    ITotal_voting_power kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IKeccak kinfo_value k_value โ‡’
    IKeccak kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISha3 kinfo_value k_value โ‡’
    ISha3 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_bls12_381_g1 kinfo_value k_value โ‡’
    IAdd_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_bls12_381_g2 kinfo_value k_value โ‡’
    IAdd_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IAdd_bls12_381_fr kinfo_value k_value โ‡’
    IAdd_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_bls12_381_g1 kinfo_value k_value โ‡’
    IMul_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_bls12_381_g2 kinfo_value k_value โ‡’
    IMul_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_bls12_381_fr kinfo_value k_value โ‡’
    IMul_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_bls12_381_z_fr kinfo_value k_value โ‡’
    IMul_bls12_381_z_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IMul_bls12_381_fr_z kinfo_value k_value โ‡’
    IMul_bls12_381_fr_z kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IInt_bls12_381_fr kinfo_value k_value โ‡’
    IInt_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INeg_bls12_381_g1 kinfo_value k_value โ‡’
    INeg_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INeg_bls12_381_g2 kinfo_value k_value โ‡’
    INeg_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | INeg_bls12_381_fr kinfo_value k_value โ‡’
    INeg_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IPairing_check_bls12_381 kinfo_value k_value โ‡’
    IPairing_check_bls12_381 kinfo_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | IComb kinfo_value n_value p_value k_value โ‡’
    IComb kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
  | IUncomb kinfo_value n_value p_value k_value โ‡’
    IUncomb kinfo_value n_value p_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | IComb_get kinfo_value n_value p_value k_value โ‡’
    IComb_get kinfo_value n_value p_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | IComb_set kinfo_value n_value p_value k_value โ‡’
    IComb_set kinfo_value n_value p_value
      (f_value.(kinstr_rewritek.apply) k_value)
  | IDup_n kinfo_value n_value p_value k_value โ‡’
    IDup_n kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
  | ITicket kinfo_value k_value โ‡’
    ITicket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IRead_ticket kinfo_value k_value โ‡’
    IRead_ticket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | ISplit_ticket kinfo_value k_value โ‡’
    ISplit_ticket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  | IJoin_tickets kinfo_value ty k_value โ‡’
    IJoin_tickets kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
  | IHalt kinfo_value โ‡’ IHalt kinfo_value
  | ILog kinfo_value event logger k_value โ‡’
    ILog kinfo_value event logger k_value
  | IOpen_chest kinfo_value k_value โ‡’
    IOpen_chest kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
  end.

Definition meta_basic : ty_metadata :=
  {| ty_metadata.size := Type_size.(TYPE_SIZE.one); |}.

Definition ty_metadata_value (function_parameter : ty) : ty_metadata :=
  match function_parameter with
  |
    (Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
    Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
    | Tx_rollup_l2_address_t) โ‡’ meta_basic
  | Pair_t _ _ meta _ โ‡’ meta
  | Union_t _ _ meta _ โ‡’ meta
  | Option_t _ meta _ โ‡’ meta
  | Lambda_t _ _ meta โ‡’ meta
  | List_t _ meta โ‡’ meta
  | Set_t _ meta โ‡’ meta
  | Map_t _ _ meta โ‡’ meta
  | Big_map_t _ _ meta โ‡’ meta
  | Ticket_t _ meta โ‡’ meta
  | Contract_t _ meta โ‡’ meta
  |
    (Sapling_transaction_t _ | Sapling_transaction_deprecated_t _ |
    Sapling_state_t _ | Operation_t | Bls12_381_g1_t | Bls12_381_g2_t |
    Bls12_381_fr_t | Chest_t | Chest_key_t) โ‡’ meta_basic
  end.

Definition comparable_ty_metadata (function_parameter : comparable_ty)
  : ty_metadata :=
  match function_parameter with
  |
    (Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
    Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
    | Tx_rollup_l2_address_t) โ‡’ meta_basic
  | Pair_t _ _ meta Dependent_bool.YesYes โ‡’ meta
  | Union_t _ _ meta Dependent_bool.YesYes โ‡’ meta
  | Option_t _ meta Dependent_bool.Yes โ‡’ meta
  | _ โ‡’ unreachable_gadt_branch
  end.

Definition ty_size (t_value : ty) : Type_size.(TYPE_SIZE.t) :=
  (ty_metadata_value t_value).(ty_metadata.size).

Definition comparable_ty_size (t_value : comparable_ty)
  : Type_size.(TYPE_SIZE.t) :=
  (comparable_ty_metadata t_value).(ty_metadata.size).

Definition is_comparable (function_parameter : ty) : Dependent_bool.dbool :=
  match function_parameter with
  | Never_t โ‡’ Dependent_bool.Yes
  | Unit_t โ‡’ Dependent_bool.Yes
  | Int_t โ‡’ Dependent_bool.Yes
  | Nat_t โ‡’ Dependent_bool.Yes
  | Signature_t โ‡’ Dependent_bool.Yes
  | String_t โ‡’ Dependent_bool.Yes
  | Bytes_t โ‡’ Dependent_bool.Yes
  | Mutez_t โ‡’ Dependent_bool.Yes
  | Bool_t โ‡’ Dependent_bool.Yes
  | Key_hash_t โ‡’ Dependent_bool.Yes
  | Key_t โ‡’ Dependent_bool.Yes
  | Timestamp_t โ‡’ Dependent_bool.Yes
  | Chain_id_t โ‡’ Dependent_bool.Yes
  | Address_t โ‡’ Dependent_bool.Yes
  | Tx_rollup_l2_address_t โ‡’ Dependent_bool.Yes
  | Pair_t _ _ _ dand_value โ‡’ Dependent_bool.dbool_of_dand dand_value
  | Union_t _ _ _ dand_value โ‡’ Dependent_bool.dbool_of_dand dand_value
  | Option_t _ _ cmp โ‡’ cmp
  | Lambda_t _ _ _ โ‡’ Dependent_bool.No
  | List_t _ _ โ‡’ Dependent_bool.No
  | Set_t _ _ โ‡’ Dependent_bool.No
  | Map_t _ _ _ โ‡’ Dependent_bool.No
  | Big_map_t _ _ _ โ‡’ Dependent_bool.No
  | Ticket_t _ _ โ‡’ Dependent_bool.No
  | Contract_t _ _ โ‡’ Dependent_bool.No
  | Sapling_transaction_t _ โ‡’ Dependent_bool.No
  | Sapling_transaction_deprecated_t _ โ‡’ Dependent_bool.No
  | Sapling_state_t _ โ‡’ Dependent_bool.No
  | Operation_t โ‡’ Dependent_bool.No
  | Bls12_381_g1_t โ‡’ Dependent_bool.No
  | Bls12_381_g2_t โ‡’ Dependent_bool.No
  | Bls12_381_fr_t โ‡’ Dependent_bool.No
  | Chest_t โ‡’ Dependent_bool.No
  | Chest_key_t โ‡’ Dependent_bool.No
  end.

Inductive ty_ex_c : Set :=
| Ty_ex_c : ty โ†’ ty_ex_c.

Definition unit_t : ty := Unit_t.

Definition unit_key : ty := unit_t.

Definition int_t : ty := Int_t.

Definition int_key : ty := int_t.

Definition nat_t : ty := Nat_t.

Definition nat_key : ty := nat_t.

Definition signature_t : ty := Signature_t.

Definition signature_key : ty := signature_t.

Definition string_t : ty := String_t.

Definition string_key : ty := string_t.

Definition bytes_t : ty := Bytes_t.

Definition bytes_key : ty := bytes_t.

Definition mutez_t : ty := Mutez_t.

Definition mutez_key : ty := mutez_t.

Definition key_hash_t : ty := Key_hash_t.

Definition key_hash_key : ty := key_hash_t.

Definition key_t : ty := Key_t.

Definition key_key : ty := key_t.

Definition timestamp_t : ty := Timestamp_t.

Definition timestamp_key : ty := timestamp_t.

Definition address_t : ty := Address_t.

Definition address_key : ty := address_t.

Definition bool_t : ty := Bool_t.

Definition bool_key : ty := bool_t.

Definition tx_rollup_l2_address_t : ty := Tx_rollup_l2_address_t.

Definition tx_rollup_l2_address_key : ty := tx_rollup_l2_address_t.

Definition pair_t
  (loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
  : M? ty_ex_c :=
  let? size_value :=
    Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
      (ty_size r_value) in
  let 'Dependent_bool.Ex_dand cmp :=
    Dependent_bool.dand_value (is_comparable l_value) (is_comparable r_value) in
  return?
    (Ty_ex_c (Pair_t l_value r_value {| ty_metadata.size := size_value; |} cmp)).

Definition comparable_pair_t
  (loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
  : M? ty :=
  let? size_value :=
    Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
      (ty_size r_value) in
  return?
    (Pair_t l_value