🍬 Script_ir_translator.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Gas_monad.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_comparable.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_annot.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Script_set.
Require TezosOfOCaml.Proto_alpha.Script_tc_context.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.

Module Typecheck_costs := Michelson_v1_gas.Cost_of.Typechecking.

Module Unparse_costs := Michelson_v1_gas.Cost_of.Unparsing.

Module Tc_context := Script_tc_context.

Inductive ex_stack_ty : Set :=
| Ex_stack_ty : Script_typed_ir.stack_ty → ex_stack_ty.

Module cinstr.
  Record record : Set := Build {
    apply :
      Script_typed_ir.kinfo → Script_typed_ir.kinstr → Script_typed_ir.kinstr;
  }.
  Definition with_apply apply (r : record) :=
    Build apply.
End cinstr.
Definition cinstr := cinstr.record.

Module descr.
  Record record : Set := Build {
    loc : Alpha_context.Script.location;
    bef : Script_typed_ir.stack_ty;
    aft : Script_typed_ir.stack_ty;
    instr : cinstr;
  }.
  Definition with_loc loc (r : record) :=
    Build loc r.(bef) r.(aft) r.(instr).
  Definition with_bef bef (r : record) :=
    Build r.(loc) bef r.(aft) r.(instr).
  Definition with_aft aft (r : record) :=
    Build r.(loc) r.(bef) aft r.(instr).
  Definition with_instr instr (r : record) :=
    Build r.(loc) r.(bef) r.(aft) instr.
End descr.
Definition descr := descr.record.

Definition close_descr (function_parameter : descr) : Script_typed_ir.kdescr :=
  let '{|
    descr.loc := loc_value;
      descr.bef := bef;
      descr.aft := aft;
      descr.instr := instr
      |} := function_parameter in
  let kinfo_value :=
    {| Script_typed_ir.kinfo.iloc := loc_value;
      Script_typed_ir.kinfo.kstack_ty := aft; |} in
  let kinfo' :=
    {| Script_typed_ir.kinfo.iloc := loc_value;
      Script_typed_ir.kinfo.kstack_ty := bef; |} in
  let kinstr := instr.(cinstr.apply) kinfo' (Script_typed_ir.IHalt kinfo_value)
    in
  {| Script_typed_ir.kdescr.kloc := loc_value;
    Script_typed_ir.kdescr.kbef := bef; Script_typed_ir.kdescr.kaft := aft;
    Script_typed_ir.kdescr.kinstr := kinstr; |}.

Definition kinfo_of_descr (function_parameter : descr)
  : Script_typed_ir.kinfo :=
  let '{| descr.loc := loc_value; descr.bef := bef |} := function_parameter in
  {| Script_typed_ir.kinfo.iloc := loc_value;
    Script_typed_ir.kinfo.kstack_ty := bef; |}.

Definition compose_descr
  (loc_value : Alpha_context.Script.location) (d1 : descr) (d2 : descr)
  : descr :=
  {| descr.loc := loc_value; descr.bef := d1.(descr.bef);
    descr.aft := d2.(descr.aft);
    descr.instr :=
      {|
        cinstr.apply :=
          fun (function_parameter : Script_typed_ir.kinfo) ⇒
            let '_ := function_parameter in
            fun (k_value : Script_typed_ir.kinstr) ⇒
              d1.(descr.instr).(cinstr.apply) (kinfo_of_descr d1)
                (d2.(descr.instr).(cinstr.apply) (kinfo_of_descr d2) k_value);
        |}; |}.

Definition tc_context : Set := Tc_context.t.

Inductive unparsing_mode : Set :=
| Optimized : unparsing_mode
| Readable : unparsing_mode
| Optimized_legacy : unparsing_mode.

Definition type_logger : Set :=
  Alpha_context.Script.location → list Alpha_context.Script.expr →
  list Alpha_context.Script.expr → unit.

Definition location {A B : Set} (function_parameter : Micheline.node A B) : A :=
  match function_parameter with
  |
    (Micheline.Prim loc_value _ _ _ | Micheline.Int loc_value _ |
    Micheline.String loc_value _ | Micheline.Bytes loc_value _ |
    Micheline.Seq loc_value _) ⇒ loc_value
  end.

Definition kind_equal
  (a_value : Script_tc_errors.kind) (b_value : Script_tc_errors.kind) : bool :=
  match (a_value, b_value) with
  |
    ((Script_tc_errors.Int_kind, Script_tc_errors.Int_kind) |
    (Script_tc_errors.String_kind, Script_tc_errors.String_kind) |
    (Script_tc_errors.Bytes_kind, Script_tc_errors.Bytes_kind) |
    (Script_tc_errors.Prim_kind, Script_tc_errors.Prim_kind) |
    (Script_tc_errors.Seq_kind, Script_tc_errors.Seq_kind)) ⇒ true
  | _ ⇒ false
  end.

Definition kind_value {A B : Set} (function_parameter : Micheline.node A B)
  : Script_tc_errors.kind :=
  match function_parameter with
  | Micheline.Int _ _ ⇒ Script_tc_errors.Int_kind
  | Micheline.String _ _ ⇒ Script_tc_errors.String_kind
  | Micheline.Bytes _ _ ⇒ Script_tc_errors.Bytes_kind
  | Micheline.Prim _ _ _ _ ⇒ Script_tc_errors.Prim_kind
  | Micheline.Seq _ _ ⇒ Script_tc_errors.Seq_kind
  end.

Definition unexpected
  (expr :
    Micheline.node Alpha_context.Script.location Michelson_v1_primitives.prim)
  (exp_kinds : list Script_tc_errors.kind)
  (exp_ns : Michelson_v1_primitives.namespace)
  (exp_prims : list Alpha_context.Script.prim) : Error_monad._error :=
  match expr with
  | Micheline.Int loc_value _ ⇒
    Build_extensible "Invalid_kind"
      (Alpha_context.Script.location × list Script_tc_errors.kind ×
        Script_tc_errors.kind)
      (loc_value, (cons Script_tc_errors.Prim_kind exp_kinds),
        Script_tc_errors.Int_kind)
  | Micheline.String loc_value _ ⇒
    Build_extensible "Invalid_kind"
      (Alpha_context.Script.location × list Script_tc_errors.kind ×
        Script_tc_errors.kind)
      (loc_value, (cons Script_tc_errors.Prim_kind exp_kinds),
        Script_tc_errors.String_kind)
  | Micheline.Bytes loc_value _ ⇒
    Build_extensible "Invalid_kind"
      (Alpha_context.Script.location × list Script_tc_errors.kind ×
        Script_tc_errors.kind)
      (loc_value, (cons Script_tc_errors.Prim_kind exp_kinds),
        Script_tc_errors.Bytes_kind)
  | Micheline.Seq loc_value _ ⇒
    Build_extensible "Invalid_kind"
      (Alpha_context.Script.location × list Script_tc_errors.kind ×
        Script_tc_errors.kind)
      (loc_value, (cons Script_tc_errors.Prim_kind exp_kinds),
        Script_tc_errors.Seq_kind)
  | Micheline.Prim loc_value name _ _ ⇒
    match ((Michelson_v1_primitives.namespace_value name), exp_ns) with
    |
      ((Michelson_v1_primitives.Type_namespace,
        Michelson_v1_primitives.Type_namespace) |
      (Michelson_v1_primitives.Instr_namespace,
        Michelson_v1_primitives.Instr_namespace) |
      (Michelson_v1_primitives.Constant_namespace,
        Michelson_v1_primitives.Constant_namespace)) ⇒
      Build_extensible "Invalid_primitive"
        (Alpha_context.Script.location × list Alpha_context.Script.prim ×
          Michelson_v1_primitives.prim) (loc_value, exp_prims, name)
    | (ns, _) ⇒
      Build_extensible "Invalid_namespace"
        (Alpha_context.Script.location × Michelson_v1_primitives.prim ×
          Michelson_v1_primitives.namespace × Michelson_v1_primitives.namespace)
        (loc_value, name, exp_ns, ns)
    end
  end.

Definition check_kind {A : Set}
  (kinds : list Script_tc_errors.kind)
  (expr : Micheline.node Alpha_context.Script.location A) : M? unit :=
  let kind_value := kind_value expr in
  if List._exists (kind_equal kind_value) kinds then
    Result.return_unit
  else
    let loc_value := location expr in
    Error_monad.error_value
      (Build_extensible "Invalid_kind"
        (Alpha_context.Script.location × list Script_tc_errors.kind ×
          Script_tc_errors.kind) (loc_value, kinds, kind_value)).

Fixpoint ty_of_comparable_ty
  (function_parameter : Script_typed_ir.comparable_ty) : Script_typed_ir.ty :=
  match function_parameter with
  | Script_typed_ir.Unit_t ⇒ Script_typed_ir.Unit_t
  | Script_typed_ir.Never_t ⇒ Script_typed_ir.Never_t
  | Script_typed_ir.Int_t ⇒ Script_typed_ir.Int_t
  | Script_typed_ir.Nat_t ⇒ Script_typed_ir.Nat_t
  | Script_typed_ir.Signature_t ⇒ Script_typed_ir.Signature_t
  | Script_typed_ir.String_t ⇒ Script_typed_ir.String_t
  | Script_typed_ir.Bytes_t ⇒ Script_typed_ir.Bytes_t
  | Script_typed_ir.Mutez_t ⇒ Script_typed_ir.Mutez_t
  | Script_typed_ir.Bool_t ⇒ Script_typed_ir.Bool_t
  | Script_typed_ir.Key_hash_t ⇒ Script_typed_ir.Key_hash_t
  | Script_typed_ir.Key_t ⇒ Script_typed_ir.Key_t
  | Script_typed_ir.Timestamp_t ⇒ Script_typed_ir.Timestamp_t
  | Script_typed_ir.Address_t ⇒ Script_typed_ir.Address_t
  | Script_typed_ir.Tx_rollup_l2_address_t ⇒
    Script_typed_ir.Tx_rollup_l2_address_t
  | Script_typed_ir.Chain_id_t ⇒ Script_typed_ir.Chain_id_t
  | Script_typed_ir.Pair_t l_value r_value meta Dependent_bool.YesYes ⇒
    Script_typed_ir.Pair_t (ty_of_comparable_ty l_value)
      (ty_of_comparable_ty r_value) meta Dependent_bool.YesYes
  | Script_typed_ir.Union_t l_value r_value meta Dependent_bool.YesYes ⇒
    Script_typed_ir.Union_t (ty_of_comparable_ty l_value)
      (ty_of_comparable_ty r_value) meta Dependent_bool.YesYes
  | Script_typed_ir.Option_t t_value meta Dependent_bool.Yes ⇒
    Script_typed_ir.Option_t (ty_of_comparable_ty t_value) meta
      Dependent_bool.Yes
  | _ ⇒ unreachable_gadt_branch
  end.

