👥 Delegate_services.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require Import TezosOfOCaml.Environment.V8.Proofs.Signature.
Require Import TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Delegate_services.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Vote_storage.
Module info.
Module Valid.
Import Proto_alpha.Delegate_services.info.
Record t (x : Delegate_services.info) : Prop := {
full_balance : Tez_repr.Valid.t x.(full_balance);
current_frozen_deposits : Tez_repr.Valid.t x.(current_frozen_deposits);
frozen_deposits : Tez_repr.Valid.t x.(frozen_deposits);
staking_balance : Tez_repr.Valid.t x.(staking_balance);
frozen_deposits_limit :
Option.Forall Tez_repr.Valid.t x.(frozen_deposits_limit);
delegated_balance : Tez_repr.Valid.t x.(delegated_balance);
grace_period : Int32.Valid.t x.(grace_period);
voting_info : Vote_storage.delegate_info.Valid.t x.(voting_info);
pending_consensus_keys :
Forall (fun '(x1, _) ⇒ Int32.Valid.t x1 ∧ True)
x.(pending_consensus_keys)
}.
End Valid.
End info.
Lemma info_encoding_is_valid
: Data_encoding.Valid.t info.Valid.t Delegate_services.info_encoding.
Data_encoding.Valid.data_encoding_auto.
intros [] []; simpl in *; hauto l: on.
Qed.
#[global] Hint Resolve info_encoding_is_valid : Data_encoding_db.
Module S.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require Import TezosOfOCaml.Environment.V8.Proofs.Signature.
Require Import TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Delegate_services.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Vote_storage.
Module info.
Module Valid.
Import Proto_alpha.Delegate_services.info.
Record t (x : Delegate_services.info) : Prop := {
full_balance : Tez_repr.Valid.t x.(full_balance);
current_frozen_deposits : Tez_repr.Valid.t x.(current_frozen_deposits);
frozen_deposits : Tez_repr.Valid.t x.(frozen_deposits);
staking_balance : Tez_repr.Valid.t x.(staking_balance);
frozen_deposits_limit :
Option.Forall Tez_repr.Valid.t x.(frozen_deposits_limit);
delegated_balance : Tez_repr.Valid.t x.(delegated_balance);
grace_period : Int32.Valid.t x.(grace_period);
voting_info : Vote_storage.delegate_info.Valid.t x.(voting_info);
pending_consensus_keys :
Forall (fun '(x1, _) ⇒ Int32.Valid.t x1 ∧ True)
x.(pending_consensus_keys)
}.
End Valid.
End info.
Lemma info_encoding_is_valid
: Data_encoding.Valid.t info.Valid.t Delegate_services.info_encoding.
Data_encoding.Valid.data_encoding_auto.
intros [] []; simpl in *; hauto l: on.
Qed.
#[global] Hint Resolve info_encoding_is_valid : Data_encoding_db.
Module S.
The query [list_query_value] is valid.
Lemma list_query_value_is_valid :
RPC_query.Valid.t (fun _ ⇒ True) Delegate_services.S.list_query_value.
Proof.
RPC_query.valid_auto.
Qed.
Lemma list_delegate_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Delegate_services.S.list_delegate.
RPC_service.rpc_auto.
intros; now apply List.Forall_True.
Qed.
Lemma info_value_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) info.Valid.t
Delegate_services.S.info_value.
RPC_service.rpc_auto.
Qed.
Lemma full_balance_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.full_balance.
RPC_service.rpc_auto.
Qed.
Lemma frozen_deposits_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.frozen_deposits.
RPC_service.rpc_auto.
Qed.
Lemma staking_balance_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.staking_balance.
RPC_service.rpc_auto.
Qed.
Lemma frozen_deposits_limit_is_valid
: RPC_service.Valid.t
(fun _ ⇒ True)
(fun _ ⇒ True)
(fun x ⇒
match x with
| Some v ⇒ Tez_repr.Valid.t v
| None ⇒ True
end
)
Delegate_services.S.frozen_deposits_limit.
RPC_service.rpc_auto.
Qed.
Lemma delegated_contracts_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Delegate_services.S.delegated_contracts.
RPC_service.rpc_auto.
intros; now apply List.Forall_True.
Qed.
Lemma delegated_balance_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.delegated_balance.
RPC_service.rpc_auto.
Qed.
Lemma deactivated_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Delegate_services.S.deactivated.
RPC_service.rpc_auto.
Qed.
Lemma grace_period_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Int32.Valid.t
Delegate_services.S.grace_period.
RPC_service.rpc_auto.
Qed.
Lemma voting_power_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Int32.Valid.t
Delegate_services.S.voting_power.
RPC_service.rpc_auto.
intros; lia.
Qed.
End S.
RPC_query.Valid.t (fun _ ⇒ True) Delegate_services.S.list_query_value.
Proof.
RPC_query.valid_auto.
Qed.
Lemma list_delegate_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Delegate_services.S.list_delegate.
RPC_service.rpc_auto.
intros; now apply List.Forall_True.
Qed.
Lemma info_value_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) info.Valid.t
Delegate_services.S.info_value.
RPC_service.rpc_auto.
Qed.
Lemma full_balance_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.full_balance.
RPC_service.rpc_auto.
Qed.
Lemma frozen_deposits_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.frozen_deposits.
RPC_service.rpc_auto.
Qed.
Lemma staking_balance_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.staking_balance.
RPC_service.rpc_auto.
Qed.
Lemma frozen_deposits_limit_is_valid
: RPC_service.Valid.t
(fun _ ⇒ True)
(fun _ ⇒ True)
(fun x ⇒
match x with
| Some v ⇒ Tez_repr.Valid.t v
| None ⇒ True
end
)
Delegate_services.S.frozen_deposits_limit.
RPC_service.rpc_auto.
Qed.
Lemma delegated_contracts_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Delegate_services.S.delegated_contracts.
RPC_service.rpc_auto.
intros; now apply List.Forall_True.
Qed.
Lemma delegated_balance_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Tez_repr.Valid.t
Delegate_services.S.delegated_balance.
RPC_service.rpc_auto.
Qed.
Lemma deactivated_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Delegate_services.S.deactivated.
RPC_service.rpc_auto.
Qed.
Lemma grace_period_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Int32.Valid.t
Delegate_services.S.grace_period.
RPC_service.rpc_auto.
Qed.
Lemma voting_power_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Int32.Valid.t
Delegate_services.S.voting_power.
RPC_service.rpc_auto.
intros; lia.
Qed.
End S.