Skip to main content

✒️ Contract_services.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.V7.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Gas_monad.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Sapling_services.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Services_registration.

Definition custom_root : RPC_path.context RPC_context.t :=
  RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "contracts".

Definition big_map_root : RPC_path.context RPC_context.t :=
  RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "big_maps".

Module info.
  Record record : Set := Build {
    balance : Alpha_context.Tez.t;
    delegate : option Alpha_context.public_key_hash;
    counter : option Alpha_context.counter;
    script : option Alpha_context.Script.t;
  }.
  Definition with_balance balance (r : record) :=
    Build balance r.(delegate) r.(counter) r.(script).
  Definition with_delegate delegate (r : record) :=
    Build r.(balance) delegate r.(counter) r.(script).
  Definition with_counter counter (r : record) :=
    Build r.(balance) r.(delegate) counter r.(script).
  Definition with_script script (r : record) :=
    Build r.(balance) r.(delegate) r.(counter) script.
End info.
Definition info := info.record.

Definition info_encoding : Data_encoding.encoding info :=
  Data_encoding.conv
    (fun (function_parameter : info) ⇒
      let '{|
        info.balance := balance;
          info.delegate := delegate;
          info.counter := counter;
          info.script := script
          |} := function_parameter in
      (balance, delegate, script, counter))
    (fun (function_parameter :
      Alpha_context.Tez.t × option Alpha_context.public_key_hash ×
        option Alpha_context.Script.t × option Alpha_context.counter) ⇒
      let '(balance, delegate, script, counter) := function_parameter in
      {| info.balance := balance; info.delegate := delegate;
        info.counter := counter; info.script := script; |}) None
    (Data_encoding.obj4
      (Data_encoding.req None None "balance" Alpha_context.Tez.encoding)
      (Data_encoding.opt None None "delegate"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.opt None None "script" Alpha_context.Script.encoding)
      (Data_encoding.opt None None "counter" Data_encoding.n_value)).

Definition legacy : Script_ir_translator_config.elab_config :=
  Script_ir_translator_config.make None None true tt.

