Skip to main content

👥 Delegate_services.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Delegate_services.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.RPC_query.
Require TezosOfOCaml.Proto_alpha.Environment.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.

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_power : Int32.Valid.t x.(voting_power);
    }.
  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 ×.
  repeat split; trivial; auto; lia.
Qed.
#[global] Hint Resolve info_encoding_is_valid : Data_encoding_db.

Lemma participation_info_encoding_is_valid
  : Data_encoding.Valid.t
    Delegate_storage.participation_info.Valid.t
    Delegate_services.participation_info_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve participation_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 vTez_repr.Valid.t v
          | NoneTrue
          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.

  Lemma participation_is_valid :
    RPC_service.Valid.t
      (fun _True) (fun _True)
      Delegate_storage.participation_info.Valid.t
      Delegate_services.S.participation.
  Proof.
    RPC_service.rpc_auto.
  Qed.
End S.