Fixpoint unparse_comparable_ty_uncarbonated {loc : Set}
  (loc_value : loc) (function_parameter : Script_typed_ir.comparable_ty)
  : Alpha_context.Script.michelson_node loc :=
  match function_parameter with
  | Script_typed_ir.Unit_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_unit nil nil
  | Script_typed_ir.Never_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_never nil nil
  | Script_typed_ir.Int_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_int nil nil
  | Script_typed_ir.Nat_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_nat nil nil
  | Script_typed_ir.Signature_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_signature nil nil
  | Script_typed_ir.String_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_string nil nil
  | Script_typed_ir.Bytes_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_bytes nil nil
  | Script_typed_ir.Mutez_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_mutez nil nil
  | Script_typed_ir.Bool_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_bool nil nil
  | Script_typed_ir.Key_hash_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_key_hash nil nil
  | Script_typed_ir.Key_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_key nil nil
  | Script_typed_ir.Timestamp_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_timestamp nil nil
  | Script_typed_ir.Address_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_address nil nil
  | Script_typed_ir.Tx_rollup_l2_address_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_tx_rollup_l2_address nil
      nil
  | Script_typed_ir.Chain_id_t ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_chain_id nil nil
  | Script_typed_ir.Pair_t l_value r_value _meta Dependent_bool.YesYes ⇒
    let tl := unparse_comparable_ty_uncarbonated loc_value l_value in
    let tr := unparse_comparable_ty_uncarbonated loc_value r_value in
    match tr with
    | Micheline.Prim _ Michelson_v1_primitives.T_pair ts [] ⇒
      Micheline.Prim loc_value Michelson_v1_primitives.T_pair (cons tl ts) nil
    | _ ⇒
      Micheline.Prim loc_value Michelson_v1_primitives.T_pair [ tl; tr ] nil
    end
  | Script_typed_ir.Union_t l_value r_value _meta Dependent_bool.YesYes ⇒
    let tl := unparse_comparable_ty_uncarbonated loc_value l_value in
    let tr := unparse_comparable_ty_uncarbonated loc_value r_value in
    Micheline.Prim loc_value Michelson_v1_primitives.T_or [ tl; tr ] nil
  | Script_typed_ir.Option_t t_value _meta Dependent_bool.Yes ⇒
    Micheline.Prim loc_value Michelson_v1_primitives.T_option
      [ unparse_comparable_ty_uncarbonated loc_value t_value ] nil
  | _ ⇒ unreachable_gadt_branch
  end.

Definition unparse_memo_size {A B : Set}
  (loc_value : A) (memo_size : Alpha_context.Sapling.Memo_size.t)
  : Micheline.node A B :=
  let z_value := Alpha_context.Sapling.Memo_size.unparse_to_z memo_size in
  Micheline.Int loc_value z_value.

Fixpoint unparse_ty_entrypoints_uncarbonated {loc : Set}
  (loc_value : loc) (ty : Script_typed_ir.ty)
  (function_parameter : Script_typed_ir.entrypoints_node)
  : Alpha_context.Script.michelson_node loc :=
  let '{|
    Script_typed_ir.entrypoints_node.at_node := at_node;
      Script_typed_ir.entrypoints_node.nested := nested_entrypoints
      |} := function_parameter in
  let '(name, args) :=
    match ty with
    | Script_typed_ir.Unit_t ⇒ (Michelson_v1_primitives.T_unit, nil)
    | Script_typed_ir.Int_t ⇒ (Michelson_v1_primitives.T_int, nil)
    | Script_typed_ir.Nat_t ⇒ (Michelson_v1_primitives.T_nat, nil)
    | Script_typed_ir.Signature_t ⇒ (Michelson_v1_primitives.T_signature, nil)
    | Script_typed_ir.String_t ⇒ (Michelson_v1_primitives.T_string, nil)
    | Script_typed_ir.Bytes_t ⇒ (Michelson_v1_primitives.T_bytes, nil)
    | Script_typed_ir.Mutez_t ⇒ (Michelson_v1_primitives.T_mutez, nil)
    | Script_typed_ir.Bool_t ⇒ (Michelson_v1_primitives.T_bool, nil)
    | Script_typed_ir.Key_hash_t ⇒ (Michelson_v1_primitives.T_key_hash, nil)
    | Script_typed_ir.Key_t ⇒ (Michelson_v1_primitives.T_key, nil)
    | Script_typed_ir.Timestamp_t ⇒ (Michelson_v1_primitives.T_timestamp, nil)
    | Script_typed_ir.Address_t ⇒ (Michelson_v1_primitives.T_address, nil)
    | Script_typed_ir.Tx_rollup_l2_address_t ⇒
      (Michelson_v1_primitives.T_tx_rollup_l2_address, nil)
    | Script_typed_ir.Operation_t ⇒ (Michelson_v1_primitives.T_operation, nil)
    | Script_typed_ir.Chain_id_t ⇒ (Michelson_v1_primitives.T_chain_id, nil)
    | Script_typed_ir.Never_t ⇒ (Michelson_v1_primitives.T_never, nil)
    | Script_typed_ir.Bls12_381_g1_t ⇒
      (Michelson_v1_primitives.T_bls12_381_g1, nil)
    | Script_typed_ir.Bls12_381_g2_t ⇒
      (Michelson_v1_primitives.T_bls12_381_g2, nil)
    | Script_typed_ir.Bls12_381_fr_t ⇒
      (Michelson_v1_primitives.T_bls12_381_fr, nil)
    | Script_typed_ir.Contract_t ut _meta ⇒
      let t_value :=
        unparse_ty_entrypoints_uncarbonated loc_value ut
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_contract, [ t_value ])
    | Script_typed_ir.Pair_t utl utr _meta _ ⇒
      let tl :=
        unparse_ty_entrypoints_uncarbonated loc_value utl
          Script_typed_ir.no_entrypoints in
      let tr :=
        unparse_ty_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      match tr with
      | Micheline.Prim _ Michelson_v1_primitives.T_pair ts [] ⇒
        (Michelson_v1_primitives.T_pair, (cons tl ts))
      | _ ⇒ (Michelson_v1_primitives.T_pair, [ tl; tr ])
      end
    | Script_typed_ir.Union_t utl utr _meta _ ⇒
      let '(entrypoints_l, entrypoints_r) :=
        match nested_entrypoints with
        | Script_typed_ir.Entrypoints_None ⇒
          (Script_typed_ir.no_entrypoints, Script_typed_ir.no_entrypoints)
        |
          Script_typed_ir.Entrypoints_Union {|
            Script_typed_ir.nested_entrypoints.Entrypoints_Union._left := _left;
              Script_typed_ir.nested_entrypoints.Entrypoints_Union._right :=
                _right
              |} ⇒ (_left, _right)
        end in
      let tl := unparse_ty_entrypoints_uncarbonated loc_value utl entrypoints_l
        in
      let tr := unparse_ty_entrypoints_uncarbonated loc_value utr entrypoints_r
        in
      (Michelson_v1_primitives.T_or, [ tl; tr ])
    | Script_typed_ir.Lambda_t uta utr _meta ⇒
      let ta :=
        unparse_ty_entrypoints_uncarbonated loc_value uta
          Script_typed_ir.no_entrypoints in
      let tr :=
        unparse_ty_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_lambda, [ ta; tr ])
    | Script_typed_ir.Option_t ut _meta _ ⇒
      let ut :=
        unparse_ty_entrypoints_uncarbonated loc_value ut
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_option, [ ut ])
    | Script_typed_ir.List_t ut _meta ⇒
      let t_value :=
        unparse_ty_entrypoints_uncarbonated loc_value ut
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_list, [ t_value ])
    | Script_typed_ir.Ticket_t ut _meta ⇒
      let t_value := unparse_comparable_ty_uncarbonated loc_value ut in
      (Michelson_v1_primitives.T_ticket, [ t_value ])
    | Script_typed_ir.Set_t ut _meta ⇒
      let t_value := unparse_comparable_ty_uncarbonated loc_value ut in
      (Michelson_v1_primitives.T_set, [ t_value ])
    | Script_typed_ir.Map_t uta utr _meta ⇒
      let ta := unparse_comparable_ty_uncarbonated loc_value uta in
      let tr :=
        unparse_ty_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_map, [ ta; tr ])
    | Script_typed_ir.Big_map_t uta utr _meta ⇒
      let ta := unparse_comparable_ty_uncarbonated loc_value uta in
      let tr :=
        unparse_ty_entrypoints_uncarbonated loc_value utr
          Script_typed_ir.no_entrypoints in
      (Michelson_v1_primitives.T_big_map, [ ta; tr ])
    | Script_typed_ir.Sapling_transaction_t memo_size ⇒
      (Michelson_v1_primitives.T_sapling_transaction,
        [ unparse_memo_size loc_value memo_size ])
    | Script_typed_ir.Sapling_transaction_deprecated_t memo_size ⇒
      (Michelson_v1_primitives.T_sapling_transaction_deprecated,
        [ unparse_memo_size loc_value memo_size ])
    | Script_typed_ir.Sapling_state_t memo_size ⇒
      (Michelson_v1_primitives.T_sapling_state,
        [ unparse_memo_size loc_value memo_size ])
    | Script_typed_ir.Chest_key_t ⇒ (Michelson_v1_primitives.T_chest_key, nil)
    | Script_typed_ir.Chest_t ⇒ (Michelson_v1_primitives.T_chest, nil)
    end in
  let annot :=
    match at_node with
    | None ⇒ nil
    |
      Some {|
        Script_typed_ir.entrypoint_info.name := name;
          Script_typed_ir.entrypoint_info.original_type_expr := _
          |} ⇒ [ Alpha_context.Entrypoint.unparse_as_field_annot name ]
    end in
  Micheline.Prim loc_value name args annot.

Definition unparse_ty_uncarbonated {A : Set}
  (loc_value : A) (ty : Script_typed_ir.ty)
  : Alpha_context.Script.michelson_node A :=
  unparse_ty_entrypoints_uncarbonated loc_value ty
    Script_typed_ir.no_entrypoints.

