🌌 Alpha_services.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_services.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Proofs.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Module Seed.
Module S.
Lemma seed_value_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True) Seed_repr.Seed.Valid.t
Alpha_services.Seed.S.seed_value.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Seed.
Module Nonce.
Module Info.
Module Valid.
Definition t (info : Alpha_services.Nonce.info) : Prop :=
match info with
| Alpha_services.Nonce.Revealed nonce ⇒ Seed_repr.Nonce.Valid.t nonce
| _ ⇒ True
end.
End Valid.
Lemma encoding_is_valid
: Data_encoding.Valid.t Valid.t Alpha_services.Nonce.info_encoding.
Data_encoding.Valid.data_encoding_auto;
intros []; tauto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Info.
Module S.
Lemma get_is_valid :
RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Info.Valid.t
Alpha_services.Nonce.S.get.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Nonce.
Module Liquidity_baking.
Module S.
Lemma get_cpmm_address_is_valid :
RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Alpha_services.Liquidity_baking.S.get_cpmm_address.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Liquidity_baking.
Module Cache.
Module S.
Lemma cached_contracts_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True)
(List.Forall (fun '(_, i) ⇒ Pervasives.Int31.Valid.t i))
Alpha_services.Cache.S.cached_contracts.
Proof.
RPC_service.rpc_auto.
apply List.Forall_impl.
hauto l: on.
Qed.
Lemma contract_cache_size_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True) Pervasives.Int31.Valid.t
Alpha_services.Cache.S.contract_cache_size.
Proof.
RPC_service.rpc_auto.
Qed.
Lemma contract_cache_size_limit_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True) Pervasives.Int31.Valid.t
Alpha_services.Cache.S.contract_cache_size_limit.
Proof.
RPC_service.rpc_auto.
Qed.
Lemma contract_rank_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True)
(Option.Forall Pervasives.Int31.Valid.t)
Alpha_services.Cache.S.contract_rank.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Cache.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_services.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Proofs.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Module Seed.
Module S.
Lemma seed_value_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True) Seed_repr.Seed.Valid.t
Alpha_services.Seed.S.seed_value.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Seed.
Module Nonce.
Module Info.
Module Valid.
Definition t (info : Alpha_services.Nonce.info) : Prop :=
match info with
| Alpha_services.Nonce.Revealed nonce ⇒ Seed_repr.Nonce.Valid.t nonce
| _ ⇒ True
end.
End Valid.
Lemma encoding_is_valid
: Data_encoding.Valid.t Valid.t Alpha_services.Nonce.info_encoding.
Data_encoding.Valid.data_encoding_auto;
intros []; tauto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Info.
Module S.
Lemma get_is_valid :
RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Info.Valid.t
Alpha_services.Nonce.S.get.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Nonce.
Module Liquidity_baking.
Module S.
Lemma get_cpmm_address_is_valid :
RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Alpha_services.Liquidity_baking.S.get_cpmm_address.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Liquidity_baking.
Module Cache.
Module S.
Lemma cached_contracts_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True)
(List.Forall (fun '(_, i) ⇒ Pervasives.Int31.Valid.t i))
Alpha_services.Cache.S.cached_contracts.
Proof.
RPC_service.rpc_auto.
apply List.Forall_impl.
hauto l: on.
Qed.
Lemma contract_cache_size_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True) Pervasives.Int31.Valid.t
Alpha_services.Cache.S.contract_cache_size.
Proof.
RPC_service.rpc_auto.
Qed.
Lemma contract_cache_size_limit_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True) Pervasives.Int31.Valid.t
Alpha_services.Cache.S.contract_cache_size_limit.
Proof.
RPC_service.rpc_auto.
Qed.
Lemma contract_rank_is_valid :
RPC_service.Valid.t
(fun _ ⇒ True) (fun _ ⇒ True)
(Option.Forall Pervasives.Int31.Valid.t)
Alpha_services.Cache.S.contract_rank.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
End Cache.