🍬 Script_ir_translator.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
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.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_comparable.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_annot.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
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_string.
Require TezosOfOCaml.Proto_alpha.Script_tc_context.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
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.Ticket_amount.
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.

Definition elab_conf : Set := Script_ir_translator_config.elab_config.

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

Inductive eq : Set :=
| Eq : eq.

Module cinstr.
  Record record : Set := Build {
    apply : 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 kinstr := instr.(cinstr.apply) (Script_typed_ir.IHalt loc_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 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 (k_value : Script_typed_ir.kinstr) ⇒
            d1.(descr.instr).(cinstr.apply)
              (d2.(descr.instr).(cinstr.apply) k_value); |}; |}.

Definition tc_context : Set := Tc_context.t.

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)).

Definition check_comparable
  (loc_value : Alpha_context.Script.location) (ty_value : Script_typed_ir.ty)
  : M? eq :=
  match Script_typed_ir.is_comparable ty_value with
  | Dependent_bool.Yes ⇒ return? Eq
  | Dependent_bool.No ⇒
    let t_value := Script_ir_unparser.serialize_ty_for_error ty_value in
    Error_monad.error_value
      (Build_extensible "Comparable_type_expected"
        (Alpha_context.Script.location × Alpha_context.Script.expr)
        (loc_value, t_value))
  end.

Definition pack_node {A : Set} (unparsed : Alpha_context.Script.expr) (ctxt : A)
  : bytes × A :=
  let bytes_value :=
    Data_encoding.Binary.to_bytes_exn None
      (Data_encoding.tup2 (Data_encoding.Fixed.string_value 1)
        Alpha_context.Script.expr_encoding) ((String.String "005" ""), unparsed)
    in
  (bytes_value, ctxt).