Definition unparse_ty {A : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (ty : Script_typed_ir.ty)
  : M? (Alpha_context.Script.michelson_node A × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt (Unparse_costs.unparse_type ty) in
  return? ((unparse_ty_uncarbonated loc_value ty), ctxt).

Definition unparse_comparable_ty {A : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (comp_ty : Script_typed_ir.comparable_ty)
  : M? (Alpha_context.Script.michelson_node A × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Unparse_costs.unparse_comparable_type comp_ty) in
  return? ((unparse_comparable_ty_uncarbonated loc_value comp_ty), ctxt).

Definition unparse_parameter_ty {A : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (ty : Script_typed_ir.ty)
  (entrypoints : Script_typed_ir.entrypoints)
  : M? (Alpha_context.Script.michelson_node A × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt (Unparse_costs.unparse_type ty) in
  return?
    ((unparse_ty_entrypoints_uncarbonated loc_value ty
      entrypoints.(Script_typed_ir.entrypoints.root)), ctxt).

Definition serialize_ty_for_error (ty : Script_typed_ir.ty)
  : Micheline.canonical Alpha_context.Script.prim :=
  Micheline.strip_locations (unparse_ty_uncarbonated tt ty).

Fixpoint comparable_ty_of_ty
  (ctxt : Alpha_context.context) (loc_value : Alpha_context.Script.location)
  (ty : Script_typed_ir.ty)
  : M? (Script_typed_ir.comparable_ty × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt Typecheck_costs.comparable_ty_of_ty_cycle in
  match ty with
  | Script_typed_ir.Unit_t ⇒ return? (Script_typed_ir.Unit_t, ctxt)
  | Script_typed_ir.Never_t ⇒ return? (Script_typed_ir.Never_t, ctxt)
  | Script_typed_ir.Int_t ⇒ return? (Script_typed_ir.Int_t, ctxt)
  | Script_typed_ir.Nat_t ⇒ return? (Script_typed_ir.Nat_t, ctxt)
  | Script_typed_ir.Signature_t ⇒ return? (Script_typed_ir.Signature_t, ctxt)
  | Script_typed_ir.String_t ⇒ return? (Script_typed_ir.String_t, ctxt)
  | Script_typed_ir.Bytes_t ⇒ return? (Script_typed_ir.Bytes_t, ctxt)
  | Script_typed_ir.Mutez_t ⇒ return? (Script_typed_ir.Mutez_t, ctxt)
  | Script_typed_ir.Bool_t ⇒ return? (Script_typed_ir.Bool_t, ctxt)
  | Script_typed_ir.Key_hash_t ⇒ return? (Script_typed_ir.Key_hash_t, ctxt)
  | Script_typed_ir.Key_t ⇒ return? (Script_typed_ir.Key_t, ctxt)
  | Script_typed_ir.Timestamp_t ⇒ return? (Script_typed_ir.Timestamp_t, ctxt)
  | Script_typed_ir.Address_t ⇒ return? (Script_typed_ir.Address_t, ctxt)
  | Script_typed_ir.Tx_rollup_l2_address_t ⇒
    return? (Script_typed_ir.Tx_rollup_l2_address_t, ctxt)
  | Script_typed_ir.Chain_id_t ⇒ return? (Script_typed_ir.Chain_id_t, ctxt)
  | Script_typed_ir.Pair_t l_value r_value pname _ ⇒
    let? '(lty, ctxt) := comparable_ty_of_ty ctxt loc_value l_value in
    let? '(rty, ctxt) := comparable_ty_of_ty ctxt loc_value r_value in
    return? ((Script_typed_ir.Pair_t lty rty pname Dependent_bool.YesYes), ctxt)
  | Script_typed_ir.Union_t l_value r_value meta _ ⇒
    let? '(lty, ctxt) := comparable_ty_of_ty ctxt loc_value l_value in
    let? '(rty, ctxt) := comparable_ty_of_ty ctxt loc_value r_value in
    return? ((Script_typed_ir.Union_t lty rty meta Dependent_bool.YesYes), ctxt)
  | Script_typed_ir.Option_t tt_value meta _ ⇒
    let? '(ty, ctxt) := comparable_ty_of_ty ctxt loc_value tt_value in
    return? ((Script_typed_ir.Option_t ty meta Dependent_bool.Yes), ctxt)
  |
    (Script_typed_ir.Lambda_t _ _ _ | Script_typed_ir.List_t _ _ |
    Script_typed_ir.Ticket_t _ _ | Script_typed_ir.Set_t _ _ |
    Script_typed_ir.Map_t _ _ _ | Script_typed_ir.Big_map_t _ _ _ |
    Script_typed_ir.Contract_t _ _ | Script_typed_ir.Operation_t |
    Script_typed_ir.Bls12_381_fr_t | Script_typed_ir.Bls12_381_g1_t |
    Script_typed_ir.Bls12_381_g2_t | Script_typed_ir.Sapling_state_t _ |
    Script_typed_ir.Sapling_transaction_t _ |
    Script_typed_ir.Sapling_transaction_deprecated_t _ |
    Script_typed_ir.Chest_key_t | Script_typed_ir.Chest_t) ⇒
    let t_value := serialize_ty_for_error ty in
    Error_monad.error_value
      (Build_extensible "Comparable_type_expected"
        (Alpha_context.Script.location ×
          Micheline.canonical Alpha_context.Script.prim) (loc_value, t_value))
  end.

Fixpoint unparse_stack_uncarbonated
  (function_parameter : Script_typed_ir.stack_ty)
  : list Alpha_context.Script.expr :=
  match function_parameter with
  | Script_typed_ir.Bot_t ⇒ nil
  | Script_typed_ir.Item_t ty rest ⇒
    let uty := unparse_ty_uncarbonated tt ty in
    let urest := unparse_stack_uncarbonated rest in
    cons (Micheline.strip_locations uty) urest
  end.

Definition serialize_stack_for_error
  (ctxt : Alpha_context.context) (stack_ty : Script_typed_ir.stack_ty)
  : list Alpha_context.Script.expr :=
  match Alpha_context.Gas.level ctxt with
  | Alpha_context.Gas.Unaccounted ⇒ unparse_stack_uncarbonated stack_ty
  | Alpha_context.Gas.Limited _ ⇒ nil
  end.

Definition unparse_unit {A B C : Set}
  (loc_value : A) (ctxt : B) (function_parameter : unit)
  : Pervasives.result (Micheline.node A Alpha_context.Script.prim × B) C :=
  let '_ := function_parameter in
  return?
    ((Micheline.Prim loc_value Michelson_v1_primitives.D_Unit nil nil), ctxt).

Definition unparse_int {A B C D : Set}
  (loc_value : A) (ctxt : B) (v_value : Alpha_context.Script_int.num)
  : Pervasives.result (Micheline.node A C × B) D :=
  return?
    ((Micheline.Int loc_value (Alpha_context.Script_int.to_zint v_value)), ctxt).

Definition unparse_nat {A B C D : Set}
  (loc_value : A) (ctxt : B) (v_value : Alpha_context.Script_int.num)
  : Pervasives.result (Micheline.node A C × B) D :=
  return?
    ((Micheline.Int loc_value (Alpha_context.Script_int.to_zint v_value)), ctxt).

Definition unparse_string {A B C D : Set}
  (loc_value : A) (ctxt : B) (s_value : Alpha_context.Script_string.t)
  : Pervasives.result (Micheline.node A C × B) D :=
  return?
    ((Micheline.String loc_value (Alpha_context.Script_string.to_string s_value)),
      ctxt).

Definition unparse_bytes {A B C D : Set}
  (loc_value : A) (ctxt : B) (s_value : bytes)
  : Pervasives.result (Micheline.node A C × B) D :=
  return? ((Micheline.Bytes loc_value s_value), ctxt).

Definition unparse_bool {A B C : Set}
  (loc_value : A) (ctxt : B) (b_value : bool)
  : Pervasives.result (Micheline.node A Alpha_context.Script.prim × B) C :=
  return?
    ((Micheline.Prim loc_value
      (if b_value then
        Michelson_v1_primitives.D_True
      else
        Michelson_v1_primitives.D_False) nil nil), ctxt).

Definition unparse_timestamp {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (t_value : Alpha_context.Script_timestamp.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    return?
      ((Micheline.Int loc_value (Alpha_context.Script_timestamp.to_zint t_value)),
        ctxt)
  | Readable ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.timestamp_readable
      in
    match Alpha_context.Script_timestamp.to_notation t_value with
    | None ⇒
      return?
        ((Micheline.Int loc_value
          (Alpha_context.Script_timestamp.to_zint t_value)), ctxt)
    | Some s_value ⇒ return? ((Micheline.String loc_value s_value), ctxt)
    end
  end.

Definition unparse_address {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (function_parameter : Script_typed_ir.address)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let '{|
    Script_typed_ir.address.destination := destination;
      Script_typed_ir.address.entrypoint := entrypoint
      |} := function_parameter in
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        (Data_encoding.tup2 Alpha_context.Destination.encoding
          Alpha_context.Entrypoint.value_encoding) (destination, entrypoint) in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_readable
      in
    let notation :=
      Pervasives.op_caret (Alpha_context.Destination.to_b58check destination)
        (Alpha_context.Entrypoint.to_address_suffix entrypoint) in
    return? ((Micheline.String loc_value notation), ctxt)
  end.

Definition unparse_tx_rollup_l2_address {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (tx_address : Script_typed_ir.tx_rollup_l2_address)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let tx_address := Indexable.to_value tx_address in
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None Tx_rollup_l2_address.encoding
        tx_address in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.contract_readable
      in
    let b58check := Tx_rollup_l2_address.to_b58check tx_address in
    return? ((Micheline.String loc_value b58check), ctxt)
  end.

Definition unparse_contract {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (function_parameter : Script_typed_ir.typed_contract)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let
    'Script_typed_ir.Typed_contract {|
      Script_typed_ir.typed_contract.Typed_contract.arg_ty := _;
        Script_typed_ir.typed_contract.Typed_contract.address := address
        |} := function_parameter in
  unparse_address loc_value ctxt mode address.

Definition unparse_signature {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (s_value : Script_typed_ir.Script_signature.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let s_value := Script_typed_ir.Script_signature.get s_value in
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt :=
      Alpha_context.Gas.consume ctxt Unparse_costs.signature_optimized in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None Signature.encoding s_value in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.signature_readable
      in
    return? ((Micheline.String loc_value (Signature.to_b58check s_value)), ctxt)
  end.

Definition unparse_mutez {A B C D : Set}
  (loc_value : A) (ctxt : B) (v_value : Alpha_context.Tez.tez)
  : Pervasives.result (Micheline.node A C × B) D :=
  return?
    ((Micheline.Int loc_value (Z.of_int64 (Alpha_context.Tez.to_mutez v_value))),
      ctxt).

Definition unparse_key {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (k_value : Signature.public_key)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt :=
      Alpha_context.Gas.consume ctxt Unparse_costs.public_key_optimized in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding) k_value in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable ⇒
    let? ctxt :=
      Alpha_context.Gas.consume ctxt Unparse_costs.public_key_readable in
    return?
      ((Micheline.String loc_value
        (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.to_b58check) k_value)),
        ctxt)
  end.

Definition unparse_key_hash {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (k_value : Signature.public_key_hash)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.key_hash_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding) k_value
      in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.key_hash_readable
      in
    return?
      ((Micheline.String loc_value
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check)
          k_value)), ctxt)
  end.

Definition unparse_operation {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (function_parameter : Script_typed_ir.operation)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let '{|
    Script_typed_ir.operation.piop := piop;
      Script_typed_ir.operation.lazy_storage_diff := _
      |} := function_parameter in
  let iop := Apply_results.contents_of_packed_internal_operation piop in
  let bytes_value :=
    Data_encoding.Binary.to_bytes_exn None
      Apply_results.internal_contents_encoding iop in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt (Unparse_costs.operation bytes_value) in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_chain_id {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (chain_id : Script_typed_ir.Script_chain_id.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  match mode with
  | (Optimized | Optimized_legacy) ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.chain_id_optimized
      in
    let bytes_value :=
      Data_encoding.Binary.to_bytes_exn None
        Script_typed_ir.Script_chain_id.encoding chain_id in
    return? ((Micheline.Bytes loc_value bytes_value), ctxt)
  | Readable ⇒
    let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.chain_id_readable
      in
    return?
      ((Micheline.String loc_value
        (Script_typed_ir.Script_chain_id.to_b58check chain_id)), ctxt)
  end.

Definition unparse_bls12_381_g1 {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (x_value : Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.t))
  : M? (Micheline.node A B × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.bls12_381_g1 in
  let bytes_value :=
    Script_typed_ir.Script_bls.G1.(Script_typed_ir.Script_bls.S.to_bytes)
      x_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_bls12_381_g2 {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (x_value : Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.t))
  : M? (Micheline.node A B × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.bls12_381_g2 in
  let bytes_value :=
    Script_typed_ir.Script_bls.G2.(Script_typed_ir.Script_bls.S.to_bytes)
      x_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_bls12_381_fr {A B : Set}
  (loc_value : A) (ctxt : Alpha_context.context)
  (x_value : Script_typed_ir.Script_bls.Fr.t)
  : M? (Micheline.node A B × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.bls12_381_fr in
  let bytes_value := Script_typed_ir.Script_bls.Fr.to_bytes x_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Definition unparse_with_data_encoding {A B C : Set}
  (loc_value : A) (ctxt : Alpha_context.context) (s_value : B)
  (unparse_cost : Alpha_context.Gas.cost) (encoding : Data_encoding.encoding B)
  : M? (Micheline.node A C × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt unparse_cost in
  let bytes_value := Data_encoding.Binary.to_bytes_exn None encoding s_value in
  return? ((Micheline.Bytes loc_value bytes_value), ctxt).

Inductive comb_witness : Set :=
| Comb_Pair : comb_witness → comb_witness
| Comb_Any : comb_witness.

Definition unparse_pair {A B C D E r G : Set}
  (loc_value : A)
  (unparse_l :
    B → C →
    Pervasives.result (Micheline.node A Alpha_context.Script.prim × D) E)
  (unparse_r :
    D → r →
    Pervasives.result (Micheline.node A Alpha_context.Script.prim × G) E)
  (ctxt : B) (mode : unparsing_mode) (r_comb_witness : comb_witness)
  (function_parameter : C × r)
  : Pervasives.result (Micheline.node A Alpha_context.Script.prim × G) E :=
  let '(l_value, r_value) := function_parameter in
  let? '(l_value, ctxt) := unparse_l ctxt l_value in
  let? '(r_value, ctxt) := unparse_r ctxt r_value in
  let res :=
    match (mode, r_comb_witness, r_value) with
    | (Optimized, Comb_Pair _, Micheline.Seq _ r_value) ⇒
      Micheline.Seq loc_value (cons l_value r_value)
    |
      (Optimized, Comb_Pair (Comb_Pair _),
        Micheline.Prim _ Michelson_v1_primitives.D_Pair
          (cons x2
            (cons
              (Micheline.Prim _ Michelson_v1_primitives.D_Pair
                (cons x3 (cons x4 [])) []) [])) []) ⇒
      Micheline.Seq loc_value [ l_value; x2; x3; x4 ]
    |
      (Readable, Comb_Pair _,
        Micheline.Prim _ Michelson_v1_primitives.D_Pair xs []) ⇒
      Micheline.Prim loc_value Michelson_v1_primitives.D_Pair (cons l_value xs)
        nil
    | _ ⇒
      Micheline.Prim loc_value Michelson_v1_primitives.D_Pair
        [ l_value; r_value ] nil
    end in
  return? (res, ctxt).

Definition unparse_union {A B C D E F : Set}
  (loc_value : A)
  (unparse_l :
    B → C →
    Pervasives.result (Micheline.node A Alpha_context.Script.prim × D) E)
  (unparse_r :
    B → F →
    Pervasives.result (Micheline.node A Alpha_context.Script.prim × D) E)
  (ctxt : B) (function_parameter : Script_typed_ir.union C F)
  : Pervasives.result (Micheline.node A Alpha_context.Script.prim × D) E :=
  match function_parameter with
  | Script_typed_ir.L l_value ⇒
    let? '(l_value, ctxt) := unparse_l ctxt l_value in
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_Left [ l_value ] nil),
        ctxt)
  | Script_typed_ir.R r_value ⇒
    let? '(r_value, ctxt) := unparse_r ctxt r_value in
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_Right [ r_value ] nil),
        ctxt)
  end.

Definition unparse_option {A B C D : Set}
  (loc_value : A)
  (unparse_v :
    B → C →
    Pervasives.result (Micheline.node A Alpha_context.Script.prim × B) D)
  (ctxt : B) (function_parameter : option C)
  : Pervasives.result (Micheline.node A Alpha_context.Script.prim × B) D :=
  match function_parameter with
  | Some v_value ⇒
    let? '(v_value, ctxt) := unparse_v ctxt v_value in
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_Some [ v_value ] nil),
        ctxt)
  | None ⇒
    return?
      ((Micheline.Prim loc_value Michelson_v1_primitives.D_None nil nil), ctxt)
  end.

Definition comparable_comb_witness2
  (function_parameter : Script_typed_ir.comparable_ty) : comb_witness :=
  match function_parameter with
  |
    Script_typed_ir.Pair_t _ (Script_typed_ir.Pair_t _ _ _ _) _
      Dependent_bool.YesYes ⇒ Comb_Pair (Comb_Pair Comb_Any)
  | Script_typed_ir.Pair_t _ _ _ _ ⇒ Comb_Pair Comb_Any
  | _ ⇒ Comb_Any
  end.

#[bypass_check(guard)]
Fixpoint unparse_comparable_data {loc a : Set}
  (loc_value : loc) (ctxt : Alpha_context.context) (mode : unparsing_mode)
  (ty : Script_typed_ir.comparable_ty) (a_value : a) {struct ty}
  : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Unparse_costs.unparse_data_cycle
    in
  match (ty, a_value) with
  | (Script_typed_ir.Unit_t, v_value) ⇒
    let v_value := cast unit v_value in
    unparse_unit loc_value ctxt v_value
  | (Script_typed_ir.Int_t, v_value) ⇒
    let v_value := cast Alpha_context.Script_int.num v_value in
    unparse_int loc_value ctxt v_value
  | (Script_typed_ir.Nat_t, v_value) ⇒
    let v_value := cast Alpha_context.Script_int.num v_value in
    unparse_nat loc_value ctxt v_value
  | (Script_typed_ir.String_t, s_value) ⇒
    let s_value := cast Alpha_context.Script_string.t s_value in
    unparse_string loc_value ctxt s_value
  | (Script_typed_ir.Bytes_t, s_value) ⇒
    let s_value := cast bytes s_value in
    unparse_bytes loc_value ctxt s_value
  | (Script_typed_ir.Bool_t, b_value) ⇒
    let b_value := cast bool b_value in
    unparse_bool loc_value ctxt b_value
  | (Script_typed_ir.Timestamp_t, t_value) ⇒
    let t_value := cast Alpha_context.Script_timestamp.t t_value in
    unparse_timestamp loc_value ctxt mode t_value
  | (Script_typed_ir.Address_t, address) ⇒
    let address := cast Script_typed_ir.address address in
    unparse_address loc_value ctxt mode address
  | (Script_typed_ir.Tx_rollup_l2_address_t, address) ⇒
    let address := cast Script_typed_ir.tx_rollup_l2_address address in
    unparse_tx_rollup_l2_address loc_value ctxt mode address
  | (Script_typed_ir.Signature_t, s_value) ⇒
    let s_value := cast Script_typed_ir.signature s_value in
    unparse_signature loc_value ctxt mode s_value
  | (Script_typed_ir.Mutez_t, v_value) ⇒
    let v_value := cast Tez_repr.t v_value in
    unparse_mutez loc_value ctxt v_value
  | (Script_typed_ir.Key_t, k_value) ⇒
    let k_value := cast Alpha_context.public_key k_value in
    unparse_key loc_value ctxt mode k_value
  | (Script_typed_ir.Key_hash_t, k_value) ⇒
    let k_value := cast Alpha_context.public_key_hash k_value in
    unparse_key_hash loc_value ctxt mode k_value
  | (Script_typed_ir.Chain_id_t, chain_id) ⇒
    let chain_id := cast Script_typed_ir.Script_chain_id.t chain_id in
    unparse_chain_id loc_value ctxt mode chain_id
  | (Script_typed_ir.Pair_t tl tr _ Dependent_bool.YesYes, pair_value) ⇒
    let 'existT _ [__0, __1] [pair_value, tr, tl] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__0, __1] ⇒
          [__0 × __1 ** Script_typed_ir.ty ** Script_typed_ir.ty])
        [pair_value, tr, tl] in
    let r_witness := comparable_comb_witness2 tr in
    let unparse_l (ctxt : Alpha_context.context) (v_value : __0)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data loc_value ctxt mode tl v_value in
    let unparse_r (ctxt : Alpha_context.context) (v_value : __1)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data loc_value ctxt mode tr v_value in
    unparse_pair loc_value unparse_l unparse_r ctxt mode r_witness pair_value
  | (Script_typed_ir.Union_t tl tr _ Dependent_bool.YesYes, v_value) ⇒
    let 'existT _ [__2, __3] [v_value, tr, tl] :=
      cast_exists (Es := [Set ** Set])
        (fun '[__2, __3] ⇒
          [Script_typed_ir.union __2 __3 ** Script_typed_ir.ty **
            Script_typed_ir.ty]) [v_value, tr, tl] in
    let unparse_l (ctxt : Alpha_context.context) (v_value : __2)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data loc_value ctxt mode tl v_value in
    let unparse_r (ctxt : Alpha_context.context) (v_value : __3)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data loc_value ctxt mode tr v_value in
    unparse_union loc_value unparse_l unparse_r ctxt v_value
  | (Script_typed_ir.Option_t t_value _ Dependent_bool.Yes, v_value) ⇒
    let 'existT _ __4 [v_value, t_value] :=
      cast_exists (Es := Set) (fun __4 ⇒ [option __4 ** Script_typed_ir.ty])
        [v_value, t_value] in
    let unparse_v (ctxt : Alpha_context.context) (v_value : __4)
      : M? (Alpha_context.Script.michelson_node loc × Alpha_context.context) :=
      unparse_comparable_data loc_value ctxt mode t_value v_value in
    unparse_option loc_value unparse_v ctxt v_value
  | _ ⇒ unreachable_gadt_branch
  end.

Definition pack_node {A : Set}
  (unparsed : Alpha_context.Script.michelson_node A)
  (ctxt : Alpha_context.context) : M? (bytes × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_locations_cost unparsed) in
  let bytes_value :=
    Data_encoding.Binary.to_bytes_exn None Alpha_context.Script.expr_encoding
      (Micheline.strip_locations unparsed) in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.serialized_cost bytes_value) in
  let bytes_value := Bytes.cat (Bytes.of_string "\005") bytes_value in
  return? (bytes_value, ctxt).

Definition pack_comparable_data {A : Set}
  (ctxt : Alpha_context.context) (ty : Script_typed_ir.comparable_ty) (data : A)
  (mode : unparsing_mode) : M? (bytes × Alpha_context.context) :=
  let? '(unparsed, ctxt) := unparse_comparable_data tt ctxt mode ty data in
  pack_node unparsed ctxt.

Definition hash_bytes (ctxt : Alpha_context.context) (bytes_value : bytes)
  : M? (Script_expr_hash.t × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Michelson_v1_gas.Cost_of.Interpreter.blake2b bytes_value) in
  return? ((Script_expr_hash.hash_bytes None [ bytes_value ]), ctxt).

Definition hash_comparable_data {A : Set}
  (ctxt : Alpha_context.context) (ty : Script_typed_ir.comparable_ty) (data : A)
  : M? (Script_expr_hash.t × Alpha_context.context) :=
  let? '(bytes_value, ctxt) :=
    pack_comparable_data ctxt ty data Optimized_legacy in
  hash_bytes ctxt bytes_value.

Definition check_dupable_comparable_ty
  (function_parameter : Script_typed_ir.comparable_ty) : unit :=
  match function_parameter with
  |
    (Script_typed_ir.Unit_t | Script_typed_ir.Never_t | Script_typed_ir.Int_t |
    Script_typed_ir.Nat_t | Script_typed_ir.Signature_t |
    Script_typed_ir.String_t | Script_typed_ir.Bytes_t | Script_typed_ir.Mutez_t
    | Script_typed_ir.Bool_t | Script_typed_ir.Key_hash_t |
    Script_typed_ir.Key_t | Script_typed_ir.Timestamp_t |
    Script_typed_ir.Chain_id_t | Script_typed_ir.Address_t |
    Script_typed_ir.Tx_rollup_l2_address_t | Script_typed_ir.Pair_t _ _ _ _ |
    Script_typed_ir.Union_t _ _ _ _ | Script_typed_ir.Option_t _ _ _) ⇒ tt
  | _ ⇒ unreachable_gadt_branch
  end.

Definition check_dupable_ty
  (ctxt : Alpha_context.context) (loc_value : Alpha_context.Script.location)
  (ty : Script_typed_ir.ty) : M? Alpha_context.context :=
  let fix aux
    (loc_value : Alpha_context.Script.location) (ty : Script_typed_ir.ty)
    : Gas_monad.t unit Error_monad._error :=
    Gas_monad.Syntax.op_letstar
      (Gas_monad.consume_gas Typecheck_costs.check_dupable_cycle)
      (fun function_parameter ⇒
        let '_ := function_parameter in
        match ty with
        | Script_typed_ir.Unit_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Int_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Nat_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Signature_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.String_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Bytes_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Mutez_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Key_hash_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Key_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Timestamp_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Address_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Tx_rollup_l2_address_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Bool_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Contract_t _ _ ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Operation_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Chain_id_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Never_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Bls12_381_g1_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Bls12_381_g2_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Bls12_381_fr_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Sapling_state_t _ ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Sapling_transaction_t _ ⇒
          Gas_monad.Syntax.return_unit
        | Script_typed_ir.Sapling_transaction_deprecated_t _ ⇒
          Gas_monad.Syntax.return_unit
        | Script_typed_ir.Chest_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Chest_key_t ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Ticket_t _ _ ⇒
          Gas_monad.Syntax.fail
            (Build_extensible "Unexpected_ticket" Alpha_context.Script.location
              loc_value)
        | Script_typed_ir.Pair_t ty_a ty_b _ _ ⇒
          Gas_monad.Syntax.op_letstar (aux loc_value ty_a)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              aux loc_value ty_b)
        | Script_typed_ir.Union_t ty_a ty_b _ _ ⇒
          Gas_monad.Syntax.op_letstar (aux loc_value ty_a)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              aux loc_value ty_b)
        | Script_typed_ir.Lambda_t _ _ _ ⇒ Gas_monad.Syntax.return_unit
        | Script_typed_ir.Option_t ty _ _ ⇒ aux loc_value ty
        | Script_typed_ir.List_t ty _ ⇒ aux loc_value ty
        | Script_typed_ir.Set_t key_ty _ ⇒
          let '_ := check_dupable_comparable_ty key_ty in
          Gas_monad.Syntax.return_unit
        | Script_typed_ir.Map_t key_ty val_ty _ ⇒
          let '_ := check_dupable_comparable_ty key_ty in
          aux loc_value val_ty
        | Script_typed_ir.Big_map_t key_ty val_ty _ ⇒
          let '_ := check_dupable_comparable_ty key_ty in
          aux loc_value val_ty
        end) in
  let gas := aux loc_value ty in
  let? '(res, ctxt) := Gas_monad.run ctxt gas in
  match res with
  | Pervasives.Ok _ ⇒ return? ctxt
  | Pervasives.Error e_value ⇒ Error_monad.error_value e_value
  end.

Inductive eq : Set :=
| Eq : eq.

Definition type_metadata_eq {error_trace : Set}
  (error_details : Script_tc_errors.error_details)
  (function_parameter : Script_typed_ir.ty_metadata)
  : Script_typed_ir.ty_metadata → Pervasives.result unit error_trace :=
  let '{| Script_typed_ir.ty_metadata.size := size_a |} := function_parameter in
  fun (function_parameter : Script_typed_ir.ty_metadata) ⇒
    let '{| Script_typed_ir.ty_metadata.size := size_b |} := function_parameter
      in
    Script_typed_ir.Type_size.check_eq error_details size_a size_b.

Definition default_ty_eq_error
  (ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.ty) : Error_monad._error :=
  let ty1 := serialize_ty_for_error ty1 in
  let ty2 := serialize_ty_for_error ty2 in
  Build_extensible "Inconsistent_types"
    (option Alpha_context.Script.location ×
      Micheline.canonical Alpha_context.Script.prim ×
      Micheline.canonical Alpha_context.Script.prim) (None, ty1, ty2).

Fixpoint comparable_ty_eq {error_trace : Set}
  (error_details : Script_tc_errors.error_details)
  (ta : Script_typed_ir.comparable_ty) (tb : Script_typed_ir.comparable_ty)
  : Gas_monad.t eq error_trace :=
  Gas_monad.Syntax.op_letstar
    (Gas_monad.consume_gas Typecheck_costs.merge_cycle)
    (fun function_parameter ⇒
      let '_ := function_parameter in
      let type_metadata_eq
        (meta_a : Script_typed_ir.ty_metadata)
        (meta_b : Script_typed_ir.ty_metadata) : Gas_monad.t unit error_trace :=
        Gas_monad.of_result (type_metadata_eq error_details meta_a meta_b) in
      let not_equal {B : Set} (function_parameter : unit)
        : Gas_monad.t B error_trace :=
        let '_ := function_parameter in
        Gas_monad.of_result
          (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
                (default_ty_eq_error (ty_of_comparable_ty ta)
                  (ty_of_comparable_ty tb)))
            end) in
      match (ta, tb) with
      | (Script_typed_ir.Unit_t, Script_typed_ir.Unit_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Unit_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Never_t, Script_typed_ir.Never_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Never_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Int_t, Script_typed_ir.Int_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Int_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Nat_t, Script_typed_ir.Nat_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Nat_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Signature_t, Script_typed_ir.Signature_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Signature_t, _) ⇒ not_equal tt
      | (Script_typed_ir.String_t, Script_typed_ir.String_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.String_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Bytes_t, Script_typed_ir.Bytes_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Bytes_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Mutez_t, Script_typed_ir.Mutez_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Mutez_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Bool_t, Script_typed_ir.Bool_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Bool_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Key_hash_t, Script_typed_ir.Key_hash_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Key_hash_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Key_t, Script_typed_ir.Key_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Key_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Timestamp_t, Script_typed_ir.Timestamp_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Timestamp_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Chain_id_t, Script_typed_ir.Chain_id_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Chain_id_t, _) ⇒ not_equal tt
      | (Script_typed_ir.Address_t, Script_typed_ir.Address_t) ⇒
        Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Address_t, _) ⇒ not_equal tt
      |
        (Script_typed_ir.Tx_rollup_l2_address_t,
          Script_typed_ir.Tx_rollup_l2_address_t) ⇒ Gas_monad.Syntax._return Eq
      | (Script_typed_ir.Tx_rollup_l2_address_t, _) ⇒ not_equal tt
      |
        (Script_typed_ir.Pair_t left_a right_a meta_a Dependent_bool.YesYes,
          Script_typed_ir.Pair_t left_b right_b meta_b Dependent_bool.YesYes) ⇒
        Gas_monad.Syntax.op_letstar (type_metadata_eq meta_a meta_b)
          (fun function_parameter ⇒
            let '_ := function_parameter in
            Gas_monad.Syntax.op_letstar
              (comparable_ty_eq error_details left_a left_b)
              (fun function_parameter ⇒
                let 'Eq := function_parameter in
                Gas_monad.Syntax.op_letplus
                  (comparable_ty_eq error_details right_a right_b)
                  (fun function_parameter ⇒
                    let 'Eq := function_parameter in
                    Eq)))
      | (Script_typed_ir.Pair_t _ _ _ _, _) ⇒ not_equal tt
      |
        (Script_typed_ir.Union_t left_a right_a meta_a Dependent_bool.YesYes,
          Script_typed_ir.Union_t left_b right_b meta_b Dependent_bool.YesYes)
        ⇒
        Gas_monad.Syntax.op_letstar (type_metadata_eq meta_a meta_b)
          (fun function_parameter ⇒
            let '_ := function_parameter in
            Gas_monad.Syntax.op_letstar
              (comparable_ty_eq error_details left_a left_b)
              (fun function_parameter ⇒
                let 'Eq := function_parameter in
                Gas_monad.Syntax.op_letplus
                  (comparable_ty_eq error_details right_a right_b)
                  (fun function_parameter ⇒
                    let 'Eq := function_parameter in
                    Eq)))
      | (Script_typed_ir.Union_t _ _ _ _, _) ⇒ not_equal tt
      |
        (Script_typed_ir.Option_t ta meta_a Dependent_bool.Yes,
          Script_typed_ir.Option_t tb meta_b Dependent_bool.Yes) ⇒
        Gas_monad.Syntax.op_letstar (type_metadata_eq meta_a meta_b)
          (fun function_parameter ⇒
            let '_ := function_parameter in
            Gas_monad.Syntax.op_letplus (comparable_ty_eq error_details ta tb)
              (fun function_parameter ⇒
                let 'Eq := function_parameter in
                Eq))
      | (Script_typed_ir.Option_t _ _ _, _) ⇒ not_equal tt
      | _ ⇒ unreachable_gadt_branch
      end).

Definition memo_size_eq {error_trace : Set}
  (error_details : Script_tc_errors.error_details)
  (ms1 : Alpha_context.Sapling.Memo_size.t)
  (ms2 : Alpha_context.Sapling.Memo_size.t)
  : Pervasives.result unit error_trace :=
  if Alpha_context.Sapling.Memo_size.equal ms1 ms2 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_memo_sizes"
            (Alpha_context.Sapling.Memo_size.t ×
              Alpha_context.Sapling.Memo_size.t) (ms1, ms2)))
      end.

