Skip to main content

🌌 Alpha_services.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_services.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.RPC_service.
Require TezosOfOCaml.Proto_alpha.Environment.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 nonceSeed_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.