Module S.
  Definition balance
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit Alpha_context.Tez.t :=
    RPC_service.get_service
      (Some
        "Access the spendable balance of a contract, excluding frozen bonds.")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "balance").

  Definition frozen_bonds
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit Alpha_context.Tez.t :=
    RPC_service.get_service (Some "Access the frozen bonds of a contract.")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "frozen_bonds").

  Definition balance_and_frozen_bonds
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit Alpha_context.Tez.t :=
    RPC_service.get_service
      (Some
        "Access the sum of the spendable balance and frozen bonds of a contract. This sum is part of the contract's stake, and it is exactly the contract's stake if the contract is not a delegate.")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "balance_and_frozen_bonds").

  Definition manager_key
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit
      (option Signature.public_key) :=
    RPC_service.get_service (Some "Access the manager of an implicit contract.")
      RPC_query.empty
      (Data_encoding.option_value
        Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "manager_key").

  Definition delegate
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit
      Signature.public_key_hash :=
    RPC_service.get_service (Some "Access the delegate of a contract, if any.")
      RPC_query.empty
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "delegate").

  Definition counter
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit Z.t :=
    RPC_service.get_service (Some "Access the counter of a contract, if any.")
      RPC_query.empty Data_encoding.z_value
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "counter").

  Definition script
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit
      Alpha_context.Script.t :=
    RPC_service.get_service (Some "Access the code and data of the contract.")
      RPC_query.empty Alpha_context.Script.encoding
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "script").

  Definition storage_value
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit unit
      Alpha_context.Script.expr :=
    RPC_service.get_service (Some "Access the data of the contract.")
      RPC_query.empty Alpha_context.Script.expr_encoding
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "storage").

  Module normalize_types_query.
    Record record : Set := Build {
      normalize_types : bool;
    }.
    Definition with_normalize_types normalize_types (r : record) :=
      Build normalize_types.
  End normalize_types_query.
  Definition normalize_types_query := normalize_types_query.record.

  Definition normalize_types_query_value : RPC_query.t normalize_types_query :=
    RPC_query.seal
      (RPC_query.op_pipeplus
        (RPC_query.query_value
          (fun (normalize_types : bool) ⇒
            {| normalize_types_query.normalize_types := normalize_types; |}))
        (RPC_query.flag
          (Some
            "Whether types should be normalized (annotations removed, combs flattened) or kept as they appeared in the original script.")
          "normalize_types"
          (fun (t_value : normalize_types_query) ⇒
            t_value.(normalize_types_query.normalize_types)))).

  Definition entrypoint_type
    : RPC_service.service RPC_context.t
      ((RPC_context.t × Alpha_context.Contract.t) × Alpha_context.Entrypoint.t)
      normalize_types_query unit Alpha_context.Script.expr :=
    RPC_service.get_service
      (Some "Return the type of the given entrypoint of the contract")
      normalize_types_query_value Alpha_context.Script.expr_encoding
      (RPC_path.op_divcolon
        (RPC_path.op_div
          (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
          "entrypoints") Alpha_context.Entrypoint.rpc_arg).

  Definition list_entrypoints
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) normalize_types_query unit
      (list (list Michelson_v1_primitives.prim) ×
        list (string × Alpha_context.Script.expr)) :=
    RPC_service.get_service
      (Some "Return the list of entrypoints of the contract")
      normalize_types_query_value
      (Data_encoding.obj2
        (Data_encoding.dft None None "unreachable"
          (Data_encoding.list_value None
            (Data_encoding.obj1
              (Data_encoding.req None None "path"
                (Data_encoding.list_value None
                  Michelson_v1_primitives.prim_encoding)))) nil)
        (Data_encoding.req None None "entrypoints"
          (Data_encoding.assoc Alpha_context.Script.expr_encoding)))
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "entrypoints").

  Definition contract_big_map_get_opt
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) unit
      (Alpha_context.Script.expr × Alpha_context.Script.expr)
      (option Alpha_context.Script.expr) :=
    RPC_service.post_service
      (Some
        "Access the value associated with a key in a big map of the contract (deprecated).")
      RPC_query.empty
      (Data_encoding.obj2
        (Data_encoding.req None None "key" Alpha_context.Script.expr_encoding)
        (Data_encoding.req None None "type" Alpha_context.Script.expr_encoding))
      (Data_encoding.option_value Alpha_context.Script.expr_encoding)
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
        "big_map_get").

  Definition big_map_get
    : RPC_service.service RPC_context.t
      ((RPC_context.t × Alpha_context.Big_map.Id.t) × Script_expr_hash.t) unit
      unit Alpha_context.Script.expr :=
    RPC_service.get_service
      (Some "Access the value associated with a key in a big map.")
      RPC_query.empty Alpha_context.Script.expr_encoding
      (RPC_path.op_divcolon
        (RPC_path.op_divcolon big_map_root Alpha_context.Big_map.Id.rpc_arg)
        Script_expr_hash.rpc_arg).

  Module big_map_get_all_query.
    Record record : Set := Build {
      offset : option int;
      length : option int;
    }.
    Definition with_offset offset (r : record) :=
      Build offset r.(length).
    Definition with_length length (r : record) :=
      Build r.(offset) length.
  End big_map_get_all_query.
  Definition big_map_get_all_query := big_map_get_all_query.record.

  Definition rpc_arg_uint : RPC_arg.t int :=
    let int_of_string (s_value : string) : Pervasives.result int string :=
      let? i_value :=
        Option.to_result
          (Format.sprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Cannot parse integer value "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format))
              "Cannot parse integer value %s") s_value)
          (Pervasives.int_of_string_opt s_value) in
      if i_value <i 0 then
        Pervasives.Error
          (Format.sprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Negative integer: "
                (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  CamlinternalFormatBasics.End_of_format))
              "Negative integer: %d") i_value)
      else
        Pervasives.Ok i_value in
    RPC_arg.make (Some "A non-negative integer (greater than or equal to 0).")
      "uint" int_of_string Pervasives.string_of_int tt.

  Definition big_map_get_all_query_value : RPC_query.t big_map_get_all_query :=
    RPC_query.seal
      (RPC_query.op_pipeplus
        (RPC_query.op_pipeplus
          (RPC_query.query_value
            (fun (offset : option int) ⇒
              fun (length : option int) ⇒
                {| big_map_get_all_query.offset := offset;
                  big_map_get_all_query.length := length; |}))
          (RPC_query.opt_field
            (Some
              "Skip the first [offset] values. Useful in combination with [length] for pagination.")
            "offset" rpc_arg_uint
            (fun (t_value : big_map_get_all_query) ⇒
              t_value.(big_map_get_all_query.offset))))
        (RPC_query.opt_field
          (Some
            "Only retrieve [length] values. Useful in combination with [offset] for pagination.")
          "length" rpc_arg_uint
          (fun (t_value : big_map_get_all_query) ⇒
            t_value.(big_map_get_all_query.length)))).

  Definition big_map_get_all
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Big_map.Id.t) big_map_get_all_query unit
      (list Alpha_context.Script.expr) :=
    RPC_service.get_service
      (Some
        "Get the (optionally paginated) list of values in a big map. Order of values is unspecified, but is guaranteed to be consistent.")
      big_map_get_all_query_value
      (Data_encoding.list_value None Alpha_context.Script.expr_encoding)
      (RPC_path.op_divcolon big_map_root Alpha_context.Big_map.Id.rpc_arg).

  Definition info_value
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.t) normalize_types_query unit info :=
    RPC_service.get_service (Some "Access the complete status of a contract.")
      normalize_types_query_value info_encoding
      (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg).

  Definition list_value
    : RPC_service.service RPC_context.t RPC_context.t unit unit
      (list Alpha_context.Contract.t) :=
    RPC_service.get_service
      (Some "All existing contracts (excluding empty implicit contracts).")
      RPC_query.empty
      (Data_encoding.list_value None Alpha_context.Contract.encoding)
      custom_root.

  Module Sapling.
    Definition single_sapling_get_id
      (ctxt : Alpha_context.context) (contract_id : Contract_hash.t)
      : M? (option Alpha_context.Sapling.Id.t × Alpha_context.context) :=
      let? '(ctxt, script) := Alpha_context.Contract.get_script ctxt contract_id
        in
      match script with
      | Nonereturn? (None, ctxt)
      | Some script
        let ctxt := Alpha_context.Gas.set_unlimited ctxt in
        let tzresult :=
          Script_ir_translator.parse_script legacy ctxt true script in
        let?
          '(Script_ir_translator.Ex_script (Script_typed_ir.Script script), ctxt) :=
          tzresult in
        Script_ir_translator.get_single_sapling_state ctxt
          script.(Script_typed_ir.script.Script.storage_type)
          script.(Script_typed_ir.script.Script.storage)
      end.

    Definition make_service {A B : Set}
      (function_parameter : Sapling_services.S.Args.t A B)
      : RPC_service.service RPC_context.t
        (RPC_context.t × Alpha_context.Contract.t) A unit B ×
        (Alpha_context.context Alpha_context.Contract.t A unit
        M? (option B)) :=
      let '{|
        Sapling_services.S.Args.t.name := name;
          Sapling_services.S.Args.t.description := description;
          Sapling_services.S.Args.t.query := query_value;
          Sapling_services.S.Args.t.output := output;
          Sapling_services.S.Args.t.f := f_value
          |} := function_parameter in
      let name := Pervasives.op_caret "single_sapling_" name in
      let path :=
        RPC_path.op_div
          (RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg) name
        in
      let service :=
        RPC_service.get_service (Some description) query_value output path in
      (service,
        (fun (ctxt : Alpha_context.context) ⇒
          fun (contract_id : Alpha_context.Contract.t) ⇒
            fun (q_value : A) ⇒
              fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                match contract_id with
                | Contract_repr.Implicit _Error_monad.return_none
                | Contract_repr.Originated contract_id
                  let? '(sapling_id, ctxt) :=
                    single_sapling_get_id ctxt contract_id in
                  Option.map_es
                    (fun (sapling_id : Alpha_context.Sapling.Id.t) ⇒
                      f_value ctxt sapling_id q_value) sapling_id
                end)).

    Definition get_diff
      : RPC_service.service RPC_context.t
        (RPC_context.t × Alpha_context.Contract.t) Sapling_services.diff_query
        unit (Alpha_context.Sapling.root × Alpha_context.Sapling.diff) ×
        (Alpha_context.context Alpha_context.Contract.t
        Sapling_services.diff_query unit
        M? (option (Alpha_context.Sapling.root × Alpha_context.Sapling.diff))) :=
      make_service Sapling_services.S.Args.get_diff.

    Definition register (function_parameter : unit) : unit :=
      let '_ := function_parameter in
      let reg {A B C D : Set}
        (chunked : bool)
        (function_parameter :
          RPC_service.t Updater.rpc_context (Updater.rpc_context × A) B C D ×
            (Alpha_context.t A B C M? (option D))) : unit :=
        let '(service, f_value) := function_parameter in
        Services_registration.opt_register1 chunked service f_value in
      reg false get_diff.

    Definition mk_call1 {A B C D E : Set}
      (function_parameter :
        RPC_service.t RPC_context.t (RPC_context.t × A) B unit C × D)
      : RPC_context.simple E E A B Error_monad.shell_tzresult C :=
      let '(service, _f) := function_parameter in
      fun (ctxt : RPC_context.simple E) ⇒
        fun (block : E) ⇒
          fun (id : A) ⇒
            fun (q_value : B) ⇒
              RPC_context.make_call1 service ctxt block id q_value tt.
  End Sapling.