Same as comparable_ty_eq but for any types.

Definition ty_eq {error_trace : Set}
  (error_details : Script_tc_errors.error_details)
  (loc_value : Alpha_context.Script.location) (ty1 : Script_typed_ir.ty)
  (ty2 : Script_typed_ir.ty) : Gas_monad.t eq error_trace :=
  let type_metadata_eq
    (meta1 : Script_typed_ir.ty_metadata) (meta2 : Script_typed_ir.ty_metadata)
    : Gas_monad.t unit error_trace :=
    Gas_monad.record_trace_eval error_details
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        let ty1 := serialize_ty_for_error ty1 in
        let ty2 := serialize_ty_for_error ty2 in
        Build_extensible "Inconsistent_types"
          (option Alpha_context.Script.location ×
            Micheline.canonical Alpha_context.Script.prim ×
            Micheline.canonical Alpha_context.Script.prim)
          ((Some loc_value), ty1, ty2))
      (Gas_monad.of_result (type_metadata_eq error_details meta1 meta2)) in
  let memo_size_eq
    (ms1 : Alpha_context.Sapling.Memo_size.t)
    (ms2 : Alpha_context.Sapling.Memo_size.t) : Gas_monad.t unit error_trace :=
    Gas_monad.of_result (memo_size_eq error_details ms1 ms2) in
  let fix help0 (ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.ty)
    : Gas_monad.t eq error_trace :=
    let help (ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.ty)
      : Gas_monad.t eq error_trace :=
      Gas_monad.record_trace_eval error_details
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          default_ty_eq_error ty1 ty2) (help0 ty1 ty2) in
    Gas_monad.Syntax.op_letstar
      (Gas_monad.consume_gas Typecheck_costs.merge_cycle)
      (fun function_parameter ⇒
        let '_ := function_parameter in
        let not_equal {B : Set} (function_parameter : unit)
          : Gas_monad.t B error_trace :=
          let '_ := function_parameter in
          Gas_monad.of_result
            (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 (default_ty_eq_error ty1 ty2))
              end) in
        match (ty1, ty2) with
        | (Script_typed_ir.Unit_t, Script_typed_ir.Unit_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Unit_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Int_t, Script_typed_ir.Int_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Int_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Nat_t, Script_typed_ir.Nat_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Nat_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Key_t, Script_typed_ir.Key_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Key_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Key_hash_t, Script_typed_ir.Key_hash_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Key_hash_t, _) ⇒ not_equal tt
        | (Script_typed_ir.String_t, Script_typed_ir.String_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.String_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Bytes_t, Script_typed_ir.Bytes_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Bytes_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Signature_t, Script_typed_ir.Signature_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Signature_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Mutez_t, Script_typed_ir.Mutez_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Mutez_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Timestamp_t, Script_typed_ir.Timestamp_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Timestamp_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Address_t, Script_typed_ir.Address_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Address_t, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Tx_rollup_l2_address_t,
            Script_typed_ir.Tx_rollup_l2_address_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Tx_rollup_l2_address_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Bool_t, Script_typed_ir.Bool_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Bool_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Chain_id_t, Script_typed_ir.Chain_id_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Chain_id_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Never_t, Script_typed_ir.Never_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Never_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Operation_t, Script_typed_ir.Operation_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Operation_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Bls12_381_g1_t, Script_typed_ir.Bls12_381_g1_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Bls12_381_g1_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Bls12_381_g2_t, Script_typed_ir.Bls12_381_g2_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Bls12_381_g2_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Bls12_381_fr_t, Script_typed_ir.Bls12_381_fr_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Bls12_381_fr_t, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Map_t tal tar meta1,
            Script_typed_ir.Map_t tbl tbr meta2) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letstar (help tar tbr)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Gas_monad.Syntax.op_letplus
                    (comparable_ty_eq error_details tal tbl)
                    (fun function_parameter ⇒
                      let 'Eq := function_parameter in
                      Eq)))
        | (Script_typed_ir.Map_t _ _ _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Big_map_t tal tar meta1,
            Script_typed_ir.Big_map_t tbl tbr meta2) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letstar (help tar tbr)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Gas_monad.Syntax.op_letplus
                    (comparable_ty_eq error_details tal tbl)
                    (fun function_parameter ⇒
                      let 'Eq := function_parameter in
                      Eq)))
        | (Script_typed_ir.Big_map_t _ _ _, _) ⇒ not_equal tt
        | (Script_typed_ir.Set_t ea meta1, Script_typed_ir.Set_t eb meta2) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letplus (comparable_ty_eq error_details ea eb)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Eq))
        | (Script_typed_ir.Set_t _ _, _) ⇒ not_equal tt
        | (Script_typed_ir.Ticket_t ea meta1, Script_typed_ir.Ticket_t eb meta2)
          ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letplus (comparable_ty_eq error_details ea eb)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Eq))
        | (Script_typed_ir.Ticket_t _ _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Pair_t tal tar meta1 cmp1,
            Script_typed_ir.Pair_t tbl tbr meta2 cmp2) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letstar (help tal tbl)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Gas_monad.Syntax.op_letplus (help tar tbr)
                    (fun function_parameter ⇒
                      let 'Eq := function_parameter in
                      let 'Dependent_bool.Eq :=
                        Dependent_bool.merge_dand cmp1 cmp2 in
                      Eq)))
        | (Script_typed_ir.Pair_t _ _ _ _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Union_t tal tar meta1 cmp1,
            Script_typed_ir.Union_t tbl tbr meta2 cmp2) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letstar (help tal tbl)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Gas_monad.Syntax.op_letplus (help tar tbr)
                    (fun function_parameter ⇒
                      let 'Eq := function_parameter in
                      let 'Dependent_bool.Eq :=
                        Dependent_bool.merge_dand cmp1 cmp2 in
                      Eq)))
        | (Script_typed_ir.Union_t _ _ _ _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Lambda_t tal tar meta1,
            Script_typed_ir.Lambda_t tbl tbr meta2) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letstar (help tal tbl)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Gas_monad.Syntax.op_letplus (help tar tbr)
                    (fun function_parameter ⇒
                      let 'Eq := function_parameter in
                      Eq)))
        | (Script_typed_ir.Lambda_t _ _ _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Contract_t tal meta1,
            Script_typed_ir.Contract_t tbl meta2) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letplus (help tal tbl)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Eq))
        | (Script_typed_ir.Contract_t _ _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Option_t tva meta1 _,
            Script_typed_ir.Option_t tvb meta2 _) ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letplus (help tva tvb)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Eq))
        | (Script_typed_ir.Option_t _ _ _, _) ⇒ not_equal tt
        | (Script_typed_ir.List_t tva meta1, Script_typed_ir.List_t tvb meta2)
          ⇒
          Gas_monad.Syntax.op_letstar (type_metadata_eq meta1 meta2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Gas_monad.Syntax.op_letplus (help tva tvb)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  Eq))
        | (Script_typed_ir.List_t _ _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Sapling_state_t ms1,
            Script_typed_ir.Sapling_state_t ms2) ⇒
          Gas_monad.Syntax.op_letplus (memo_size_eq ms1 ms2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Eq)
        | (Script_typed_ir.Sapling_state_t _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Sapling_transaction_t ms1,
            Script_typed_ir.Sapling_transaction_t ms2) ⇒
          Gas_monad.Syntax.op_letplus (memo_size_eq ms1 ms2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Eq)
        | (Script_typed_ir.Sapling_transaction_t _, _) ⇒ not_equal tt
        |
          (Script_typed_ir.Sapling_transaction_deprecated_t ms1,
            Script_typed_ir.Sapling_transaction_deprecated_t ms2) ⇒
          Gas_monad.Syntax.op_letplus (memo_size_eq ms1 ms2)
            (fun function_parameter ⇒
              let '_ := function_parameter in
              Eq)
        | (Script_typed_ir.Sapling_transaction_deprecated_t _, _) ⇒
          not_equal tt
        | (Script_typed_ir.Chest_t, Script_typed_ir.Chest_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Chest_t, _) ⇒ not_equal tt
        | (Script_typed_ir.Chest_key_t, Script_typed_ir.Chest_key_t) ⇒
          Gas_monad.Syntax._return Eq
        | (Script_typed_ir.Chest_key_t, _) ⇒ not_equal tt
        end) in
  Gas_monad.record_trace_eval error_details
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      default_ty_eq_error ty1 ty2) (help0 ty1 ty2).

