🍃 RPC_service.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.

Module Valid.
  Import RPC_service.t.

  Record t {prefix params query input output : Set}
    (domain_query : query → Prop)
    (domain_input : input → Prop)
    (domain_output : output → Prop)
    (service : RPC_service.t prefix params query input output) : Prop := {
    query_rpc : RPC_query.Valid.t domain_query service.(query_rpc);
    input_encoding :
      Data_encoding.Valid.t domain_input service.(input_encoding);
    output_encoding :
      Data_encoding.Valid.t domain_output service.(output_encoding);
  }.
End Valid.

Ltac rpc_auto :=
  constructor;
  match goal with
  | |- Data_encoding.Valid.t _ _ ⇒ Data_encoding.Valid.data_encoding_auto
  | |- RPC_query.Valid.t _ _ ⇒ RPC_query.valid_auto
  end.