End S.

Definition register (function_parameter : unit) : unit :=
  let '_ := function_parameter in
  let '_ :=
    Services_registration.register0 true S.list_value
      (fun (ctxt : Alpha_context.t) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Alpha_context.Contract.list_value ctxt) in
  let register_field_gen {A B C D E : Set}
    (filter_contract :
      Alpha_context.Contract.t (A Pervasives.result (option B) C)
      M? (option D)) (wrap_result : E Pervasives.result (option B) C)
    (chunked : bool)
    (s_value :
      RPC_service.t Updater.rpc_context
        (Updater.rpc_context × Alpha_context.Contract.t) unit unit D)
    (f_value : Alpha_context.t A E) : unit :=
    Services_registration.opt_register1 chunked s_value
      (fun (ctxt : Alpha_context.t) ⇒
        fun (contract : Alpha_context.Contract.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              filter_contract contract
                (fun (filtered_contract : A) ⇒
                  let function_parameter :=
                    Alpha_context.Contract._exists ctxt contract in
                  match function_parameter with
                  | truewrap_result (f_value ctxt filtered_contract)
                  | falseError_monad.return_none
                  end)) in
  let register_field_with_query_gen {A B C D E F : Set}
    (filter_contract :
      Alpha_context.Contract.t (A Pervasives.result (option B) C)
      M? (option D)) (wrap_result : E Pervasives.result (option B) C)
    (chunked : bool)
    (s_value :
      RPC_service.t Updater.rpc_context
        (Updater.rpc_context × Alpha_context.Contract.t) F unit D)
    (f_value : Alpha_context.t A F E) : unit :=
    Services_registration.opt_register1 chunked s_value
      (fun (ctxt : Alpha_context.t) ⇒
        fun (contract : Alpha_context.Contract.t) ⇒
          fun (query_value : F) ⇒
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              filter_contract contract
                (fun (filtered_contract : A) ⇒
                  let function_parameter :=
                    Alpha_context.Contract._exists ctxt contract in
                  match function_parameter with
                  | true
                    wrap_result (f_value ctxt filtered_contract query_value)
                  | falseError_monad.return_none
                  end)) in
  let register_field {A : Set}
    (s_value :
      RPC_service.t Updater.rpc_context
        (Updater.rpc_context × Alpha_context.Contract.t) unit unit A)
    : bool (Alpha_context.t Alpha_context.Contract.t M? A) unit :=
    fun x_1
      register_field_gen
        (fun (c_value : Alpha_context.Contract.t) ⇒
          fun (k_value : Alpha_context.Contract.t M? (option A)) ⇒
            k_value c_value)
        (fun (res : M? A) ⇒ Error_monad.op_gtpipeeqquestion res Option.some)
        x_1 s_value in
  let register_field_with_query {A B : Set}
    (s_value :
      RPC_service.t Updater.rpc_context
        (Updater.rpc_context × Alpha_context.Contract.t) A unit B)
    : bool (Alpha_context.t Alpha_context.Contract.t A M? B) unit :=
    fun x_1
      register_field_with_query_gen
        (fun (c_value : Alpha_context.Contract.t) ⇒
          fun (k_value : Alpha_context.Contract.t M? (option B)) ⇒
            k_value c_value)
        (fun (res : M? B) ⇒ Error_monad.op_gtpipeeqquestion res Option.some)
        x_1 s_value in
  let register_opt_field {A : Set}
    (s_value :
      RPC_service.t Updater.rpc_context
        (Updater.rpc_context × Alpha_context.Contract.t) unit unit A)
    : bool (Alpha_context.t Alpha_context.Contract.t M? (option A))
    unit :=
    fun x_1
      register_field_gen
        (fun (c_value : Alpha_context.Contract.t) ⇒
          fun (k_value : Alpha_context.Contract.t M? (option A)) ⇒
            k_value c_value) (fun (res : M? (option A)) ⇒ res) x_1 s_value in
  let register_originated_opt_field {A : Set}
    (s_value :
      RPC_service.t Updater.rpc_context
        (Updater.rpc_context × Alpha_context.Contract.t) unit unit A)
    : bool (Alpha_context.t Contract_hash.t M? (option A)) unit :=
    fun x_1
      register_field_gen
        (fun (c_value : Alpha_context.Contract.t) ⇒
          fun (k_value : Contract_hash.t M? (option A)) ⇒
            match c_value with
            | Contract_repr.Implicit _Error_monad.return_none
            | Contract_repr.Originated c_valuek_value c_value
            end) (fun (res : M? (option A)) ⇒ res) x_1 s_value in
  let do_big_map_get
    (ctxt : Alpha_context.context) (id : Alpha_context.Big_map.Id.t)
    (key_value : Script_expr_hash.t) : M? (option Alpha_context.Script.expr) :=
    let ctxt := Alpha_context.Gas.set_unlimited ctxt in
    let? '(ctxt, types) := Alpha_context.Big_map._exists ctxt id in
    match types with
    | NoneError_monad.return_none
    | Some (_, value_type)
      let? '(Script_typed_ir.Ex_ty value_type, ctxt) :=
        Script_ir_translator.parse_big_map_value_ty ctxt true
          (Micheline.root_value value_type) in
      let 'existT _ __Ex_ty_'a [ctxt, value_type] :=
        cast_exists (Es := Set)
          (fun __Ex_ty_'a[Alpha_context.context ** Script_typed_ir.ty])
          [ctxt, value_type] in
      let? '(_ctxt, value_value) :=
        Alpha_context.Big_map.get_opt ctxt id key_value in
      match value_value with
      | NoneError_monad.return_none
      | Some value_value
        let? '(value_value, ctxt) :=
          Script_ir_translator.parse_data legacy ctxt true value_type
            (Micheline.root_value value_value) in
        let? '(value_value, _ctxt) :=
          Script_ir_translator.unparse_data ctxt Script_ir_unparser.Readable
            value_type (value_value : __Ex_ty_'a) in
        return? (Some value_value)
      end
    end in
  let do_big_map_get_all
    (offset : option int) (length : option int) (ctxt : Alpha_context.context)
    (id : Alpha_context.Big_map.Id.t) : M? (list Alpha_context.Script.expr) :=
    let ctxt := Alpha_context.Gas.set_unlimited ctxt in
    let? '(ctxt, types) := Alpha_context.Big_map._exists ctxt id in
    match types with
    | NonePervasives.raise (Build_extensible "Not_found" unit tt)
    | Some (_, value_type)
      let? '(Script_typed_ir.Ex_ty value_type, ctxt) :=
        Script_ir_translator.parse_big_map_value_ty ctxt true
          (Micheline.root_value value_type) in
      let 'existT _ __Ex_ty_'a1 [ctxt, value_type] :=
        cast_exists (Es := Set)
          (fun __Ex_ty_'a1[Alpha_context.context ** Script_typed_ir.ty])
          [ctxt, value_type] in
      let? '(ctxt, key_values) :=
        Alpha_context.Big_map.list_key_values offset length ctxt id in
      let? '(_ctxt, rev_values) :=
        List.fold_left_s
          (fun (acc_value :
            M? (Alpha_context.context × list Alpha_context.Script.expr)) ⇒
            fun (function_parameter :
              Script_expr_hash.t × Micheline.canonical Alpha_context.Script.prim)
              ⇒
              let '(_key_hash, value_value) := function_parameter in
              let? '(ctxt, rev_values) := acc_value in
              let? '(value_value, ctxt) :=
                Script_ir_translator.parse_data legacy ctxt true value_type
                  (Micheline.root_value value_value) in
              let? '(value_value, ctxt) :=
                Script_ir_translator.unparse_data ctxt
                  Script_ir_unparser.Readable value_type
                  (value_value : __Ex_ty_'a1) in
              return? (ctxt, (cons value_value rev_values)))
          (Pervasives.Ok (ctxt, nil)) key_values in
      return? (List.rev rev_values)
    end in
  let '_ := register_field S.balance false Alpha_context.Contract.get_balance in
  let '_ :=
    register_field S.frozen_bonds false Alpha_context.Contract.get_frozen_bonds
    in
  let '_ :=
    register_field S.balance_and_frozen_bonds false
      Alpha_context.Contract.get_balance_and_frozen_bonds in
  let '_ :=
    Services_registration.opt_register1 false S.manager_key
      (fun (ctxt : Alpha_context.t) ⇒
        fun (contract : Alpha_context.Contract.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              match contract with
              | Contract_repr.Originated _Error_monad.return_none
              | Contract_repr.Implicit mgr
                let? function_parameter :=
                  Alpha_context.Contract.is_manager_key_revealed ctxt mgr in
                match function_parameter with
                | falseError_monad.return_some None
                | true
                  let? key_value :=
                    Alpha_context.Contract.get_manager_key None ctxt mgr in
                  return? (Some (Some key_value))
                end
              end) in
  let '_ :=
    register_opt_field S.delegate false Alpha_context.Contract.Delegate.find in
  let '_ :=
    Services_registration.opt_register1 false S.counter
      (fun (ctxt : Alpha_context.t) ⇒
        fun (contract : Alpha_context.Contract.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              match contract with
              | Contract_repr.Originated _Error_monad.return_none
              | Contract_repr.Implicit mgr
                let? counter := Alpha_context.Contract.get_counter ctxt mgr in
                return? (Some counter)
              end) in
  let '_ :=
    register_originated_opt_field S.script true
      (fun (c_value : Alpha_context.t) ⇒
        fun (v_value : Contract_hash.t) ⇒
          let? '(_, v_value) :=
            Alpha_context.Contract.get_script c_value v_value in
          return? v_value) in
  let '_ :=
    register_originated_opt_field S.storage_value true
      (fun (ctxt : Alpha_context.t) ⇒
        fun (contract : Contract_hash.t) ⇒
          let? '(ctxt, script) :=
            Alpha_context.Contract.get_script ctxt contract in
          match script with
          | NoneError_monad.return_none
          | Some script
            let ctxt := Alpha_context.Gas.set_unlimited ctxt in
            let?
              '(Script_ir_translator.Ex_script
                (Script_typed_ir.Script {|
                  Script_typed_ir.script.Script.storage := storage_value;
                    Script_typed_ir.script.Script.storage_type := storage_type
                    |}), ctxt) :=
              Script_ir_translator.parse_script legacy ctxt true script in
            let? '(storage_value, _ctxt) :=
              Script_ir_translator.unparse_data ctxt Script_ir_unparser.Readable
                storage_type storage_value in
            return? (Some storage_value)
          end) in
  let '_ :=
    Services_registration.opt_register2 true S.entrypoint_type
      (fun (ctxt : Alpha_context.t) ⇒
        fun (v_value : Alpha_context.Contract.t) ⇒
          fun (entrypoint : Alpha_context.Entrypoint.t) ⇒
            fun (function_parameter : S.normalize_types_query) ⇒
              let '{|
                S.normalize_types_query.normalize_types := normalize_types
                  |} := function_parameter in
              fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                match v_value with
                | Contract_repr.Implicit _Error_monad.return_none
                | Contract_repr.Originated _
                  let? '(_, expr) :=
                    Alpha_context.Contract.get_script_code ctxt v_value in
                  match expr with
                  | NoneError_monad.return_none
                  | Some expr
                    let ctxt := Alpha_context.Gas.set_unlimited ctxt in
                    let legacy := true in
                    let? '(expr, _) :=
                      Alpha_context.Script.force_decode_in_context
                        Alpha_context.Script.When_needed ctxt expr in
                    let?
                      '({|
                        Script_ir_translator.toplevel.arg_type := arg_type
                          |}, ctxt) :=
                      Script_ir_translator.parse_toplevel ctxt legacy expr in
                    let?
                      '(Script_ir_translator.Ex_parameter_ty_and_entrypoints {|
                        Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.arg_type
                          := arg_type;
                          Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.entrypoints
                            := entrypoints
                          |}, _) :=
                      Script_ir_translator.parse_parameter_ty_and_entrypoints
                        ctxt legacy arg_type in
                    let 'existT _ __Ex_parameter_ty_and_entrypoints_'a
                      [entrypoints, arg_type] :=
                      cast_exists (Es := Set)
                        (fun __Ex_parameter_ty_and_entrypoints_'a
                          [Script_typed_ir.entrypoints ** Script_typed_ir.ty])
                        [entrypoints, arg_type] in
                    cast (M? (option Alpha_context.Script.expr))
                    (let? '(r_value, ctxt) :=
                      Gas_monad.run ctxt
                        (Script_ir_translator.find_entrypoint
                          (Script_tc_errors.Informative tt) arg_type entrypoints
                          entrypoint) in
                    (fun (function_parameter :
                      M?
                        (Script_ir_translator.ex_ty_cstr
                          __Ex_parameter_ty_and_entrypoints_'a)) ⇒
                      match function_parameter with
                      |
                        Pervasives.Ok
                          (Script_ir_translator.Ex_ty_cstr {|
                            Script_ir_translator.ex_ty_cstr.Ex_ty_cstr.ty := ty_value;
                              Script_ir_translator.ex_ty_cstr.Ex_ty_cstr.original_type_expr
                                := original_type_expr
                              |}) ⇒
                        if normalize_types then
                          let? '(ty_node, _ctxt) :=
                            Script_ir_unparser.unparse_ty tt ctxt ty_value in
                          return? (Some (Micheline.strip_locations ty_node))
                        else
                          return?
                            (Some (Micheline.strip_locations original_type_expr))
                      | Pervasives.Error _Result.return_none
                      end) r_value)
                  end
                end) in
  let '_ :=
    Services_registration.opt_register1 true S.list_entrypoints
      (fun (ctxt : Alpha_context.t) ⇒
        fun (v_value : Alpha_context.Contract.t) ⇒
          fun (function_parameter : S.normalize_types_query) ⇒
            let '{|
              S.normalize_types_query.normalize_types := normalize_types |} :=
              function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              match v_value with
              | Contract_repr.Implicit _Error_monad.return_none
              | Contract_repr.Originated _
                let? '(_, expr) :=
                  Alpha_context.Contract.get_script_code ctxt v_value in
                match expr with
                | NoneError_monad.return_none
                | Some expr
                  let ctxt := Alpha_context.Gas.set_unlimited ctxt in
                  let legacy := true in
                  let? '(expr, _) :=
                    Alpha_context.Script.force_decode_in_context
                      Alpha_context.Script.When_needed ctxt expr in
                  let?
                    '({| Script_ir_translator.toplevel.arg_type := arg_type |},
                      ctxt) :=
                    Script_ir_translator.parse_toplevel ctxt legacy expr in
                  let?
                    '(Script_ir_translator.Ex_parameter_ty_and_entrypoints {|
                      Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.arg_type
                        := arg_type;
                        Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.entrypoints
                          := entrypoints
                        |}, _) :=
                    Script_ir_translator.parse_parameter_ty_and_entrypoints ctxt
                      legacy arg_type in
                  let '(unreachable_entrypoint, map) :=
                    Script_ir_translator.list_entrypoints_uncarbonated arg_type
                      entrypoints in
                  let? '(entrypoint_types, _ctxt) :=
                    Alpha_context.Entrypoint.Map.(Map.S.fold_e)
                      (fun (entry : Entrypoint_repr.t) ⇒
                        fun (function_parameter :
                          Script_typed_ir.ex_ty ×
                            Micheline.node Alpha_context.Script.location
                              Alpha_context.Script.prim) ⇒
                          let
                            '(Script_typed_ir.Ex_ty ty_value, original_type_expr) :=
                            function_parameter in
                          fun (function_parameter :
                            list (string × Alpha_context.Script.expr) ×
                              Alpha_context.context) ⇒
                            let '(acc_value, ctxt) := function_parameter in
                            let? '(ty_expr, ctxt) :=
                              if normalize_types then
                                let? '(ty_node, ctxt) :=
                                  Script_ir_unparser.unparse_ty tt ctxt ty_value
                                  in
                                return?
                                  ((Micheline.strip_locations ty_node), ctxt)
                              else
                                return?
                                  ((Micheline.strip_locations original_type_expr),
                                    ctxt) in
                            return?
                              ((cons
                                ((Alpha_context.Entrypoint.to_string entry),
                                  ty_expr) acc_value), ctxt)) map (nil, ctxt) in
                  return? (Some (unreachable_entrypoint, entrypoint_types))
                end
              end) in
  let '_ :=
    Services_registration.opt_register1 true S.contract_big_map_get_opt
      (fun (ctxt : Alpha_context.t) ⇒
        fun (contract : Alpha_context.Contract.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter :
              Alpha_context.Script.expr × Alpha_context.Script.expr) ⇒
              let '(key_value, key_type) := function_parameter in
              match contract with
              | Contract_repr.Implicit _Error_monad.return_none
              | Contract_repr.Originated contract
                let? '(ctxt, script) :=
                  Alpha_context.Contract.get_script ctxt contract in
                let key_type_node := Micheline.root_value key_type in
                let? '(Script_ir_translator.Ex_comparable_ty key_type, ctxt) :=
                  Script_ir_translator.parse_comparable_ty ctxt key_type_node in
                let? '(key_value, ctxt) :=
                  Script_ir_translator.parse_comparable_data None ctxt key_type
                    (Micheline.root_value key_value) in
                let? '(key_value, ctxt) :=
                  Script_ir_translator.hash_comparable_data ctxt key_type
                    key_value in
                match script with
                | NoneError_monad.return_none
                | Some script
                  let ctxt := Alpha_context.Gas.set_unlimited ctxt in
                  let?
                    '(Script_ir_translator.Ex_script
                      (Script_typed_ir.Script script), ctxt) :=
                    Script_ir_translator.parse_script legacy ctxt true script in
                  let? '(ids, _ctxt) :=
                    Script_ir_translator.collect_lazy_storage ctxt
                      script.(Script_typed_ir.script.Script.storage_type)
                      script.(Script_typed_ir.script.Script.storage) in
                  match Script_ir_translator.list_of_big_map_ids ids with
                  | ([] | cons _ (cons _ _)) ⇒ Error_monad.return_some None
                  | cons id []
                    Error_monad.op_gtpipeeqquestion
                      (do_big_map_get ctxt id key_value) Option.some
                  end
                end
              end) in
  let '_ :=
    Services_registration.opt_register2 true S.big_map_get
      (fun (ctxt : Alpha_context.t) ⇒
        fun (id : Alpha_context.Big_map.Id.t) ⇒
          fun (key_value : Script_expr_hash.t) ⇒
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                do_big_map_get ctxt id key_value) in
  let '_ :=
    Services_registration.register1 true S.big_map_get_all
      (fun (ctxt : Alpha_context.t) ⇒
        fun (id : Alpha_context.Big_map.Id.t) ⇒
          fun (function_parameter : S.big_map_get_all_query) ⇒
            let '{|
              S.big_map_get_all_query.offset := offset;
                S.big_map_get_all_query.length := length
                |} := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              do_big_map_get_all offset length ctxt id) in
  let '_ :=
    register_field_with_query S.info_value false
      (fun (ctxt : Alpha_context.t) ⇒
        fun (contract : Alpha_context.Contract.t) ⇒
          fun (function_parameter : S.normalize_types_query) ⇒
            let '{|
              S.normalize_types_query.normalize_types := normalize_types |} :=
              function_parameter in
            let? balance := Alpha_context.Contract.get_balance ctxt contract in
            let? delegate := Alpha_context.Contract.Delegate.find ctxt contract
              in
            match contract with
            | Contract_repr.Implicit manager
              let? counter := Alpha_context.Contract.get_counter ctxt manager in
              return?
                {| info.balance := balance; info.delegate := delegate;
                  info.counter := Some counter; info.script := None; |}
            | Contract_repr.Originated contract
              let? '(ctxt, script) :=
                Alpha_context.Contract.get_script ctxt contract in
              match script with
              | None
                return?
                  {| info.balance := balance; info.delegate := delegate;
                    info.counter := None; info.script := None; |}
              | Some script
                let ctxt := Alpha_context.Gas.set_unlimited ctxt in
                let? '(script, _ctxt) :=
                  Script_ir_translator.parse_and_unparse_script_unaccounted ctxt
                    true true Script_ir_unparser.Readable normalize_types script
                  in
                return?
                  {| info.balance := balance; info.delegate := delegate;
                    info.counter := None; info.script := Some script; |}
              end
            end) in
  S.Sapling.register tt.