Fixpoint stack_eq
  (loc_value : Alpha_context.Script.location) (ctxt : Alpha_context.context)
  (lvl : int) (stack1 : Script_typed_ir.stack_ty)
  (stack2 : Script_typed_ir.stack_ty) : M? (eq × Alpha_context.context) :=
  match (stack1, stack2) with
  | (Script_typed_ir.Bot_t, Script_typed_ir.Bot_t) ⇒ return? (Eq, ctxt)
  | (Script_typed_ir.Item_t ty1 rest1, Script_typed_ir.Item_t ty2 rest2) ⇒
    let? '(eq_value, ctxt) :=
      Error_monad.record_trace (Build_extensible "Bad_stack_item" int lvl)
        (Gas_monad.run ctxt
          (ty_eq Script_tc_errors.Informative loc_value ty1 ty2)) in
    let? 'Eq := eq_value in
    let? '(Eq, ctxt) := stack_eq loc_value ctxt (lvl +i 1) rest1 rest2 in
    return? (Eq, ctxt)
  | (_, _) ⇒
    Error_monad.error_value (Build_extensible "Bad_stack_length" unit tt)
  end.

Records for the constructor parameters

Module ConstructorRecords_judgement.
  Module judgement.
    Module Failed.
      Record record {descr : Set} : Set := Build {
        descr : descr;
      }.
      Arguments record : clear implicits.
      Definition with_descr {t_descr} descr (r : record t_descr) :=
        Build t_descr descr.
    End Failed.
    Definition Failed_skeleton := Failed.record.
  End judgement.
