Skip to content

Services: make the RPC_services predicate more general

Guillaume Claret requested to merge clarus@update_rpc_services_predicate into master

In this MR we add two domain parameters to the predicate RPC_service.Valid.t as parameters for the respective data-encodings. This is required by the service https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/alpha_services#Seed.S.seed_value because one of the encodings of this service is only true on a certain domain.

The downside is that this is very verbose and requires changing other RPC_service.Valid.t predicates by adding (fun _ => True) everywhere. I do not know about a good method to have default arguments in Coq, as this domain should probably be (fun _ => True) by default. A technique would be to use an option type for the domain, which would get reduced to None instead.

Edited by Guillaume Claret

Merge request reports