Definition list_value {A : Set} (ctxt : RPC_context.simple A) (block : A)
  : Error_monad.shell_tzresult (list Alpha_context.Contract.t) :=
  RPC_context.make_call0 S.list_value ctxt block tt tt.

Definition info_value {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.t) (normalize_types : bool)
  : Error_monad.shell_tzresult info :=
  RPC_context.make_call1 S.info_value ctxt block contract
    {| S.normalize_types_query.normalize_types := normalize_types; |} tt.

Definition balance {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.t)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.balance ctxt block contract tt tt.

Definition frozen_bonds {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.t)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.frozen_bonds ctxt block contract tt tt.

Definition balance_and_frozen_bonds {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.t)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.balance_and_frozen_bonds ctxt block contract tt tt.

Definition manager_key {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (mgr : Alpha_context.public_key_hash)
  : Error_monad.shell_tzresult (option Signature.public_key) :=
  RPC_context.make_call1 S.manager_key ctxt block (Contract_repr.Implicit mgr)
    tt tt.

Definition delegate {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.t)
  : Error_monad.shell_tzresult Signature.public_key_hash :=
  RPC_context.make_call1 S.delegate ctxt block contract tt tt.

Definition delegate_opt {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.t)
  : Error_monad.shell_tzresult (option Signature.public_key_hash) :=
  RPC_context.make_opt_call1 S.delegate ctxt block contract tt tt.

Definition counter {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (mgr : Alpha_context.public_key_hash) : Error_monad.shell_tzresult Z.t :=
  RPC_context.make_call1 S.counter ctxt block (Contract_repr.Implicit mgr) tt tt.

Definition script {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
  : Error_monad.shell_tzresult Alpha_context.Script.t :=
  let contract := Contract_repr.Originated contract in
  RPC_context.make_call1 S.script ctxt block contract tt tt.

Definition script_opt {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
  : Error_monad.shell_tzresult (option Alpha_context.Script.t) :=
  let contract := Contract_repr.Originated contract in
  RPC_context.make_opt_call1 S.script ctxt block contract tt tt.

Definition storage_value {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
  : Error_monad.shell_tzresult Alpha_context.Script.expr :=
  let contract := Contract_repr.Originated contract in
  RPC_context.make_call1 S.storage_value ctxt block contract tt tt.

Definition entrypoint_type {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
  (entrypoint : Alpha_context.Entrypoint.t) (normalize_types : bool)
  : Error_monad.shell_tzresult Alpha_context.Script.expr :=
  RPC_context.make_call2 S.entrypoint_type ctxt block
    (Contract_repr.Originated contract) entrypoint
    {| S.normalize_types_query.normalize_types := normalize_types; |} tt.

Definition list_entrypoints {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
  (normalize_types : bool)
  : Error_monad.shell_tzresult
    (list (list Michelson_v1_primitives.prim) ×
      list (string × Alpha_context.Script.expr)) :=
  RPC_context.make_call1 S.list_entrypoints ctxt block
    (Contract_repr.Originated contract)
    {| S.normalize_types_query.normalize_types := normalize_types; |} tt.

Definition storage_opt {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
  : Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
  let contract := Contract_repr.Originated contract in
  RPC_context.make_opt_call1 S.storage_value ctxt block contract tt tt.

Definition big_map_get {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (id : Alpha_context.Big_map.Id.t)
  (key_value : Script_expr_hash.t)
  : Error_monad.shell_tzresult Alpha_context.Script.expr :=
  RPC_context.make_call2 S.big_map_get ctxt block id key_value tt tt.

Definition contract_big_map_get_opt {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
  (key_value : Alpha_context.Script.expr × Alpha_context.Script.expr)
  : Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
  let contract := Contract_repr.Originated contract in
  RPC_context.make_call1 S.contract_big_map_get_opt ctxt block contract tt
    key_value.

Definition single_sapling_get_diff {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (id : Contract_hash.t)
  (offset_commitment : option Int64.t) (offset_nullifier : option Int64.t)
  (function_parameter : unit)
  : Error_monad.shell_tzresult
    (Alpha_context.Sapling.root × Alpha_context.Sapling.diff) :=
  let '_ := function_parameter in
  S.Sapling.mk_call1 S.Sapling.get_diff ctxt block (Contract_repr.Originated id)
    {| Sapling_services.diff_query.offset_commitment := offset_commitment;
      Sapling_services.diff_query.offset_nullifier := offset_nullifier; |}.