End ConstructorRecords_judgement.
Import ConstructorRecords_judgement.

Reserved Notation "'judgement.Failed".

Inductive judgement : Set :=
| Typed : descr → judgement
| Failed : 'judgement.Failed → judgement

where "'judgement.Failed" :=
  (judgement.Failed_skeleton (Script_typed_ir.stack_ty → descr)).

Module judgement.
  Include ConstructorRecords_judgement.judgement.
  Definition Failed := 'judgement.Failed.
End judgement.

Module branch.
  Record record : Set := Build {
    branch : descr → descr → descr;
  }.
  Definition with_branch branch (r : record) :=
    Build branch.
End branch.
Definition branch := branch.record.

Definition merge_branches
  (ctxt : Alpha_context.context) (loc_value : Alpha_context.Script.location)
  (btr : judgement) (bfr : judgement) (function_parameter : branch)
  : M? (judgement × Alpha_context.context) :=
  let '{| branch.branch := branch |} := function_parameter in
  match (btr, bfr) with
  |
    (Typed ({| descr.aft := aftbt |} as dbt),
      Typed ({| descr.aft := aftbf |} as dbf)) ⇒
    let unmatched_branches (function_parameter : unit) : Error_monad._error :=
      let '_ := function_parameter in
      let aftbt := serialize_stack_for_error ctxt aftbt in
      let aftbf := serialize_stack_for_error ctxt aftbf in
      Build_extensible "Unmatched_branches"
        (Alpha_context.Script.location × Script_tc_errors.unparsed_stack_ty ×
          Script_tc_errors.unparsed_stack_ty) (loc_value, aftbt, aftbf) in
    Error_monad.record_trace_eval unmatched_branches
      (let? '(Eq, ctxt) := stack_eq loc_value ctxt 1 aftbt aftbf in
      return? ((Typed (branch dbt dbf)), ctxt))
  |
    (Failed {| judgement.Failed.descr := descrt |},
      Failed {| judgement.Failed.descr := descrf |}) ⇒
    let descr_value (ret_value : Script_typed_ir.stack_ty) : descr :=
      branch (descrt ret_value) (descrf ret_value) in
    return? ((Failed {| judgement.Failed.descr := descr_value; |}), ctxt)
  | (Typed dbt, Failed {| judgement.Failed.descr := descrf |}) ⇒
    return? ((Typed (branch dbt (descrf dbt.(descr.aft)))), ctxt)
  | (Failed {| judgement.Failed.descr := descrt |}, Typed dbf) ⇒
    return? ((Typed (branch (descrt dbf.(descr.aft)) dbf)), ctxt)
  end.

