🥷 Sapling_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.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
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") "sapling".

Module diff_query.
  Record record : Set := Build {
    offset_commitment : option Int64.t;
    offset_nullifier : option Int64.t;
  }.
  Definition with_offset_commitment offset_commitment (r : record) :=
    Build offset_commitment r.(offset_nullifier).
  Definition with_offset_nullifier offset_nullifier (r : record) :=
    Build r.(offset_commitment) offset_nullifier.
End diff_query.
Definition diff_query := diff_query.record.

Module S.
  Module Args.
    Module t.
      Record record {query_type output_type : Set} : Set := Build {
        name : string;
        description : string;
        query : RPC_query.t query_type;
        output : Data_encoding.t output_type;
        f :
          Alpha_context.context → Alpha_context.Sapling.Id.t → query_type →
          M? output_type;
      }.
      Arguments record : clear implicits.
      Definition with_name {t_query_type t_output_type} name
        (r : record t_query_type t_output_type) :=
        Build t_query_type t_output_type name r.(description) r.(query)
          r.(output) r.(f).
      Definition with_description {t_query_type t_output_type} description
        (r : record t_query_type t_output_type) :=
        Build t_query_type t_output_type r.(name) description r.(query)
          r.(output) r.(f).
      Definition with_query {t_query_type t_output_type} query
        (r : record t_query_type t_output_type) :=
        Build t_query_type t_output_type r.(name) r.(description) query
          r.(output) r.(f).
      Definition with_output {t_query_type t_output_type} output
        (r : record t_query_type t_output_type) :=
        Build t_query_type t_output_type r.(name) r.(description) r.(query)
          output r.(f).
      Definition with_f {t_query_type t_output_type} f
        (r : record t_query_type t_output_type) :=
        Build t_query_type t_output_type r.(name) r.(description) r.(query)
          r.(output) f.
    End t.
    Definition t := t.record.

    Definition get_diff_query : RPC_query.t diff_query :=
      RPC_query.seal
        (RPC_query.op_pipeplus
          (RPC_query.op_pipeplus
            (RPC_query.query_value
              (fun (offset_commitment : option Int64.t) ⇒
                fun (offset_nullifier : option Int64.t) ⇒
                  {| diff_query.offset_commitment := offset_commitment;
                    diff_query.offset_nullifier := offset_nullifier; |}))
            (RPC_query.opt_field
              (Some
                "Commitments and ciphertexts are returned from the specified offset up to the most recent.")
              "offset_commitment" RPC_arg.uint63
              (fun (function_parameter : diff_query) ⇒
                let '{| diff_query.offset_commitment := offset_commitment |} :=
                  function_parameter in
                offset_commitment)))
          (RPC_query.opt_field
            (Some
              "Nullifiers are returned from the specified offset up to the most recent.")
            "offset_nullifier" RPC_arg.uint63
            (fun (function_parameter : diff_query) ⇒
              let '{| diff_query.offset_nullifier := offset_nullifier |} :=
                function_parameter in
              offset_nullifier))).

    Definition encoding
      : Data_encoding.encoding
        (Alpha_context.Sapling.root × Alpha_context.Sapling.diff) :=
      Data_encoding.merge_objs
        (Data_encoding.obj1
          (Data_encoding.req None None "root"
            Alpha_context.Sapling.root_encoding))
        Alpha_context.Sapling.diff_encoding.

    Definition get_diff
      : t diff_query (Alpha_context.Sapling.root × Alpha_context.Sapling.diff) :=
      {| t.name := "get_diff";
        t.description :=
          "Returns the root and a diff of a state starting from an optional offset which is zero by default.";
        t.query := get_diff_query; t.output := encoding;
        t.f :=
          fun (ctxt : Alpha_context.context) ⇒
            fun (id : Alpha_context.Sapling.Id.t) ⇒
              fun (function_parameter : diff_query) ⇒
                let '{|
                  diff_query.offset_commitment := offset_commitment;
                    diff_query.offset_nullifier := offset_nullifier
                    |} := function_parameter in
                Alpha_context.Sapling.get_diff ctxt id offset_commitment
                  offset_nullifier tt; |}.
  End Args.

  Definition make_service {A B : Set} (function_parameter : Args.t A B)
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Sapling.Id.t) A unit B ×
      (Alpha_context.context → Alpha_context.Sapling.Id.t → A → unit → M? B) :=
    let '{|
      Args.t.name := name;
        Args.t.description := description;
        Args.t.query := query_value;
        Args.t.output := output;
        Args.t.f := f_value
        |} := function_parameter in
    let path :=
      RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Sapling.rpc_arg) name in
    let service :=
      RPC_service.get_service (Some description) query_value output path in
    (service,
      (fun (ctxt : Alpha_context.context) ⇒
        fun (id : Alpha_context.Sapling.Id.t) ⇒
          fun (q_value : A) ⇒
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              f_value ctxt id q_value)).

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

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? D)) : unit :=
    let '(service, f_value) := function_parameter in
    Services_registration.register1 chunked service f_value in
  reg false S.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.

Definition get_diff {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (id : Alpha_context.Sapling.Id.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
  mk_call1 S.get_diff ctxt block id
    {| diff_query.offset_commitment := offset_commitment;
      diff_query.offset_nullifier := offset_nullifier; |}.