🥷 Sapling_services.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sapling_services.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Proto_alpha.Proofs.Sapling_repr.
Module Diff_query.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sapling_services.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Proto_alpha.Proofs.Sapling_repr.
Module Diff_query.
The definition of a valid [diff_query].
Module Valid.
Import Sapling_services.diff_query.
Record t (q : Sapling_services.diff_query) : Prop := {
offset_commitment :
Option.Forall Int64.Valid.non_negative q.(offset_commitment);
offset_nullifier :
Option.Forall Int64.Valid.non_negative q.(offset_nullifier);
}.
End Valid.
End Diff_query.
Module S.
Module Args.
Import Sapling_services.diff_query.
Record t (q : Sapling_services.diff_query) : Prop := {
offset_commitment :
Option.Forall Int64.Valid.non_negative q.(offset_commitment);
offset_nullifier :
Option.Forall Int64.Valid.non_negative q.(offset_nullifier);
}.
End Valid.
End Diff_query.
Module S.
Module Args.
The query [get_diff_query] is valid.
Lemma get_diff_query_is_valid :
RPC_query.Valid.t Diff_query.Valid.t
Sapling_services.S.Args.get_diff_query.
Proof.
RPC_query.valid_auto.
Qed.
RPC_query.Valid.t Diff_query.Valid.t
Sapling_services.S.Args.get_diff_query.
Proof.
RPC_query.valid_auto.
Qed.
The encoding [Args.encoding] is valid.
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sapling_services.S.Args.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Args.
Data_encoding.Valid.t (fun _ ⇒ True) Sapling_services.S.Args.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Args.
The [get_diff] service is valid.
Lemma get_diff_is_valid :
RPC_service.Valid.t Diff_query.Valid.t (fun _ ⇒ True) (fun _ ⇒ True)
(fst (Sapling_services.S.get_diff)).
Proof.
RPC_service.rpc_auto.
Qed.
End S.
RPC_service.Valid.t Diff_query.Valid.t (fun _ ⇒ True) (fun _ ⇒ True)
(fst (Sapling_services.S.get_diff)).
Proof.
RPC_service.rpc_auto.
Qed.
End S.