Definition parse_memo_size
  (n_value :
    Micheline.node Alpha_context.Script.location Alpha_context.Script.prim)
  : M? Alpha_context.Sapling.Memo_size.t :=
  match n_value with
  | Micheline.Int _ z_value ⇒
    match Alpha_context.Sapling.Memo_size.parse_z z_value with
    | (Pervasives.Ok _) as ok_memo_size ⇒
      cast (M? Alpha_context.Sapling.Memo_size.t) ok_memo_size
    | Pervasives.Error msg ⇒
      Error_monad.error_value
        (Build_extensible "Invalid_syntactic_constant"
          (Alpha_context.Script.location ×
            Micheline.canonical Alpha_context.Script.prim × string)
          ((location n_value), (Micheline.strip_locations n_value), msg))
    end
  | _ ⇒
    Error_monad.error_value
      (Build_extensible "Invalid_kind"
        (Alpha_context.Script.location × list Script_tc_errors.kind ×
          Script_tc_errors.kind)
        ((location n_value), [ Script_tc_errors.Int_kind ], (kind_value n_value)))
  end.

Inductive ex_comparable_ty : Set :=
| Ex_comparable_ty : Script_typed_ir.comparable_ty → ex_comparable_ty.

#[bypass_check(guard)]
Fixpoint parse_comparable_ty_aux
  (stack_depth : int) (ctxt : Alpha_context.context)
  (ty : Alpha_context.Script.node) {struct ty}
  : M? (ex_comparable_ty × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.parse_type_cycle
    in
  if stack_depth >i 10000 then
    Error_monad.error_value
      (Build_extensible "Typechecking_too_many_recursive_calls" unit tt)
  else
    match ty with
    | Micheline.Prim loc_value Michelson_v1_primitives.T_unit [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.unit_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_never [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.never_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_int [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.int_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_nat [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.nat_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_signature [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.signature_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_string [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.string_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_bytes [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.bytes_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_mutez [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.mutez_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_bool [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.bool_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_key_hash [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.key_hash_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_key [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.key_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_timestamp [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.timestamp_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_chain_id [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.chain_id_key), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_address [] annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? ((Ex_comparable_ty Script_typed_ir.address_key), ctxt)
    |
      Micheline.Prim loc_value Michelson_v1_primitives.T_tx_rollup_l2_address []
        annot ⇒
      if Alpha_context.Constants.tx_rollup_enable ctxt then
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        return?
          ((Ex_comparable_ty Script_typed_ir.tx_rollup_l2_address_key), ctxt)
      else
        Error_monad.error_value
          (Build_extensible "Tx_rollup_addresses_disabled"
            Alpha_context.Script.location loc_value)
    |
      Micheline.Prim loc_value
        ((Michelson_v1_primitives.T_unit | Michelson_v1_primitives.T_never |
        Michelson_v1_primitives.T_int | Michelson_v1_primitives.T_nat |
        Michelson_v1_primitives.T_string | Michelson_v1_primitives.T_bytes |
        Michelson_v1_primitives.T_mutez | Michelson_v1_primitives.T_bool |
        Michelson_v1_primitives.T_key_hash | Michelson_v1_primitives.T_timestamp
        | Michelson_v1_primitives.T_address | Michelson_v1_primitives.T_chain_id
        | Michelson_v1_primitives.T_signature | Michelson_v1_primitives.T_key)
          as prim) l_value _ ⇒
      Error_monad.error_value
        (Build_extensible "Invalid_arity"
          (Alpha_context.Script.location × Alpha_context.Script.prim × int × int)
          (loc_value, prim, 0, (List.length l_value)))
    |
      Micheline.Prim loc_value Michelson_v1_primitives.T_pair
        (cons _left _right) annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? _left := Script_ir_annot.remove_field_annot _left in
      let? _right :=
        match _right with
        | cons _right [] ⇒ Script_ir_annot.remove_field_annot _right
        | _right ⇒
          return?
            (Micheline.Prim loc_value Michelson_v1_primitives.T_pair _right nil)
        end in
      let? '(Ex_comparable_ty _right, ctxt) :=
        parse_comparable_ty_aux (stack_depth +i 1) ctxt _right in
      let? '(Ex_comparable_ty _left, ctxt) :=
        parse_comparable_ty_aux (stack_depth +i 1) ctxt _left in
      let? ty := Script_typed_ir.pair_key loc_value _left _right in
      return? ((Ex_comparable_ty ty), ctxt)
    |
      Micheline.Prim loc_value Michelson_v1_primitives.T_or
        (cons _left (cons _right [])) annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? _left := Script_ir_annot.remove_field_annot _left in
      let? _right := Script_ir_annot.remove_field_annot _right in
      let? '(Ex_comparable_ty _right, ctxt) :=
        parse_comparable_ty_aux (stack_depth +i 1) ctxt _right in
      let? '(Ex_comparable_ty _left, ctxt) :=
        parse_comparable_ty_aux (stack_depth +i 1) ctxt _left in
      let? ty := Script_typed_ir.union_key loc_value _left _right in
      return? ((Ex_comparable_ty ty), ctxt)
    |
      Micheline.Prim loc_value
        ((Michelson_v1_primitives.T_pair | Michelson_v1_primitives.T_or) as prim)
        l_value _ ⇒
      Error_monad.error_value
        (Build_extensible "Invalid_arity"
          (Alpha_context.Script.location × Alpha_context.Script.prim × int × int)
          (loc_value, prim, 2, (List.length l_value)))
    |
      Micheline.Prim loc_value Michelson_v1_primitives.T_option
        (cons t_value []) annot ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? '(Ex_comparable_ty t_value, ctxt) :=
        parse_comparable_ty_aux (stack_depth +i 1) ctxt t_value in
      let? ty := Script_typed_ir.option_key loc_value t_value in
      return? ((Ex_comparable_ty ty), ctxt)
    | Micheline.Prim loc_value Michelson_v1_primitives.T_option l_value _ ⇒
      Error_monad.error_value
        (Build_extensible "Invalid_arity"
          (Alpha_context.Script.location × Alpha_context.Script.prim × int × int)
          (loc_value, Michelson_v1_primitives.T_option, 1, (List.length l_value)))
    |
      Micheline.Prim loc_value
        (Michelson_v1_primitives.T_set | Michelson_v1_primitives.T_map |
        Michelson_v1_primitives.T_list | Michelson_v1_primitives.T_lambda |
        Michelson_v1_primitives.T_contract | Michelson_v1_primitives.T_operation)
        _ _ ⇒
      Error_monad.error_value
        (Build_extensible "Comparable_type_expected"
          (Alpha_context.Script.location ×
            Micheline.canonical Alpha_context.Script.prim)
          (loc_value, (Micheline.strip_locations ty)))
    | expr ⇒
      Error_monad.error_value
        (unexpected expr nil Michelson_v1_primitives.Type_namespace
          [
            Michelson_v1_primitives.T_unit;
            Michelson_v1_primitives.T_never;
            Michelson_v1_primitives.T_int;
            Michelson_v1_primitives.T_nat;
            Michelson_v1_primitives.T_string;
            Michelson_v1_primitives.T_bytes;
            Michelson_v1_primitives.T_mutez;
            Michelson_v1_primitives.T_bool;
            Michelson_v1_primitives.T_key_hash;
            Michelson_v1_primitives.T_timestamp;
            Michelson_v1_primitives.T_address;
            Michelson_v1_primitives.T_pair;
            Michelson_v1_primitives.T_or;
            Michelson_v1_primitives.T_option;
            Michelson_v1_primitives.T_chain_id;
            Michelson_v1_primitives.T_signature;
            Michelson_v1_primitives.T_key
          ])
    end.

Inductive ex_ty : Set :=
| Ex_ty : Script_typed_ir.ty → ex_ty.

Records for the constructor parameters

Module ConstructorRecords_ex_parameter_ty_and_entrypoints_node.
  Module ex_parameter_ty_and_entrypoints_node.
    Module Ex_parameter_ty_and_entrypoints_node.
      Record record {arg_type entrypoints : Set} : Set := Build {
        arg_type : arg_type;
        entrypoints : entrypoints;
      }.
      Arguments record : clear implicits.
      Definition with_arg_type {t_arg_type t_entrypoints} arg_type
        (r : record t_arg_type t_entrypoints) :=
        Build t_arg_type t_entrypoints arg_type r.(entrypoints).
      Definition with_entrypoints {t_arg_type t_entrypoints} entrypoints
        (r : record t_arg_type t_entrypoints) :=
        Build t_arg_type t_entrypoints r.(arg_type) entrypoints.
    End Ex_parameter_ty_and_entrypoints_node.
    Definition Ex_parameter_ty_and_entrypoints_node_skeleton :=
      Ex_parameter_ty_and_entrypoints_node.record.
  End ex_parameter_ty_and_entrypoints_node.
End ConstructorRecords_ex_parameter_ty_and_entrypoints_node.
Import ConstructorRecords_ex_parameter_ty_and_entrypoints_node.

Reserved Notation
  "'ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node".

Inductive ex_parameter_ty_and_entrypoints_node : Set :=
| Ex_parameter_ty_and_entrypoints_node :
  'ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node →
  ex_parameter_ty_and_entrypoints_node

where "'ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node"
  :=
  (ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node_skeleton
    Script_typed_ir.ty Script_typed_ir.entrypoints_node).

Module ex_parameter_ty_and_entrypoints_node.
  Include ConstructorRecords_ex_parameter_ty_and_entrypoints_node.ex_parameter_ty_and_entrypoints_node.
  Definition Ex_parameter_ty_and_entrypoints_node :=
    'ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.
End ex_parameter_ty_and_entrypoints_node.

[parse_ty_aux] can be used to parse regular types as well as parameter types together with their entrypoints.

In the first case, use [~ret:Don't_parse_entrypoints], [parse_ty_aux] will return an [ex_ty].

In the second case, use [~ret:Parse_entrypoints], [parse_ty_aux] will return an [ex_parameter_ty_and_entrypoints].

Inductive parse_ty_ret : Set :=
| Don't_parse_entrypoints : parse_ty_ret
| Parse_entrypoints : parse_ty_ret.

Reserved Notation "'parse_passable_ty_aux_with_ret".
Reserved Notation "'parse_any_ty_aux".
Reserved Notation "'parse_big_map_value_ty_aux".

#[bypass_check(guard)]
Fixpoint parse_ty_aux {ret : Set}
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (allow_lazy_storage : bool) (allow_operation : bool) (allow_contract : bool)
  (allow_ticket : bool) (ret_value : parse_ty_ret)
  (node_value : Alpha_context.Script.node) {struct node_value}
  : M? (ret × Alpha_context.context) :=
  let parse_passable_ty_aux_with_ret {ret} := 'parse_passable_ty_aux_with_ret
    ret in
  let parse_any_ty_aux := 'parse_any_ty_aux in
  let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.parse_type_cycle
    in
  if stack_depth >i 10000 then
    Error_monad.error_value
      (Build_extensible "Typechecking_too_many_recursive_calls" unit tt)
  else
    let? '(node_value, name) :=
      match ret_value with
      | Don't_parse_entrypoints ⇒ return? (node_value, None)
      | Parse_entrypoints ⇒ Script_ir_annot.extract_entrypoint_annot node_value
      end in
    let _return (ctxt : Alpha_context.context) (ty : Script_typed_ir.ty)
      : ret × Alpha_context.context :=
      match ret_value with
      | Don't_parse_entrypoints ⇒
        cast (ret × Alpha_context.context) ((Ex_ty ty), ctxt)
      | Parse_entrypoints ⇒
        cast (ret × Alpha_context.context)
        (let at_node :=
          Option.map
            (fun (name : Alpha_context.Entrypoint.t) ⇒
              {| Script_typed_ir.entrypoint_info.name := name;
                Script_typed_ir.entrypoint_info.original_type_expr :=
                  node_value; |}) name in
        ((Ex_parameter_ty_and_entrypoints_node
          {|
            ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.arg_type
              := ty;
            ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.entrypoints
              :=
              {| Script_typed_ir.entrypoints_node.at_node := at_node;
                Script_typed_ir.entrypoints_node.nested :=
                  Script_typed_ir.Entrypoints_None; |}; |}), ctxt))
      end in
    match
      (node_value,
        match node_value with
        | Micheline.Prim loc_value Michelson_v1_primitives.T_big_map args annot
          ⇒ allow_lazy_storage
        | _ ⇒ false
        end,
        match node_value with
        |
          Micheline.Prim loc_value Michelson_v1_primitives.T_sapling_state
            (cons memo_size []) annot ⇒ allow_lazy_storage
        | _ ⇒ false
        end) with
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_unit [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.unit_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_int [] annot, _, _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.int_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_nat [] annot, _, _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.nat_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_string [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.string_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_bytes [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.bytes_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_mutez [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.mutez_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_bool [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.bool_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_key [] annot, _, _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.key_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_key_hash [] annot, _,
        _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.key_hash_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_chest_key [] annot, _,
        _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.chest_key_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_chest [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.chest_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_timestamp [] annot, _,
        _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.timestamp_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_address [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.address_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_tx_rollup_l2_address
        [] annot, _, _) ⇒
      if Alpha_context.Constants.tx_rollup_enable ctxt then
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        return? (_return ctxt Script_typed_ir.tx_rollup_l2_address_t)
      else
        Error_monad.error_value
          (Build_extensible "Tx_rollup_addresses_disabled"
            Alpha_context.Script.location loc_value)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_signature [] annot, _,
        _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.signature_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_operation [] annot, _,
        _) ⇒
      if allow_operation then
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        return? (_return ctxt Script_typed_ir.operation_t)
      else
        Error_monad.error_value
          (Build_extensible "Unexpected_operation" Alpha_context.Script.location
            loc_value)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_chain_id [] annot, _,
        _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.chain_id_t)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_never [] annot, _, _)
      ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.never_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_bls12_381_g1 [] annot,
        _, _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.bls12_381_g1_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_bls12_381_g2 [] annot,
        _, _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.bls12_381_g2_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_bls12_381_fr [] annot,
        _, _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      return? (_return ctxt Script_typed_ir.bls12_381_fr_t)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_contract (cons utl [])
        annot, _, _) ⇒
      if allow_contract then
        let? '(Ex_ty tl, ctxt) :=
          parse_passable_ty_aux_with_ret ctxt (stack_depth +i 1) legacy
            Don't_parse_entrypoints utl in
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        let? ty := Script_typed_ir.contract_t loc_value tl in
        return? (_return ctxt ty)
      else
        Error_monad.error_value
          (Build_extensible "Unexpected_contract" Alpha_context.Script.location
            loc_value)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_pair (cons utl utr)
        annot, _, _) ⇒
      let? utl := Script_ir_annot.remove_field_annot utl in
      let? '(Ex_ty tl, ctxt) :=
        parse_ty_aux ctxt (stack_depth +i 1) legacy allow_lazy_storage
          allow_operation allow_contract allow_ticket Don't_parse_entrypoints
          utl in
      let? utr :=
        match utr with
        | cons utr [] ⇒ Script_ir_annot.remove_field_annot utr
        | utr ⇒
          return?
            (Micheline.Prim loc_value Michelson_v1_primitives.T_pair utr nil)
        end in
      let? '(Ex_ty tr, ctxt) :=
        parse_ty_aux ctxt (stack_depth +i 1) legacy allow_lazy_storage
          allow_operation allow_contract allow_ticket Don't_parse_entrypoints
          utr in
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? 'Script_typed_ir.Ty_ex_c ty := Script_typed_ir.pair_t loc_value tl tr
        in
      return? (_return ctxt ty)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_or
        (cons utl (cons utr [])) annot, _, _) ⇒
      let? '(utl, utr) :=
        match ret_value with
        | Don't_parse_entrypoints ⇒
          let? utl := Script_ir_annot.remove_field_annot utl in
          let? utr := Script_ir_annot.remove_field_annot utr in
          return? (utl, utr)
        | Parse_entrypoints ⇒ return? (utl, utr)
        end in
      let? '(parsed_l, ctxt) :=
        parse_ty_aux ctxt (stack_depth +i 1) legacy allow_lazy_storage
          allow_operation allow_contract allow_ticket ret_value utl in
      let? '(parsed_r, ctxt) :=
        parse_ty_aux ctxt (stack_depth +i 1) legacy allow_lazy_storage
          allow_operation allow_contract allow_ticket ret_value utr in
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      match (ret_value, (parsed_l : ret), (parsed_r : ret)) with
      | (Don't_parse_entrypoints, parsed_l, parsed_r) ⇒
        let '[parsed_r, parsed_l] := cast [ex_ty ** ex_ty] [parsed_r, parsed_l]
          in
        cast (M? (ret × Alpha_context.context))
        (let 'Ex_ty tl := parsed_l in
        let 'Ex_ty tr := parsed_r in
        let? 'Script_typed_ir.Ty_ex_c ty :=
          Script_typed_ir.union_t loc_value tl tr in
        return? ((Ex_ty ty), ctxt))
      | (Parse_entrypoints, parsed_l, parsed_r) ⇒
        let '[parsed_r, parsed_l] :=
          cast
            [ex_parameter_ty_and_entrypoints_node **
              ex_parameter_ty_and_entrypoints_node] [parsed_r, parsed_l] in
        cast (M? (ret × Alpha_context.context))
        (let
          'Ex_parameter_ty_and_entrypoints_node {|
            ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.arg_type
              := tl;
              ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.entrypoints
                := _left
              |} := parsed_l in
        let
          'Ex_parameter_ty_and_entrypoints_node {|
            ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.arg_type
              := tr;
              ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.entrypoints
                := _right
              |} := parsed_r in
        let? 'Script_typed_ir.Ty_ex_c arg_type :=
          Script_typed_ir.union_t loc_value tl tr in
        let entrypoints :=
          let at_node :=
            Option.map
              (fun (name : Alpha_context.Entrypoint.t) ⇒
                {| Script_typed_ir.entrypoint_info.name := name;
                  Script_typed_ir.entrypoint_info.original_type_expr :=
                    node_value; |}) name in
          {| Script_typed_ir.entrypoints_node.at_node := at_node;
            Script_typed_ir.entrypoints_node.nested :=
              Script_typed_ir.Entrypoints_Union
                {|
                  Script_typed_ir.nested_entrypoints.Entrypoints_Union._left :=
                    _left;
                  Script_typed_ir.nested_entrypoints.Entrypoints_Union._right :=
                    _right; |}; |} in
        return?
          ((Ex_parameter_ty_and_entrypoints_node
            {|
              ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.arg_type
                := arg_type;
              ex_parameter_ty_and_entrypoints_node.Ex_parameter_ty_and_entrypoints_node.entrypoints
                := entrypoints; |}), ctxt))
      end
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_lambda
        (cons uta (cons utr [])) annot, _, _) ⇒
      let? '(Ex_ty ta, ctxt) :=
        parse_any_ty_aux ctxt (stack_depth +i 1) legacy uta in
      let? '(Ex_ty tr, ctxt) :=
        parse_any_ty_aux ctxt (stack_depth +i 1) legacy utr in
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? ty := Script_typed_ir.lambda_t loc_value ta tr in
      return? (_return ctxt ty)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_option (cons ut [])
        annot, _, _) ⇒
      let? ut :=
        if legacy then
          let? ut := Script_ir_annot.remove_field_annot ut in
          let? '_ := Script_ir_annot.check_composed_type_annot loc_value annot
            in
          return? ut
        else
          let? '_ := Script_ir_annot.check_type_annot loc_value annot in
          return? ut in
      let? '(Ex_ty t_value, ctxt) :=
        parse_ty_aux ctxt (stack_depth +i 1) legacy allow_lazy_storage
          allow_operation allow_contract allow_ticket Don't_parse_entrypoints ut
        in
      let? ty := Script_typed_ir.option_t loc_value t_value in
      return? (_return ctxt ty)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_list (cons ut [])
        annot, _, _) ⇒
      let? '(Ex_ty t_value, ctxt) :=
        parse_ty_aux ctxt (stack_depth +i 1) legacy allow_lazy_storage
          allow_operation allow_contract allow_ticket Don't_parse_entrypoints ut
        in
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? ty := Script_typed_ir.list_t loc_value t_value in
      return? (_return ctxt ty)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_ticket (cons ut [])
        annot, _, _) ⇒
      if allow_ticket then
        let? '(Ex_comparable_ty t_value, ctxt) :=
          parse_comparable_ty_aux (stack_depth +i 1) ctxt ut in
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        let? ty := Script_typed_ir.ticket_t loc_value t_value in
        return? (_return ctxt ty)
      else
        Error_monad.error_value
          (Build_extensible "Unexpected_ticket" Alpha_context.Script.location
            loc_value)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_set (cons ut []) annot,
        _, _) ⇒
      let? '(Ex_comparable_ty t_value, ctxt) :=
        parse_comparable_ty_aux (stack_depth +i 1) ctxt ut in
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? ty := Script_typed_ir.set_t loc_value t_value in
      return? (_return ctxt ty)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_map
        (cons uta (cons utr [])) annot, _, _) ⇒
      let? '(Ex_comparable_ty ta, ctxt) :=
        parse_comparable_ty_aux (stack_depth +i 1) ctxt uta in
      let? '(Ex_ty tr, ctxt) :=
        parse_ty_aux ctxt (stack_depth +i 1) legacy allow_lazy_storage
          allow_operation allow_contract allow_ticket Don't_parse_entrypoints
          utr in
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? ty := Script_typed_ir.map_t loc_value ta tr in
      return? (_return ctxt ty)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_sapling_transaction
        (cons memo_size []) annot, _, _) ⇒
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? memo_size := parse_memo_size memo_size in
      return? (_return ctxt (Script_typed_ir.sapling_transaction_t memo_size))
    |
      (Micheline.Prim loc_value
        Michelson_v1_primitives.T_sapling_transaction_deprecated
        (cons memo_size []) annot, _, _) ⇒
      if legacy then
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        let? memo_size := parse_memo_size memo_size in
        return?
          (_return ctxt
            (Script_typed_ir.sapling_transaction_deprecated_t memo_size))
      else
        Error_monad.error_value
          (Build_extensible "Deprecated_instruction" Alpha_context.Script.prim
            Michelson_v1_primitives.T_sapling_transaction_deprecated)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_big_map args annot,
        true, _) ⇒
      let? '(Ex_ty ty, ctxt) :=
        parse_big_map_ty ctxt (stack_depth +i 1) legacy loc_value args annot in
      return? (_return ctxt ty)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_sapling_state
        (cons memo_size [])