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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
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_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 :=
  (let arg :=
    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; |}) in
  fun (eta :
    Data_encoding.encoding
      (Alpha_context.Tez.t × option Alpha_context.public_key_hash ×
        option Alpha_context.Script.t × option Alpha_context.counter)) ⇒
    arg None eta)
    (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)).

Module S.
  Definition balance
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Contract.contract) 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.contract) 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.contract) 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.contract) unit unit
      (option Signature.public_key) :=
    RPC_service.get_service (Some "Access the manager of a 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.contract) 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.contract) 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.contract) 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.contract) 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.contract) ×
        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.contract) 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.contract) 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.contract) 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 (including non-empty default 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 : Alpha_context.Contract.contract)
      : 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 None ctxt true 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.contract) A unit B ×
        (Alpha_context.context Alpha_context.Contract.contract 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.contract) ⇒
            fun (q_value : A) ⇒
              fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                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)).

    Definition get_diff
      : RPC_service.service RPC_context.t
        (RPC_context.t × Alpha_context.Contract.contract)
        Sapling_services.diff_query unit
        (Alpha_context.Sapling.root × Alpha_context.Sapling.diff) ×
        (Alpha_context.context Alpha_context.Contract.contract
        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.

Axiom register : unit unit.

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.contract) (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.contract)
  : 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.contract)
  : 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.contract)
  : 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
    (Alpha_context.Contract.implicit_contract mgr) tt tt.

Definition delegate {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.contract)
  : 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.contract)
  : 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
    (Alpha_context.Contract.implicit_contract mgr) tt tt.

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

Definition script_opt {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.contract)
  : Error_monad.shell_tzresult (option Alpha_context.Script.t) :=
  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 : Alpha_context.Contract.contract)
  : Error_monad.shell_tzresult Alpha_context.Script.expr :=
  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 : Alpha_context.Contract.contract)
  (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 entrypoint
    {| S.normalize_types_query.normalize_types := normalize_types; |} tt.

Definition list_entrypoints {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.contract) (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
    {| S.normalize_types_query.normalize_types := normalize_types; |} tt.

Definition storage_opt {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (contract : Alpha_context.Contract.contract)
  : Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
  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 : Alpha_context.Contract.contract)
  (key_value : Alpha_context.Script.expr × Alpha_context.Script.expr)
  : Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
  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 : Alpha_context.Contract.contract) (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 id
    {| Sapling_services.diff_query.offset_commitment := offset_commitment;
      Sapling_services.diff_query.offset_nullifier := offset_nullifier; |}.