👥 Delegate_services.v

Proofs

See code, Gitlab , OCaml

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.

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.