🥷 Sapling_services.v
Translated 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; |}.
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; |}.