Definition pack_comparable_data {A : Set}
  (ctxt : Alpha_context.context) (ty_value : Script_typed_ir.comparable_ty)
  (data : A) : M? (bytes × Alpha_context.context) :=
  let? '(unparsed, ctxt) :=
    Script_ir_unparser.unparse_comparable_data ctxt
      Script_ir_unparser.Optimized_legacy ty_value data in
  return? (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_value : Script_typed_ir.comparable_ty)
  (data : A) : M? (Script_expr_hash.t × Alpha_context.context) :=
  let? '(bytes_value, ctxt) := pack_comparable_data ctxt ty_value data 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_value : Script_typed_ir.ty) : M? Alpha_context.context :=
  let fix aux
    (loc_value : Alpha_context.Script.location) (ty_value : 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_value 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_value _ _ ⇒ aux loc_value ty_value
        | Script_typed_ir.List_t ty_value _ ⇒ aux loc_value ty_value
        | 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_value 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.

Definition type_metadata_eq {A error_trace : Set}
  (error_details : Script_tc_errors.error_details A)
  (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
  (loc_value : Alpha_context.Script.location) (ty1 : Script_typed_ir.ty)
  (ty2 : Script_typed_ir.ty) : Error_monad._error :=
  let ty1 := Script_ir_unparser.serialize_ty_for_error ty1 in
  let ty2 := Script_ir_unparser.serialize_ty_for_error ty2 in
  Build_extensible "Inconsistent_types"
    (Alpha_context.Script.location × Alpha_context.Script.expr ×
      Alpha_context.Script.expr) (loc_value, ty1, ty2).

Definition memo_size_eq {A error_trace : Set}
  (error_details : Script_tc_errors.error_details A)
  (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.

Fixpoint ty_eq {error_trace : Set}
  (error_details : Script_tc_errors.error_details 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 (loc_value : Alpha_context.Script.location) ⇒
        default_ty_eq_error 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 help (ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.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 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 loc_value ⇒
                let loc_value := cast Alpha_context.Script.location loc_value in
                cast error_trace
                (Error_monad.trace_of_error
                  (default_ty_eq_error loc_value ty1 ty2))
              end) in
        Gas_monad.record_trace_eval error_details
          (fun (loc_value : Alpha_context.Script.location) ⇒
            default_ty_eq_error loc_value ty1 ty2)
          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 (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 (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 (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 (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 (loc_value : Alpha_context.Script.location) ⇒
      default_ty_eq_error loc_value ty1 ty2) (help 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 := Script_ir_unparser.serialize_stack_for_error ctxt aftbt in
      let aftbf := Script_ir_unparser.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 memo_size ⇒ Pervasives.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.

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_node].

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

#[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? 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_value : Script_typed_ir.ty)
      : ret × Alpha_context.context :=
      match (ret_value, name) with
      | (Don't_parse_entrypoints, _) ⇒
        cast (ret × Alpha_context.context)
        ((Script_typed_ir.Ex_ty ty_value), ctxt)
      | (Parse_entrypoints, name) ⇒
        let name := cast (option Alpha_context.Entrypoint.t) name in
        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_value;
            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, _,
        _) ⇒
      if legacy then
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        return? (_return ctxt Script_typed_ir.chest_key_t)
      else
        Error_monad.error_value
          (Build_extensible "Deprecated_instruction" Alpha_context.Script.prim
            Michelson_v1_primitives.T_chest_key)
    | (Micheline.Prim loc_value Michelson_v1_primitives.T_chest [] annot, _, _)
      ⇒
      if legacy then
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        return? (_return ctxt Script_typed_ir.chest_t)
      else
        Error_monad.error_value
          (Build_extensible "Deprecated_instruction" Alpha_context.Script.prim
            Michelson_v1_primitives.T_chest)
    |
      (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? '(Script_typed_ir.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_value := Script_typed_ir.contract_t loc_value tl in
        return? (_return ctxt ty_value)
      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? '(Script_typed_ir.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? '(Script_typed_ir.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_value :=
        Script_typed_ir.pair_t loc_value tl tr in
      return? (_return ctxt ty_value)
    |
      (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, parsed_r, name) with
      | (Don't_parse_entrypoints, _, _, _) ⇒
        cast (M? (ret × Alpha_context.context))
        (let 'Script_typed_ir.Ex_ty tl := parsed_l in
        let 'Script_typed_ir.Ex_ty tr := parsed_r in
        let? 'Script_typed_ir.Ty_ex_c ty_value :=
          Script_typed_ir.union_t loc_value tl tr in
        return? ((Script_typed_ir.Ex_ty ty_value), ctxt))
      | (Parse_entrypoints, parsed_l, parsed_r, name) ⇒
        let '[name, parsed_r, parsed_l] :=
          cast
            [option Alpha_context.Entrypoint.t **
              ex_parameter_ty_and_entrypoints_node **
              ex_parameter_ty_and_entrypoints_node] [name, 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? '(Script_typed_ir.Ex_ty ta, ctxt) :=
        parse_any_ty_aux ctxt (stack_depth +i 1) legacy uta in
      let? '(Script_typed_ir.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_value := Script_typed_ir.lambda_t loc_value ta tr in
      return? (_return ctxt ty_value)
    |
      (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? '(Script_typed_ir.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_value := Script_typed_ir.option_t loc_value t_value in
      return? (_return ctxt ty_value)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_list (cons ut [])
        annot, _, _) ⇒
      let? '(Script_typed_ir.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_value := Script_typed_ir.list_t loc_value t_value in
      return? (_return ctxt ty_value)
    |
      (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 ctxt (stack_depth +i 1) ut in
        let? '_ := Script_ir_annot.check_type_annot loc_value annot in
        let? ty_value := Script_typed_ir.ticket_t loc_value t_value in
        return? (_return ctxt ty_value)
      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 ctxt (stack_depth +i 1) ut in
      let? '_ := Script_ir_annot.check_type_annot loc_value annot in
      let? ty_value := Script_typed_ir.set_t loc_value t_value in
      return? (_return ctxt ty_value)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_map
        (cons uta (cons utr [])) annot, _, _) ⇒
      let? '(Ex_comparable_ty ta, ctxt) :=
        parse_comparable_ty_aux ctxt (stack_depth +i 1) uta in
      let? '(Script_typed_ir.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_value := Script_typed_ir.map_t loc_value ta tr in
      return? (_return ctxt ty_value)
    |
      (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? '(Script_typed_ir.Ex_ty ty_value, ctxt) :=
        parse_big_map_ty ctxt (stack_depth +i 1) legacy loc_value args annot in
      return? (_return ctxt ty_value)
    |
      (Micheline.Prim loc_value Michelson_v1_primitives.T_sapling_state
        (cons memo_size []) annot, _, true) ⇒
      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_state_t memo_size))
    |
      (Micheline.Prim loc_value
        (Michelson_v1_primitives.T_big_map |
        Michelson_v1_primitives.T_sapling_state) _ _, _, _) ⇒
      Error_monad.error_value
        (Build_extensible "Unexpected_lazy_storage"
          Alpha_context.Script.location loc_value)
    |
      (Micheline.Prim loc_value
        ((Michelson_v1_primitives.T_unit | Michelson_v1_primitives.T_signature |
        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 | Michelson_v1_primitives.T_key_hash |
        Michelson_v1_primitives.T_timestamp | Michelson_v1_primitives.T_address
        | Michelson_v1_primitives.T_tx_rollup_l2_address |
        Michelson_v1_primitives.T_chain_id | Michelson_v1_primitives.T_operation
        | Michelson_v1_primitives.T_never) 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_set | Michelson_v1_primitives.T_list |
        Michelson_v1_primitives.T_option | Michelson_v1_primitives.T_contract |
        Michelson_v1_primitives.T_ticket) 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, 1, (List.length l_value)))
    |
      (Micheline.Prim loc_value
        ((Michelson_v1_primitives.T_pair | Michelson_v1_primitives.T_or |
        Michelson_v1_primitives.T_map | Michelson_v1_primitives.T_lambda) 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)))
    | (expr, _, _) ⇒
      Error_monad.error_value
        (unexpected expr nil Michelson_v1_primitives.Type_namespace
          [
            Michelson_v1_primitives.T_bls12_381_fr;
            Michelson_v1_primitives.T_bls12_381_g1;
            Michelson_v1_primitives.T_bls12_381_g2;
            Michelson_v1_primitives.T_bool;
            Michelson_v1_primitives.T_bytes;
            Michelson_v1_primitives.T_chain_id;
            Michelson_v1_primitives.T_contract;
            Michelson_v1_primitives.T_int;
            Michelson_v1_primitives.T_key;
            Michelson_v1_primitives.T_key_hash;
            Michelson_v1_primitives.T_lambda;
            Michelson_v1_primitives.T_list;
            Michelson_v1_primitives.T_map;
            Michelson_v1_primitives.T_mutez;
            Michelson_v1_primitives.T_nat;
            Michelson_v1_primitives.T_never;
            Michelson_v1_primitives.T_operation;
            Michelson_v1_primitives.T_option;
            Michelson_v1_primitives.T_or;
            Michelson_v1_primitives.T_pair;
            Michelson_v1_primitives.T_set;
            Michelson_v1_primitives.T_signature;
            Michelson_v1_primitives.T_string;
            Michelson_v1_primitives.T_ticket;
            Michelson_v1_primitives.T_timestamp;
            Michelson_v1_primitives.T_tx_rollup_l2_address;
            Michelson_v1_primitives.T_unit
          ])
    end

with parse_comparable_ty_aux
  (ctxt : Alpha_context.context) (stack_depth : int)
  (node_value : Alpha_context.Script.node) {struct stack_depth}
  : M? (ex_comparable_ty × Alpha_context.context) :=
  let? '(Script_typed_ir.Ex_ty t_value, ctxt) :=
    parse_ty_aux ctxt (stack_depth +i 1) false false false false false
      Don't_parse_entrypoints node_value in
  match Script_typed_ir.is_comparable t_value with
  | Dependent_bool.Yes ⇒ return? ((Ex_comparable_ty t_value), ctxt)
  | Dependent_bool.No ⇒
    Error_monad.error_value
      (Build_extensible "Comparable_type_expected"
        (Alpha_context.Script.location ×
          Micheline.canonical Alpha_context.Script.prim)
        ((location node_value), (Micheline.strip_locations node_value)))
  end

with parse_passable_ty_aux_with_ret {ret : Set}
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  {struct stack_depth}
  : parse_ty_ret → Alpha_context.Script.node →
  M? (ret × Alpha_context.context) :=
  parse_ty_aux ctxt stack_depth legacy true false true true

with parse_any_ty_aux
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  {struct stack_depth}
  : Alpha_context.Script.node →
  M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  parse_ty_aux ctxt stack_depth legacy true true true true
    Don't_parse_entrypoints

with parse_big_map_ty
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (big_map_loc : Alpha_context.Script.location)
  (args :
    list
      (Micheline.node Alpha_context.Script.location Alpha_context.Script.prim))
  (map_annot : Micheline.annot) {struct args}
  : M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.parse_type_cycle
    in
  match args with
  | cons key_ty (cons value_ty []) ⇒
    let? '(Ex_comparable_ty key_ty, ctxt) :=
      parse_comparable_ty_aux ctxt (stack_depth +i 1) key_ty in
    let? '(Script_typed_ir.Ex_ty value_ty, ctxt) :=
      parse_big_map_value_ty_aux ctxt (stack_depth +i 1) legacy value_ty in
    let? '_ := Script_ir_annot.check_type_annot big_map_loc map_annot in
    let? big_map_ty := Script_typed_ir.big_map_t big_map_loc key_ty value_ty in
    return? ((Script_typed_ir.Ex_ty big_map_ty), ctxt)
  | args ⇒
    Error_monad.error_value
      (Build_extensible "Invalid_arity"
        (Alpha_context.Script.location × Alpha_context.Script.prim × int × int)
        (big_map_loc, Michelson_v1_primitives.T_big_map, 2, (List.length args)))
  end

with parse_big_map_value_ty_aux
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (value_ty :
    Micheline.node Alpha_context.Script.location Alpha_context.Script.prim)
  {struct stack_depth} : M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  parse_ty_aux ctxt stack_depth legacy false false legacy true
    Don't_parse_entrypoints value_ty.

Definition parse_packable_ty_aux
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (node_value : Alpha_context.Script.node)
  : M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  parse_ty_aux ctxt stack_depth legacy false false legacy false
    Don't_parse_entrypoints node_value.

Definition parse_view_input_ty
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (node_value : Alpha_context.Script.node)
  : M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  parse_ty_aux ctxt stack_depth legacy false false true false
    Don't_parse_entrypoints node_value.

Definition parse_view_output_ty
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (node_value : Alpha_context.Script.node)
  : M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  parse_ty_aux ctxt stack_depth legacy false false true false
    Don't_parse_entrypoints node_value.

Definition parse_normal_storage_ty
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (node_value : Alpha_context.Script.node)
  : M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  parse_ty_aux ctxt stack_depth legacy true false legacy true
    Don't_parse_entrypoints node_value.

Definition parse_storage_ty
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (node_value : Alpha_context.Script.node)
  : M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  match
    (node_value,
      match node_value with
      |
        Micheline.Prim loc_value Michelson_v1_primitives.T_pair
          (cons
            (Micheline.Prim big_map_loc Michelson_v1_primitives.T_big_map args
              map_annot) (cons remaining_storage [])) storage_annot ⇒ legacy
      | _ ⇒ false
      end) with
  |
    (Micheline.Prim loc_value Michelson_v1_primitives.T_pair
      (cons
        (Micheline.Prim big_map_loc Michelson_v1_primitives.T_big_map args
          map_annot) (cons remaining_storage [])) storage_annot, true) ⇒
    match
      (storage_annot,
        match storage_annot with
        | cons single [] ⇒
          ((String.length single) >i 0) &&
          (Compare.Char.(Compare.S.op_eq) (String.get single 0) "%" % char)
        | _ ⇒ false
        end) with
    | ([], _) ⇒ parse_normal_storage_ty ctxt stack_depth legacy node_value
    | (cons single [], true) ⇒
      parse_normal_storage_ty ctxt stack_depth legacy node_value
    | (_, _) ⇒
      let? ctxt :=
        Alpha_context.Gas.consume ctxt Typecheck_costs.parse_type_cycle in
      let? '(Script_typed_ir.Ex_ty big_map_ty, ctxt) :=
        parse_big_map_ty ctxt (stack_depth +i 1) legacy big_map_loc args
          map_annot in
      let? '(Script_typed_ir.Ex_ty remaining_storage, ctxt) :=
        parse_normal_storage_ty ctxt (stack_depth +i 1) legacy remaining_storage
        in
      let? '_ :=
        Script_ir_annot.check_composed_type_annot loc_value storage_annot in
      let? 'Script_typed_ir.Ty_ex_c ty_value :=
        Script_typed_ir.pair_t loc_value big_map_ty remaining_storage in
      return? ((Script_typed_ir.Ex_ty ty_value), ctxt)
    end
  | (_, _) ⇒ parse_normal_storage_ty ctxt stack_depth legacy node_value
  end.

Definition check_packable
  (legacy : bool) (loc_value : Alpha_context.Script.location)
  (root_value : Script_typed_ir.ty) : M? unit :=
  let fix check (function_parameter : Script_typed_ir.ty) : M? unit :=
    match
      (function_parameter,
        match function_parameter with
        | Script_typed_ir.Contract_t _ _ ⇒ legacy
        | _ ⇒ false
        end) with
    | (Script_typed_ir.Big_map_t _ _ _, _) ⇒
      Error_monad.error_value
        (Build_extensible "Unexpected_lazy_storage"
          Alpha_context.Script.location loc_value)
    | (Script_typed_ir.Sapling_state_t _, _) ⇒
      Error_monad.error_value
        (Build_extensible "Unexpected_lazy_storage"
          Alpha_context.Script.location loc_value)
    | (Script_typed_ir.Operation_t, _) ⇒
      Error_monad.error_value
        (Build_extensible "Unexpected_operation" Alpha_context.Script.location
          loc_value)
    | (Script_typed_ir.Unit_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Int_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Nat_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Signature_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.String_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Bytes_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Mutez_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Key_hash_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Key_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Timestamp_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Address_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Tx_rollup_l2_address_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Bool_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Chain_id_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Never_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Set_t _ _, _) ⇒ Result.return_unit
    | (Script_typed_ir.Ticket_t _ _, _) ⇒
      Error_monad.error_value
        (Build_extensible "Unexpected_ticket" Alpha_context.Script.location
          loc_value)
    | (Script_typed_ir.Lambda_t _ _ _, _) ⇒ Result.return_unit
    | (Script_typed_ir.Bls12_381_g1_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Bls12_381_g2_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Bls12_381_fr_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Pair_t l_ty r_ty _ _, _) ⇒
      let? '_ := check l_ty in
      check r_ty
    | (Script_typed_ir.Union_t l_ty r_ty _ _, _) ⇒
      let? '_ := check l_ty in
      check r_ty
    | (Script_typed_ir.Option_t v_ty _ _, _) ⇒ check v_ty
    | (Script_typed_ir.List_t elt_ty _, _) ⇒ check elt_ty
    | (Script_typed_ir.Map_t _ elt_ty _, _) ⇒ check elt_ty
    | (Script_typed_ir.Contract_t _ _, true) ⇒ Result.return_unit
    | (Script_typed_ir.Contract_t _ _, _) ⇒
      Error_monad.error_value
        (Build_extensible "Unexpected_contract" Alpha_context.Script.location
          loc_value)
    | (Script_typed_ir.Sapling_transaction_t _, _) ⇒ return? tt
    | (Script_typed_ir.Sapling_transaction_deprecated_t _, _) ⇒ return? tt
    | (Script_typed_ir.Chest_key_t, _) ⇒ Result.return_unit
    | (Script_typed_ir.Chest_t, _) ⇒ Result.return_unit
    end in
  check root_value.

Module toplevel.
  Record record : Set := Build {
    code_field : Alpha_context.Script.node;
    arg_type : Alpha_context.Script.node;
    storage_type : Alpha_context.Script.node;
    views : Script_typed_ir.view_map;
  }.
  Definition with_code_field code_field (r : record) :=
    Build code_field r.(arg_type) r.(storage_type) r.(views).
  Definition with_arg_type arg_type (r : record) :=
    Build r.(code_field) arg_type r.(storage_type) r.(views).
  Definition with_storage_type storage_type (r : record) :=
    Build r.(code_field) r.(arg_type) storage_type r.(views).
  Definition with_views views (r : record) :=
    Build r.(code_field) r.(arg_type) r.(storage_type) views.
End toplevel.
Definition toplevel := toplevel.record.

Records for the constructor parameters

Module ConstructorRecords_code.
  Module code.
    Module Code.
      Record record {code arg_type storage_type views entrypoints code_size :
        Set} : Set := Build {
        code : code;
        arg_type : arg_type;
        storage_type : storage_type;
        views : views;
        entrypoints : entrypoints;
        code_size : code_size;
      }.
      Arguments record : clear implicits.
      Definition with_code
        {t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size}
        code
        (r :
          record t_code t_arg_type t_storage_type t_views t_entrypoints
            t_code_size) :=
        Build t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size
          code r.(arg_type) r.(storage_type) r.(views) r.(entrypoints)
          r.(code_size).
      Definition with_arg_type
        {t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size}
        arg_type
        (r :
          record t_code t_arg_type t_storage_type t_views t_entrypoints
            t_code_size) :=
        Build t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size
          r.(code) arg_type r.(storage_type) r.(views) r.(entrypoints)
          r.(code_size).
      Definition with_storage_type
        {t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size}
        storage_type
        (r :
          record t_code t_arg_type t_storage_type t_views t_entrypoints
            t_code_size) :=
        Build t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size
          r.(code) r.(arg_type) storage_type r.(views) r.(entrypoints)
          r.(code_size).
      Definition with_views
        {t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size}
        views
        (r :
          record t_code t_arg_type t_storage_type t_views t_entrypoints
            t_code_size) :=
        Build t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size
          r.(code) r.(arg_type) r.(storage_type) views r.(entrypoints)
          r.(code_size).
      Definition with_entrypoints
        {t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size}
        entrypoints
        (r :
          record t_code t_arg_type t_storage_type t_views t_entrypoints
            t_code_size) :=
        Build t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size
          r.(code) r.(arg_type) r.(storage_type) r.(views) entrypoints
          r.(code_size).
      Definition with_code_size
        {t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size}
        code_size
        (r :
          record t_code t_arg_type t_storage_type t_views t_entrypoints
            t_code_size) :=
        Build t_code t_arg_type t_storage_type t_views t_entrypoints t_code_size
          r.(code) r.(arg_type) r.(storage_type) r.(views) r.(entrypoints)
          code_size.
    End Code.
    Definition Code_skeleton := Code.record.
  End code.
End ConstructorRecords_code.
Import ConstructorRecords_code.

Reserved Notation "'code.Code".

Inductive code : Set :=
| Code : 'code.Code → code

where "'code.Code" :=
  (code.Code_skeleton Script_typed_ir.lambda Script_typed_ir.ty
    Script_typed_ir.ty Script_typed_ir.view_map Script_typed_ir.entrypoints
    Cache_memory_helpers.sint).

Module code.
  Include ConstructorRecords_code.code.
  Definition Code := 'code.Code.
End code.

Inductive ex_script : Set :=
| Ex_script : ∀ {c : Set}, Script_typed_ir.script c → ex_script.

Inductive ex_code : Set :=
| Ex_code : code → ex_code.

Records for the constructor parameters

Module ConstructorRecords_typed_view.
  Module typed_view.
    Module Typed_view.
      Record record {input_ty output_ty kinstr original_code_expr : Set} : Set := Build {
        input_ty : input_ty;
        output_ty : output_ty;
        kinstr : kinstr;
        original_code_expr : original_code_expr;
      }.
      Arguments record : clear implicits.
      Definition with_input_ty
        {t_input_ty t_output_ty t_kinstr t_original_code_expr} input_ty
        (r : record t_input_ty t_output_ty t_kinstr t_original_code_expr) :=
        Build t_input_ty t_output_ty t_kinstr t_original_code_expr input_ty
          r.(output_ty) r.(kinstr) r.(original_code_expr).
      Definition with_output_ty
        {t_input_ty t_output_ty t_kinstr t_original_code_expr} output_ty
        (r : record t_input_ty t_output_ty t_kinstr t_original_code_expr) :=
        Build t_input_ty t_output_ty t_kinstr t_original_code_expr r.(input_ty)
          output_ty r.(kinstr) r.(original_code_expr).
      Definition with_kinstr
        {t_input_ty t_output_ty t_kinstr t_original_code_expr} kinstr
        (r : record t_input_ty t_output_ty t_kinstr t_original_code_expr) :=
        Build t_input_ty t_output_ty t_kinstr t_original_code_expr r.(input_ty)
          r.(output_ty) kinstr r.(original_code_expr).
      Definition with_original_code_expr
        {t_input_ty t_output_ty t_kinstr t_original_code_expr}
        original_code_expr
        (r : record t_input_ty t_output_ty t_kinstr t_original_code_expr) :=
        Build t_input_ty t_output_ty t_kinstr t_original_code_expr r.(input_ty)
          r.(output_ty) r.(kinstr) original_code_expr.
    End Typed_view.
    Definition Typed_view_skeleton := Typed_view.record.
  End typed_view.
End ConstructorRecords_typed_view.
Import ConstructorRecords_typed_view.

Reserved Notation "'typed_view.Typed_view".

Inductive typed_view : Set :=
| Typed_view : 'typed_view.Typed_view → typed_view

where "'typed_view.Typed_view" :=
  (typed_view.Typed_view_skeleton Script_typed_ir.ty Script_typed_ir.ty
    Script_typed_ir.kinstr Alpha_context.Script.node).

Module typed_view.
  Include ConstructorRecords_typed_view.typed_view.
  Definition Typed_view := 'typed_view.Typed_view.
End typed_view.

Definition typed_view_map : Set :=
  Script_typed_ir.map Script_string.t typed_view.

Inductive dig_proof_argument : Set :=
| Dig_proof_argument :
  Script_typed_ir.stack_prefix_preservation_witness → Script_typed_ir.ty →
  Script_typed_ir.stack_ty → dig_proof_argument.

Inductive dug_proof_argument : Set :=
| Dug_proof_argument :
  Script_typed_ir.stack_prefix_preservation_witness × Script_typed_ir.stack_ty
  → dug_proof_argument.

Inductive dipn_proof_argument : Set :=
| Dipn_proof_argument :
  Script_typed_ir.stack_prefix_preservation_witness → Alpha_context.context →
  descr → Script_typed_ir.stack_ty → dipn_proof_argument.

Inductive dropn_proof_argument : Set :=
| Dropn_proof_argument :
  Script_typed_ir.stack_prefix_preservation_witness →
  Script_typed_ir.stack_ty → dropn_proof_argument.

Inductive comb_proof_argument : Set :=
| Comb_proof_argument :
  Script_typed_ir.comb_gadt_witness → Script_typed_ir.stack_ty →
  comb_proof_argument.

Inductive uncomb_proof_argument : Set :=
| Uncomb_proof_argument :
  Script_typed_ir.uncomb_gadt_witness → Script_typed_ir.stack_ty →
  uncomb_proof_argument.

Inductive comb_get_proof_argument : Set :=
| Comb_get_proof_argument :
  Script_typed_ir.comb_get_gadt_witness → Script_typed_ir.ty →
  comb_get_proof_argument.

Inductive comb_set_proof_argument : Set :=
| Comb_set_proof_argument :
  Script_typed_ir.comb_set_gadt_witness → Script_typed_ir.ty →
  comb_set_proof_argument.

Inductive dup_n_proof_argument : Set :=
| Dup_n_proof_argument :
  Script_typed_ir.dup_n_gadt_witness → Script_typed_ir.ty →
  dup_n_proof_argument.

Fixpoint make_dug_proof_argument
  (loc_value : Alpha_context.Script.location) (n_value : int)
  (x_value : Script_typed_ir.ty) (stk : Script_typed_ir.stack_ty)
  : option dug_proof_argument :=
  match (n_value, stk) with
  | (0, rest) ⇒
    Some
      (Dug_proof_argument
        (Script_typed_ir.KRest, (Script_typed_ir.Item_t x_value rest)))
  | (n_value, Script_typed_ir.Item_t v_value rest) ⇒
    Option.map
      (fun (function_parameter : dug_proof_argument) ⇒
        let 'Dug_proof_argument (n', aft') := function_parameter in
        Dug_proof_argument
          ((Script_typed_ir.KPrefix loc_value v_value n'),
            (Script_typed_ir.Item_t v_value aft')))
      (make_dug_proof_argument loc_value (n_value -i 1) x_value rest)
  | (_, _) ⇒ None
  end.

Fixpoint make_comb_get_proof_argument
  (n_value : int) (ty_value : Script_typed_ir.ty)
  : option comb_get_proof_argument :=
  match (n_value, ty_value) with
  | (0, value_ty) ⇒
    Some (Comb_get_proof_argument Script_typed_ir.Comb_get_zero value_ty)
  | (1, Script_typed_ir.Pair_t hd_ty _ _annot _) ⇒
    Some (Comb_get_proof_argument Script_typed_ir.Comb_get_one hd_ty)
  | (n_value, Script_typed_ir.Pair_t _ tl_ty _annot _) ⇒
    Option.map
      (fun (function_parameter : comb_get_proof_argument) ⇒
        let 'Comb_get_proof_argument comb_get_left_witness ty' :=
          function_parameter in
        Comb_get_proof_argument
          (Script_typed_ir.Comb_get_plus_two comb_get_left_witness) ty')
      (make_comb_get_proof_argument (n_value -i 2) tl_ty)
  | _ ⇒ None
  end.

Fixpoint make_comb_set_proof_argument
  (ctxt : Alpha_context.context) (stack_ty : Script_typed_ir.stack_ty)
  (loc_value : Alpha_context.Script.location) (n_value : int)
  (value_ty : Script_typed_ir.ty) (ty_value : Script_typed_ir.ty)
  : M? comb_set_proof_argument :=
  match (n_value, ty_value) with
  | (0, _) ⇒
    return? (Comb_set_proof_argument Script_typed_ir.Comb_set_zero value_ty)
  | (1, Script_typed_ir.Pair_t _hd_ty tl_ty _ _) ⇒
    let? 'Script_typed_ir.Ty_ex_c after_ty :=
      Script_typed_ir.pair_t loc_value value_ty tl_ty in
    return? (Comb_set_proof_argument Script_typed_ir.Comb_set_one after_ty)
  | (n_value, Script_typed_ir.Pair_t hd_ty tl_ty _ _) ⇒
    let? 'Comb_set_proof_argument comb_set_left_witness tl_ty' :=
      make_comb_set_proof_argument ctxt stack_ty loc_value (n_value -i 2)
        value_ty tl_ty in
    let? 'Script_typed_ir.Ty_ex_c after_ty :=
      Script_typed_ir.pair_t loc_value hd_ty tl_ty' in
    return?
      (Comb_set_proof_argument
        (Script_typed_ir.Comb_set_plus_two comb_set_left_witness) after_ty)
  | _ ⇒
    let whole_stack :=
      Script_ir_unparser.serialize_stack_for_error ctxt stack_ty in
    Error_monad.error_value
      (Build_extensible "Bad_stack"
        (Alpha_context.Script.location × Alpha_context.Script.prim × int ×
          Script_tc_errors.unparsed_stack_ty)
        (loc_value, Michelson_v1_primitives.I_UPDATE, 2, whole_stack))
  end.

Records for the constructor parameters

Module ConstructorRecords_ex_ty_cstr.
  Module ex_ty_cstr.
    Module Ex_ty_cstr.
      Record record {ty construct original_type_expr : Set} : Set := Build {
        ty : ty;
        construct : construct;
        original_type_expr : original_type_expr;
      }.
      Arguments record : clear implicits.
      Definition with_ty {t_ty t_construct t_original_type_expr} ty
        (r : record t_ty t_construct t_original_type_expr) :=
        Build t_ty t_construct t_original_type_expr ty r.(construct)
          r.(original_type_expr).
      Definition with_construct {t_ty t_construct t_original_type_expr}
        construct (r : record t_ty t_construct t_original_type_expr) :=
        Build t_ty t_construct t_original_type_expr r.(ty) construct
          r.(original_type_expr).
      Definition with_original_type_expr {t_ty t_construct t_original_type_expr}
        original_type_expr (r : record t_ty t_construct t_original_type_expr) :=
        Build t_ty t_construct t_original_type_expr r.(ty) r.(construct)
          original_type_expr.
    End Ex_ty_cstr.
    Definition Ex_ty_cstr_skeleton := Ex_ty_cstr.record.
  End ex_ty_cstr.
End ConstructorRecords_ex_ty_cstr.
Import ConstructorRecords_ex_ty_cstr.

Reserved Notation "'ex_ty_cstr.Ex_ty_cstr".

Inductive ex_ty_cstr (a : Set) : Set :=
| Ex_ty_cstr : ∀ {b : Set}, 'ex_ty_cstr.Ex_ty_cstr a b → ex_ty_cstr a

where "'ex_ty_cstr.Ex_ty_cstr" :=
  (fun (t_a t_b : Set) ⇒ ex_ty_cstr.Ex_ty_cstr_skeleton Script_typed_ir.ty
    (t_b → t_a) Alpha_context.Script.node).

Module ex_ty_cstr.
  Include ConstructorRecords_ex_ty_cstr.ex_ty_cstr.
  Definition Ex_ty_cstr := 'ex_ty_cstr.Ex_ty_cstr.
End ex_ty_cstr.

Arguments Ex_ty_cstr {_ _}.

#[bypass_check(guard)]
Definition find_entrypoint {error_context full error_trace : Set}
  (error_details : Script_tc_errors.error_details error_context)
  (full_value : Script_typed_ir.ty) (entrypoints : Script_typed_ir.entrypoints)
  (entrypoint : Alpha_context.Entrypoint.t)
  : Gas_monad.t (ex_ty_cstr full) error_trace :=
  let fix find_entrypoint {t : Set}
    (ty_value : Script_typed_ir.ty)
    (entrypoints : Script_typed_ir.entrypoints_node)
    (entrypoint : Alpha_context.Entrypoint.t) {struct ty_value}
    : Gas_monad.t (ex_ty_cstr t) unit :=
    Gas_monad.Syntax.op_letstar
      (Gas_monad.consume_gas Typecheck_costs.find_entrypoint_cycle)
      (fun function_parameter ⇒
        let '_ := function_parameter in
        match
          ((ty_value, entrypoints),
            match (ty_value, entrypoints) with
            |
              (_, {|
                Script_typed_ir.entrypoints_node.at_node :=
                  Some {|
                    Script_typed_ir.entrypoint_info.name := name;
                      Script_typed_ir.entrypoint_info.original_type_expr
                        :=
                        original_type_expr
                      |}
                  |}) ⇒ Alpha_context.Entrypoint.op_eq name entrypoint
            | _ ⇒ false
            end) with
        |
          ((_, {|
            Script_typed_ir.entrypoints_node.at_node :=
              Some {|
                Script_typed_ir.entrypoint_info.name := name;
                  Script_typed_ir.entrypoint_info.original_type_expr
                    :=
                    original_type_expr
                  |}
              |}), true) ⇒
          let '[original_type_expr, name] :=
            cast [Alpha_context.Script.node ** Alpha_context.Entrypoint.t]
              [original_type_expr, name] in
          Gas_monad.Syntax._return
            (Ex_ty_cstr
              {| ex_ty_cstr.Ex_ty_cstr.ty := ty_value;
                ex_ty_cstr.Ex_ty_cstr.construct := fun (e_value : t) ⇒ e_value;
                ex_ty_cstr.Ex_ty_cstr.original_type_expr := original_type_expr;
                |})
        |
          ((Script_typed_ir.Union_t tl tr _ _, {|
            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
                  |}
              |}), _) ⇒
          let 'existT _ [__1, __0] [_right, _left, tr, tl] :=
            cast_exists (Es := [Set ** Set])
              (fun '[__1, __0] ⇒
                [Script_typed_ir.entrypoints_node **
                  Script_typed_ir.entrypoints_node ** Script_typed_ir.ty **
                  Script_typed_ir.ty]) [_right, _left, tr, tl] in
          cast (Gas_monad.t (ex_ty_cstr t) unit)
            (Gas_monad.bind_recover (find_entrypoint tl _left entrypoint)
              (fun (function_parameter :
                Pervasives.result (ex_ty_cstr __0) unit) ⇒
                match function_parameter with
                |
                  Pervasives.Ok
                    (Ex_ty_cstr {|
                      ex_ty_cstr.Ex_ty_cstr.ty := ty_value;
                        ex_ty_cstr.Ex_ty_cstr.construct := construct;
                        ex_ty_cstr.Ex_ty_cstr.original_type_expr :=
                          original_type_expr
                        |}) ⇒
                  let 'existT _ __Ex_ty_cstr_'b
                    [original_type_expr, construct, ty_value] :=
                    cast_exists (Es := Set)
                      (fun __Ex_ty_cstr_'b ⇒
                        [Alpha_context.Script.node ** __Ex_ty_cstr_'b → __0 **
                          Script_typed_ir.ty])
                      [original_type_expr, construct, ty_value] in
                  Gas_monad.Syntax._return
                    (Ex_ty_cstr
                      {| ex_ty_cstr.Ex_ty_cstr.ty := ty_value;
                        ex_ty_cstr.Ex_ty_cstr.construct :=
                          fun (e_value : __Ex_ty_cstr_'b) ⇒
                            Script_typed_ir.L (construct e_value);
                        ex_ty_cstr.Ex_ty_cstr.original_type_expr :=
                          original_type_expr; |})
                | Pervasives.Error _ ⇒
                  Gas_monad.Syntax.op_letplus
                    ((find_entrypoint tr _right entrypoint) :
                      Gas_monad.t (ex_ty_cstr __1) unit)
                    (fun x_value ⇒
                      let
                        'Ex_ty_cstr {|
                          ex_ty_cstr.Ex_ty_cstr.ty := ty_value;
                            ex_ty_cstr.Ex_ty_cstr.construct := construct;
                            ex_ty_cstr.Ex_ty_cstr.original_type_expr :=
                              original_type_expr
                            |} := x_value in
                      let 'existT _ __Ex_ty_cstr_'b1
                        [original_type_expr, construct, ty_value] :=
                        cast_exists (Es := Set)
                          (fun __Ex_ty_cstr_'b1 ⇒
                            [Alpha_context.Script.node **
                              __Ex_ty_cstr_'b1 → __1 ** Script_typed_ir.ty])
                          [original_type_expr, construct, ty_value] in
                      Ex_ty_cstr
                        {| ex_ty_cstr.Ex_ty_cstr.ty := ty_value;
                          ex_ty_cstr.Ex_ty_cstr.construct :=
                            fun (e_value : __Ex_ty_cstr_'b1) ⇒
                              Script_typed_ir.R (construct e_value);
                          ex_ty_cstr.Ex_ty_cstr.original_type_expr :=
                            original_type_expr; |})
                end))
        |
          ((_, {|
            Script_typed_ir.entrypoints_node.nested := Script_typed_ir.Entrypoints_None
              |}), _) ⇒ Gas_monad.of_result (Pervasives.Error tt)
        | _ ⇒ unreachable_gadt_branch
        end) in
  let '{|
    Script_typed_ir.entrypoints.root := root_value;
      Script_typed_ir.entrypoints.original_type_expr := original_type_expr
      |} := entrypoints in
  Gas_monad.bind_recover (find_entrypoint full_value root_value entrypoint)
    (fun (function_parameter : Pervasives.result (ex_ty_cstr full) unit) ⇒
      match function_parameter with
      | Pervasives.Ok f_t ⇒ Gas_monad.Syntax._return f_t
      | Pervasives.Error _ ⇒
        if Alpha_context.Entrypoint.is_default entrypoint then
          Gas_monad.Syntax._return
            (Ex_ty_cstr
              {| ex_ty_cstr.Ex_ty_cstr.ty := full_value;
                ex_ty_cstr.Ex_ty_cstr.construct :=
                  fun (e_value : full) ⇒ e_value;
                ex_ty_cstr.Ex_ty_cstr.original_type_expr := original_type_expr;
                |})
        else
          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
                  (Build_extensible "No_such_entrypoint"
                    Alpha_context.Entrypoint.t entrypoint))
              end)
      end).

Definition find_entrypoint_for_type {full : Set} {error_trace : Set}
  (error_details : Script_tc_errors.error_details Alpha_context.Script.location)
  (full_value : Script_typed_ir.ty) (expected : Script_typed_ir.ty)
  (entrypoints : Script_typed_ir.entrypoints)
  (entrypoint : Alpha_context.Entrypoint.t)
  : Gas_monad.t (Alpha_context.Entrypoint.t × Script_typed_ir.ty) error_trace :=
  Gas_monad.Syntax.op_letstar
    ((find_entrypoint error_details full_value entrypoints entrypoint) :
      Gas_monad.t (ex_ty_cstr full) error_trace)
    (fun res ⇒
      let 'Ex_ty_cstr {| ex_ty_cstr.Ex_ty_cstr.ty := ty_value |} := res in
      match
        (entrypoints.(Script_typed_ir.entrypoints.root).(Script_typed_ir.entrypoints_node.at_node),
          match
            entrypoints.(Script_typed_ir.entrypoints.root).(Script_typed_ir.entrypoints_node.at_node)
            with
          |
            Some {|
              Script_typed_ir.entrypoint_info.name := name;
                Script_typed_ir.entrypoint_info.original_type_expr := _
                |} ⇒
            (Alpha_context.Entrypoint.is_root name) &&
            (Alpha_context.Entrypoint.is_default entrypoint)
          | _ ⇒ false
          end) with
      |
        (Some {|
          Script_typed_ir.entrypoint_info.name := name;
            Script_typed_ir.entrypoint_info.original_type_expr := _
            |}, true) ⇒
        Gas_monad.bind_recover (ty_eq Script_tc_errors.Fast ty_value expected)
          (fun (function_parameter :
            Pervasives.result eq Script_tc_errors.inconsistent_types_fast_error)
            ⇒
            match function_parameter with
            | Pervasives.Ok Eq ⇒
              Gas_monad.Syntax._return
                (Alpha_context.Entrypoint.default, ty_value)
            | Pervasives.Error Script_tc_errors.Inconsistent_types_fast ⇒
              Gas_monad.Syntax.op_letplus
                (ty_eq error_details full_value expected)
                (fun function_parameter ⇒
                  let 'Eq := function_parameter in
                  (Alpha_context.Entrypoint.root_value, full_value))
            end)
      | (_, _) ⇒
        Gas_monad.Syntax.op_letplus (ty_eq error_details ty_value expected)
          (fun function_parameter ⇒
            let 'Eq := function_parameter in
            (entrypoint, ty_value))
      end).

Definition well_formed_entrypoints
  (full_value : Script_typed_ir.ty)
  (entrypoints : Script_typed_ir.entrypoints_node) : M? unit :=
  let merge {A : Set}
    (path : list A) (ty_value : Script_typed_ir.ty)
    (entrypoints : Script_typed_ir.entrypoints_node) (reachable : bool)
    (function_parameter : option (list A) × Entrypoint_repr._Set.(_Set.S.t))
    : M? ((option (list A) × Entrypoint_repr._Set.(_Set.S.t)) × bool) :=
    let '(first_unreachable, all) as acc_value := function_parameter in
    match entrypoints.(Script_typed_ir.entrypoints_node.at_node) with
    | None ⇒
      return?
        ((if reachable then
          acc_value
        else
          match ty_value with
          | Script_typed_ir.Union_t _ _ _ _ ⇒ acc_value
          | _ ⇒
            match first_unreachable with
            | None ⇒ ((Some (List.rev path)), all)
            | Some _ ⇒ acc_value
            end
          end), reachable)
    |
      Some {|
        Script_typed_ir.entrypoint_info.name := name;
          Script_typed_ir.entrypoint_info.original_type_expr := _
          |} ⇒
      if Alpha_context.Entrypoint._Set.(_Set.S.mem) name all then
        Error_monad.error_value
          (Build_extensible "Duplicate_entrypoint" Alpha_context.Entrypoint.t
            name)
      else
        return?
          ((first_unreachable,
            (Alpha_context.Entrypoint._Set.(_Set.S.add) name all)), true)
    end in
  let fix check
    (t_value : Script_typed_ir.ty)
    (entrypoints : Script_typed_ir.entrypoints_node)
    (path : list Alpha_context.Script.prim) (reachable : bool)
    (acc_value :
      option (list Alpha_context.Script.prim) × Entrypoint_repr._Set.(_Set.S.t))
    : M?
      (option (list Alpha_context.Script.prim) × Entrypoint_repr._Set.(_Set.S.t)) :=
    match (t_value, entrypoints) with
    |
      (Script_typed_ir.Union_t tl tr _ _, {|
        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
              |}
          |}) ⇒
      let? '(acc_value, l_reachable) :=
        merge (cons Michelson_v1_primitives.D_Left path) tl _left reachable
          acc_value in
      let? '(acc_value, r_reachable) :=
        merge (cons Michelson_v1_primitives.D_Right path) tr _right reachable
          acc_value in
      let? acc_value :=
        check tl _left (cons Michelson_v1_primitives.D_Left path) l_reachable
          acc_value in
      check tr _right (cons Michelson_v1_primitives.D_Right path) r_reachable
        acc_value
    | _ ⇒ return? acc_value
    end in
  let '(init_value, reachable) :=
    match entrypoints.(Script_typed_ir.entrypoints_node.at_node) with
    | None ⇒ (Alpha_context.Entrypoint._Set.(_Set.S.empty), false)
    |
      Some {|
        Script_typed_ir.entrypoint_info.name := name;
          Script_typed_ir.entrypoint_info.original_type_expr := _
          |} ⇒ ((Alpha_context.Entrypoint._Set.(_Set.S.singleton) name), true)
    end in
  let? '(first_unreachable, all) :=
    check full_value entrypoints nil reachable (None, init_value) in
  if
    Pervasives.not
      (Alpha_context.Entrypoint._Set.(_Set.S.mem)
        Alpha_context.Entrypoint.default all)
  then
    Result.return_unit
  else
    match first_unreachable with
    | None ⇒ Result.return_unit
    | Some path ⇒
      Error_monad.error_value
        (Build_extensible "Unreachable_entrypoint"
          (list Alpha_context.Script.prim) path)
    end.

Records for the constructor parameters

Module ConstructorRecords_ex_parameter_ty_and_entrypoints.
  Module ex_parameter_ty_and_entrypoints.
    Module Ex_parameter_ty_and_entrypoints.
      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.
    Definition Ex_parameter_ty_and_entrypoints_skeleton :=
      Ex_parameter_ty_and_entrypoints.record.
  End ex_parameter_ty_and_entrypoints.
End ConstructorRecords_ex_parameter_ty_and_entrypoints.
Import ConstructorRecords_ex_parameter_ty_and_entrypoints.

Reserved Notation
  "'ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints".

Inductive ex_parameter_ty_and_entrypoints : Set :=
| Ex_parameter_ty_and_entrypoints :
  'ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints →
  ex_parameter_ty_and_entrypoints

where "'ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints" :=
  (ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints_skeleton
    Script_typed_ir.ty Script_typed_ir.entrypoints).

Module ex_parameter_ty_and_entrypoints.
  Include ConstructorRecords_ex_parameter_ty_and_entrypoints.ex_parameter_ty_and_entrypoints.
  Definition Ex_parameter_ty_and_entrypoints :=
    'ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.
End ex_parameter_ty_and_entrypoints.

Definition parse_parameter_ty_and_entrypoints_aux
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (node_value : Alpha_context.Script.node)
  : M? (ex_parameter_ty_and_entrypoints × Alpha_context.context) :=
  let?
    '(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) :=
    parse_passable_ty_aux_with_ret ctxt (stack_depth +i 1) legacy
      Parse_entrypoints node_value in
  let? '_ :=
    if legacy then
      Result.return_unit
    else
      well_formed_entrypoints arg_type entrypoints in
  let entrypoints :=
    {| Script_typed_ir.entrypoints.root := entrypoints;
      Script_typed_ir.entrypoints.original_type_expr := node_value; |} in
  return?
    ((Ex_parameter_ty_and_entrypoints
      {|
        ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.arg_type
          := arg_type;
        ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.entrypoints
          := entrypoints; |}), ctxt).

Definition parse_passable_ty_aux
  : Alpha_context.context → int → bool → Alpha_context.Script.node →
  M? (Script_typed_ir.ex_ty × Alpha_context.context) :=
  fun x_1 x_2 x_3 ⇒
    parse_passable_ty_aux_with_ret x_1 x_2 x_3 Don't_parse_entrypoints.

Definition parse_uint (nb_bits : int)
  : Micheline.node Alpha_context.Script.location Alpha_context.Script.prim →
  M? int :=
  if (nb_bits ≥i 0) && (nb_bits ≤i 30) then
    let max_int := (Pervasives.lsl 1 nb_bits) -i 1 in
    let max_z := Z.of_int max_int in
    fun (function_parameter :
      Micheline.node Alpha_context.Script.location Alpha_context.Script.prim) ⇒
      match
        (function_parameter,
          match function_parameter with
          | Micheline.Int _ n_value ⇒
            (Z.zero ≤Z n_value) && (n_value ≤Z max_z)
          | _ ⇒ false
          end) with
      | (Micheline.Int _ n_value, true) ⇒ return? (Z.to_int n_value)
      | (node_value, _) ⇒
        Error_monad.error_value
          (Build_extensible "Invalid_syntactic_constant"
            (Alpha_context.Script.location ×
              Micheline.canonical Alpha_context.Script.prim × string)
            ((location node_value), (Micheline.strip_locations node_value),
              (Pervasives.op_caret "a positive "
                (Pervasives.op_caret (Pervasives.string_of_int nb_bits)
                  (Pervasives.op_caret "-bit integer (between 0 and "
                    (Pervasives.op_caret (Pervasives.string_of_int max_int) ")"))))))
      end
  else
    fun (function_parameter :
      Micheline.node Alpha_context.Script.location Alpha_context.Script.prim) ⇒
      let '_ := function_parameter in
      Error_monad.error_value (Build_extensible "Asserted" unit tt).

Definition parse_uint10
  : Micheline.node Alpha_context.Script.location Alpha_context.Script.prim →
  M? int := parse_uint 10.

Definition parse_uint11
  : Micheline.node Alpha_context.Script.location Alpha_context.Script.prim →
  M? int := parse_uint 11.

Definition opened_ticket_type
  (loc_value : Alpha_context.Script.location)
  (ty_value : Script_typed_ir.comparable_ty)
  : M? Script_typed_ir.comparable_ty :=
  Script_typed_ir.comparable_pair_3_t loc_value Script_typed_ir.address_t
    ty_value Script_typed_ir.nat_t.

Definition parse_unit
  (ctxt : Alpha_context.context) (legacy : bool)
  (function_parameter :
    Micheline.node Alpha_context.Script.location Alpha_context.Script.prim)
  : M? (unit × Alpha_context.context) :=
  match function_parameter with
  | Micheline.Prim loc_value Michelson_v1_primitives.D_Unit [] annot ⇒
    let? '_ :=
      if legacy then
        Result.return_unit
      else
        Script_ir_annot.error_unexpected_annot loc_value annot in
    let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.unit_value in
    return? (tt, ctxt)
  | Micheline.Prim loc_value Michelson_v1_primitives.D_Unit 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.D_Unit, 0, (List.length l_value)))
  | expr ⇒
    Error_monad.error_value
      (unexpected expr nil Michelson_v1_primitives.Constant_namespace
        [ Michelson_v1_primitives.D_Unit ])
  end.

Definition parse_bool
  (ctxt : Alpha_context.context) (legacy : bool)
  (function_parameter :
    Micheline.node Alpha_context.Script.location Alpha_context.Script.prim)
  : M? (bool × Alpha_context.context) :=
  match function_parameter with
  | Micheline.Prim loc_value Michelson_v1_primitives.D_True [] annot ⇒
    let? '_ :=
      if legacy then
        Result.return_unit
      else
        Script_ir_annot.error_unexpected_annot loc_value annot in
    let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.bool_value in
    return? (true, ctxt)
  | Micheline.Prim loc_value Michelson_v1_primitives.D_False [] annot ⇒
    let? '_ :=
      if legacy then
        Result.return_unit
      else
        Script_ir_annot.error_unexpected_annot loc_value annot in
    let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.bool_value in
    return? (false, ctxt)
  |
    Micheline.Prim loc_value
      ((Michelson_v1_primitives.D_True | Michelson_v1_primitives.D_False) as
        c_value) l_value _ ⇒
    Error_monad.error_value
      (Build_extensible "Invalid_arity"
        (Alpha_context.Script.location × Alpha_context.Script.prim × int × int)
        (loc_value, c_value, 0, (List.length l_value)))
  | expr ⇒
    Error_monad.error_value
      (unexpected expr nil Michelson_v1_primitives.Constant_namespace
        [ Michelson_v1_primitives.D_True; Michelson_v1_primitives.D_False ])
  end.

Definition parse_string
  (ctxt : Alpha_context.context)
  (function_parameter : Alpha_context.Script.node)
  : M? (Script_string.t × Alpha_context.context) :=
  match function_parameter with
  | (Micheline.String loc_value v_value) as expr ⇒
    let? ctxt :=
      Alpha_context.Gas.consume ctxt (Typecheck_costs.check_printable v_value)
      in
    Error_monad.record_trace
      (Build_extensible "Invalid_syntactic_constant"
        (Alpha_context.Script.location ×
          Micheline.canonical Alpha_context.Script.prim × string)
        (loc_value, (Micheline.strip_locations expr), "a printable ascii string"))
      (let? s_value := Script_string.of_string